МИНОБРНАУКИ
ТОМСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ
ФАКУЛЬТЕТ ИНФОРМАТИКИ
УТВЕРЖДАЮ
Декан факультета
« » 2010 г.
МАТЕМАТИЧЕСКАЯ ЛОГИКА И ТЕОРИЯ АЛГОРИТМОВ
(СД.02)
РАБОЧАЯ ПРОГРАММА
трудоемкость дисциплины 4 зачетные единицы
НАПРАВЛЕНИЕ 080800 – ПРИКЛАДНАЯ ИНФОРМАТИКА
Томск
2010
УТВЕРЖДЕНО кафедрой программной инженерии. Протокол №19 от 01.01.2001 Зав. кафедрой, профессор | СОСТАВИТЕЛЬ старший преподаватель кафедры программной инженерии |
II. Организационно-методический раздел
Цель курса – изучение методов математической логики.
Задача учебного курса – ознакомление с основными понятиями и методами математической логики и теории алгоритмов с ориентацией на их использование в практической информатике.
Дисциплины-предшественники – нет.
Требования к уровню освоения дисциплины – умение пользоваться методами математической логики, оценивать вычислительную сложность алгоритмов.
III. Содержание дисциплины
III.1. Лекционный курс
Тема 1. Логика высказываний.
Язык логики высказываний. Синтаксис языка: алфавит и правила построения формул. Семантика языка, интерпретация формул. Свойства формул: общезначимость, выполнимость, противоречивость.
Тема 2. Методы анализа выполнимости и общезначимости формул.
Семантическое дерево, алгоритмы Квайна и Девиса-Патнема, алгебраический подход. Алгоритм преобразования формул в КНФ и ДНФ.
Тема 3. Вывод в логике высказываний.
Понятие логического следования Методы логического вывода. Метод резолюций в логике высказываний, стратегии вычеркивания.
Тема 4. Логика предикатов.
Синтаксис языка логики предикатов: алфавит, термы, атомы, правила построения формул. Свободные и связанные вхождения переменных, замкнутые формулы. Семантика языка логики предикатов, интерпретация формул.
Тема 5. Логический вывод в логике предикатов.
Предваренная нормальная форма, сколемизация, приведения к стандартной нормальной форме. Метод резолюций в логике предикатов. Теорема о полноте резолютивного вывода. Унификация, нахождение наиболее общего унификатора. Хорновские дизъюнкты и метод резолюций на них. Принципы логического программирования.
Тема 6. Формальные системы.
Понятия формальной системы и формального вывода. Исчисление высказываний как формальная система, множественность аксиоматизаций. Теорема дедукции. Связь выводимости и истинности формул в логике высказываний. Исчисление предикатов как формальная система. Примеры формального вывода.
Тема 7. Метатеория формальных систем.
Основные свойства формальных систем: непротиворечивость, полнота, разрешимость. Теоремы о неполноте формальных систем, смысл и значение теорем Геделя для практической информатики.
Тема 8. Теория алгоритмов.
Понятие алгоритмической системы. Частично-рекурсивные функции, тезис Черча. Машины Тьюринга, тезис Тьюринга. Рекурсивные и рекурсивно-перечислимые множества и языки. Алгоритмически разрешимые и неразрешимые задачи.
Тема 9. Сложность алгоритмов.
Меры сложности алгоритмов. Классы задач P и NP. NP – полные задачи.
III.2. Практические занятия
По некоторым темам лекционной части курса предусмотрены практические занятия.
IV. Распределение часов курса по темам и видам работ
№№ пп | Наименование тем | Всего часов | Аудиторные занятия (час), в том числе | Самостоятельная работа | ||
лекции | практики | лабораторные занятия | ||||
1 | Логика высказываний | 6 | 4 | 2 | ||
2 | Методы анализа выполнимости и общезначимости формул | 10 | 6 | 2 | 2 | |
3 | Вывод в логике высказываний | 12 | 6 | 2 | 4 | |
4 | Логика предикатов | 6 | 4 | 2 | ||
5 | Логический вывод в логике предикатов | 12 | 6 | 2 | 4 | |
6 | Формальные системы | 6 | 4 | 2 | ||
7 | Метатеория формальных систем | 6 | 4 | 2 | ||
8 | Теория алгоритмов | 10 | 6 | 4 | ||
9 | Сложность алгоритмов | 12 | 6 | 2 | 4 | |
ИТОГО | 80 | 46 | 8 | 0 | 26 |
