Раздел 4. ТЕОРИЯ АЛГОРИТМОВ

РАБОЧАЯ ПРОГРАММА

Дисциплины

МАТЕМАТИЧЕСКАЯ ЛОГИКА И ТЕОРИЯ АЛГОРИТМОВ

Квалификация выпускника - бакалавр

Уровень высшего образования - первый

Специальность 220400 « Программное обеспечение ВТ

и автоматизированных систем»

Тула 2009

Программу составил доцент каф. АТМ О.В.Красоткина

Рабочая программа обсуждена на заседании кафедры автоматики и телемеханики “22” декабря 2009 г., протокол № 6.

Зав. кафедрой _________________ А.А. Фомичев

Цели и задачи дисциплины:

Цель дисциплины – ознакомление с основными понятиями и методами математической логики и теории алгоритмов с ориентацией на их использование в практической информатике и вычислительной технике.

Требования к уровню освоения дисциплины

В результате изучения дисциплины студенты должны:

1. Знать основные понятия и методы математической логики и теории алгоритмов, используемые в информатике и вычислительной технике.

2. Уметь использовать их для построения несложных логических моделей предметных областей, реализации логического вывода и оценки вычислительной сложности алгоритмов

3. Иметь представление о направлениях развития данной дисциплины и перспективах ее использования в информатике и вычислительной технике.

РАСПРЕДЕЛЕНИЕ ЧАСОВ ПО СЕМЕСТРАМ И ВИДАМ ЗАНЯТИЙ

Виды аудиторных занятий, ч
Семестр	Лекции	Лабор. занятия	Практ. занятия	ККР	Инд. работа	Вид отчетн.	Итого
						зачет
Итого по дисц.						зачет

ТЕМЫ И СОДЕРЖАНИЕ ЛЕКЦИЙ

ВВЕДЕНИЕ

Предмет курса, его связь с другими дисциплинами учебного плана, значение

Раздел 1. ЛОГИКА ВЫСКАЗЫВАНИЙ

Тема 1. Основы логики высказываний -4 часа

Язык логики высказываний. Синтаксис языка: алфавит и правила построения формул. Семантика языка, интерпретация формул. Свойства формул: общезначимость, выполнимость, противоречивость.

Методы анализа выполнимости и общезначимости формул: семантическое дерево, тривиальный алгоритм, алгоритм Квайна, алгоритм редукции, алгебраический подход. Алгоритм преобразования формул в КНФ. Базовый алгоритм проверки общезначимости КНФ, модификация Девиса-Патнема.

Тема 2. Вывод в логике высказываний -2 часа

Понятие логического следования, проблема дедукции. Принцип дедукции. Правило резолюций, метод резолюций. Стратегии метода резолюций.

Раздел 2. ЛОГИКА ПРЕДИКАТОВ

Тема 3. Язык логики предикатов-2 часа

Синтаксис языка логики предикатов: алфавит, термы, атомы, правила построения формул. Свободные и связанные вхождения переменных, замкнутые формулы. Семантика языка логики предикатов, интерпретация формул.

Тема 4. Логический вывод в логике предикатов -4 часа

Предваренная, сколемовская и клаузальная формы. Алгоритм получения клаузальной формы. Метод резолюций в логике предикатов. Теорема Робинсона. Подстановка, композиция подстановок, унификатор. Алгоритм построения наиболее общего унификатора. Хорновские дизъюнкты и метод резолюций на хорновских дизъюнктах. Принцип логического программирования.

Раздел 3. ФОРМАЛЬНЫЕ (АКСИОМАТИЧЕСКИЕ) СИСТЕМЫ

Тема 5. Основы теории формальных систем -4 часа

Понятия формальной системы и формального вывода. Исчисление высказываний как формальная система, множественность аксиоматизаций. Теорема дедукции. Связь выводимости и истинности формул в логике высказываний. Исчисление предикатов как формальная система. Примеры формального вывода.

Тема 6. Метатеория формальных систем -2 часа

Основные свойства формальных систем: непротиворечивость, полнота, разрешимость. Теоремы о неполноте формальных систем, смысл и значение теорем Геделя для практической информатики.

Раздел 4. ТЕОРИЯ АЛГОРИТМОВ

Тема 7. Алгоритмические системы. Алгоритмически разрешимые и неразрешимые задачи -4 часа

Понятие алгоритмической системы. Частично-рекурсивные функции, тезис Черча.

Машины Тьюринга, тезис Тьюринга. Рекурсивные и рекурсивно-перечислимые множества и языки. Алгоритмически разрешимые и неразрешимые задачи. Проблема остановки, проблема пустой ленты, метод сведения.

Тема 8. Сложность алгоритмов -6 часов

Меры сложности алгоритмов: временная и емкостная сложность. Асимптотическая сложность, порядок сложности. Сложность в среднем и в худшем случае.

Языки и задачи. Легко- и трудноразрешимые задачи, классы задач P и NP. NP-полные задачи. Недетерминированная машина Тьюринга (НМТ). Сложность моделирования НМТ с помощью ДМТ. Примеры NP-полных задач. Полиномиальная сводимость и полиномиальная трансформируемость. Теорема Кука. Примеры практически значимых NP-полных задач. Задача 3-выполнимости, доказательство NP-полноты методом сведения.

Тема 9. Алгоритмическая логика -2 часа

Алгоритмическая логика Хоара. Предусловие и постусловие алгоритма. Тройки Хоара. Формальная постановка задачи верификации. Понятие слабейшего предусловия и его основные свойства. Верификация операторов присваивания и их последовательностей.

ЗАКЛЮЧЕНИЕ –2 часа

Перспективы развития методов математической логики для решения задач спецификации и верификации программно-аппаратных средств, создания систем искусственного интеллекта и Семантического Web.