Содержание дисциплины "Математическая логика"
Раздел 1. Исчисление высказываний.
Тема 1.1.Формальные исчисления. Язык исчисления высказываний (ИВ). Система аксиом и правил вывода ИВ. Понятие вывода формулы из множества гипотез. Теорема о дедукции.
Тема 1.2.Основные эквивалентности. Нормальные формы. Интерпретации и семантика ИВ. Тождественно истинные и тождественно ложные формулы. Непротиворечивость, полнота и разрешимость ИВ.
Тема 1.3. Алгоритм Квайна и алгоритм редукции проверки общезначимости формул. Метод резолюций в ИВ. Хорновские дизъюнкты.
Раздел 2. Исчисление предикатов.
Тема 2.1. Алгебраические системы. Формулы логики предикатов. Истинность формул на алгебраических системах. Выполнимость формул логики предикатов. Модель множества формул. Теорема компактности.
Тема 2.2. Исчисление предикатов (ИП): аксиомы и правила вывода. Основные эквивалентности ИП. Пренексные нормальные формы. Непротиворечивость и полнота ИП.
Тема 2.3. Элементарные теории. Полные теории. Категоричность в мощности. Система аксиом арифметики Пеано. Стандартные и нестандартные модели арифметики.
Тема 2.4. Метод резолюций в ИП.
Тема 2.5. Формальное определение программы. Логические формулы, описывающие исполнение программ. Анализ программ с помощью резолюции. Понятие о логическом программировании и языке программирования Пролог.
Раздел 3. Алгоритмы и рекурсивные функции.
Тема 3.1. Понятие алгоритма. Тезис Чёрча. Машины Тьюринга. Вычислимость на машинах Тьюринга.
Тема 3.2. Примитивно рекурсивные и частично рекурсивные функции. Рекурсивность основных арифметических операций. Нумерация множества кортежей натуральных чисел. Рекурсивные множества. Эквивалентность моделей алгоритмов.
Тема 3.3. Универсальная частично рекурсивная функция. Существование нерекурсивных множеств. Рекурсивно перечислимые множества. Гёделевская нумерация формул, аксиом и правил вывода ИП. Разрешимые и неразрешимые теории. Теорема Чёрча о неразрешимости арифметики. Теорема Гёделя о неполноте арифметики.
Тема 3.4. Временнaя и ёмкостная сложность алгоритмов. Классы алгоритмов P и NP. Метод сводимости. NP-полные задачи.
Тема 3.5. Конечные автоматы. Способы задания автоматов. Операции над автоматами. Детерминированные и недетерминированные конечные автоматы, связь между ними. Состояния и эквивалентные состояния автоматов.
Раздел 4. Неклассические логики.
Тема 4.1. Пропозициональные логики: интуиционистские логики, многозначные логики, нечеткие логики и нечеткие подмножества, модальные логики, временные (темпоральные) логики, квантовые логики.
Тема 4.2. Предикатные логики: многосортные логики первого порядка, слабая логика второго порядка, бесконечные логики, логики с новыми кванторами, предикатные временные логики и их приложение к программированию, алгоритмические логики.
Тема 4.3. Комбинаторная логика Карри и ламбда-исчисление Чёрча. Понятие о функциональном программировании и языке программирования Хаскелл.