Модели вычислений

Лектор - профессор Захаров Владимир Анатольевич.

Программа курса

Логика предикатов первого порядка

1. Синтаксис и семантика логики предикатов. Термы, формулы, интерпретация. Отношение выполнимости формулы на интерпретации.
2. Выполнимость, общезначимость, противоречивость формул логики предикатов. Примеры общезначимых и противоречивых формул логики предикатов. Модель. Логическое следствие. Теорема о логическом следствии.
3. Проблемы выполнимости и общезначимости. Пример формулы, не имеющей конечных моделей.
4. Семантические таблицы в логике предикатов. Табличный вывод. Теорема корректности табличного вывода.
5. Теорема полноты табличного вывода.
6. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева.
7. Равносильные формулы. Примеры равносильных формул. Теорема о равносильной замене.

Метод резолюций

8. Предваренная нормальная форма. Теорема о приведении формулы к предваренной нормальной форме.
9. Сколемовская стандартная форма. Теорема о приведении формулы к сколемовской стандартной форме.
10. Эрбрановский универсум, эрбрановский базис, эрбрановские интерпретации. Теорема об эрбрановской модели для сколемовской стандартной формы. Сведение проблемы общезначимости формул к проблеме противоречивости систем дизъюнктов. Теорема Эрбрана.
11. Подстановки. Применение подстановок к термам и формулам. Композиция подстановок. Унификатор. Наиболее общий унификатор.
12. Сведение задачи унификации к задаче решения системы термальных уравнений. Лемма о связке. Алгоритм унификации. Теорема о корректности и завершаемости алгоритма унификации.
13. Метод резолюций для логики предикатов: правила резолюции и склейки, резолютивный вывод. Теорема корректности резолютивного вывода.
14. Лемма о подъеме. Теорема полноты резолютивного вывода для логики предикатов.
15. Общая схема доказательства общезначимости формул логики предикатов методом резолюций. Стратегии резолютивного вывода.

Основы логического программирования

16. Использование метода резолюций для нахождения ответов на запросы. Истолкование резолютивного вывода как вычисления. Примеры вычислительных возможностей резолютивного вывода.
17. Хорновские дизъюнкты. Синтаксис языка логического программирования: логические программы и запросы. Декларативная семантика логических программ. Правильный ответ.
18. Теорема о пересечении эрбрановских моделей логических программ. Теорема о наименьшей эрбрановской модели. Теорема об основных правильных ответах.
19. SLD-резолюция. SLD-резолютивные вычисления (опровержения) логических программ. Процедурная интерпретация SLD-выводов. Примеры SLD-опровержений успешных, тупиковых и бесконечных. Вычислимый ответ. Операционная (процедурная) семантика логических программ.
20. Теорема корректности SLD-резолютивных вычислений логических программ.
21. Теорема полноты SLD-резолютивных вычислений логических программ.
22. Правило вычислений и его роль. R-вычислимый ответ. Переключательная лемма. Теорема о независимости правила вычислений. Теорема сильной полноты SLD-резолюции.
23. Дерево SLD-вычислений логических программ. Стратегии вычислений. Полные и неполные стратегии вычислений. Стандартная стратегия исполнения логических программ. Неполнота стандартной стратегии.
24. Управление исполнением логических программ. Оператор отсечения. Операционная семантика оператора отсечения.
25. Отрицание в Прологе. Допущение замкнутости мира. Отрицание как неудача. Эффект немонотонности вычислений логических программ с оператором отрицания.
26. Встроенные предикаты и функции. Операционная семантика встроенных средств.
27. Теорема о вычислительной универсальности чистого Пролога. Теорема Чёрча о неразрешимости логики предикатов первого порядка.

Неклассические прикладные логики

28. Интуиционистская логика. Модели Крипке для интуиционистской логики. Примеры интуиционистски общезначимых и необщезначимых формул. Модальные логики. Модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики.
29. Проблема верификации последовательных программ. Операционная семантика типовых программных конструкций. Предусловие и постусловие. Частичная корректность программ. Тройки Хоара и их содержательный смысл. Правила вывода в логике Хоара для доказательства частичной корректности последовательных программ.
30. Моделирование программ системами переходов. Темпоральная логика высказываний линейного времени (LTL): синтаксис и семантика. Применение темпоральных логик для спецификации поведения реагирующих программных систем.
31. Задача проверки выполнимости формул LTL на конечной модели. Равносильные преобразования формул LTL. Табличный алгоритм проверки выполнимости формул LTL на конечной модели: основные этапы.

Основания математики

32. Как устроена математика. Исчисление предикатов первого порядка. Аксиоматические теории. Элементарная геометрия. Теория множеств Цермело-Френкеля. Арифметика Пеано. Теорема Геделя о неполноте формальной арифметики.