Математическая логика и логическое программирование (3-й поток)

Актуальность информации: осенний семестр 2025/2026 учебного года.

Обязательный курс для студентов 3 потока 4 курса в 7 семестре. Лектор: Подымов В.В.

Материалы занятий

Лекции

Блок 1 (вступительный). Что такое логика. Несколько логических парадоксов. Чего ожидать в лекциях.

Блок 2. Логика высказываний: синтаксис, семантика.

Блок 3. Логика предикатов: синтаксис, семантика.

Блок 4. Как формализовать предложение на языке логики предикатов (пример).

Блок 5. Логика высказываний: выполнимые и общезначимые формулы.

Блок 6. Логика предикатов: выполнимые и общезначимые формулы, модели формул, логическое следствие, проблема общезначимости формул (постановка).

Блок 7. Логика предикатов: можно ли проверить общезначимость формулы "в лоб"?

Блок 8. Метод семантических таблиц: семантические таблицы.

Блок 9. Подстановки (основные определения).

Блок 10. Метод семантических таблиц: табличный вывод.

Блок 11. Метод семантических таблиц: корректность табличного вывода.

Блок 12. Метод семантических таблиц: полнота табличного вывода.

Блок 13. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Автоматизация доказательства теорем.

Блок 14. Общая схема метода резолюций.

Блок 15. Равносильность формул логики предикатов.

Блок 16. Предварённая нормальная форма (ПНФ).

Блок 17. Сколемовская стандартная форма (ССФ).

Блок 18. Системы дизъюнктов.

Блок 19. Композиция подстановок. Постановка задачи унификации.

Материалы будут появляться по мере проведения занятий.

Прошлогодние

Блок 20. Алгоритм унификации атомарных формул.

Блок 21. Монотонность и транзитивность логического следования.

Блок 22. Резолютивный вывод. Корректность резолютивного вывода.

Блок 23. Обоснование общезначимости формулы методом резолюций (пример).

Блок 24. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях.

Блок 25. Теорема Эрбрана. Полнота резолютивного вывода.

Блок 26. Иллюстрация полноты резолютивного вывода.

Блок 27. Стратегии резолютивного вывода.

Блок 28. Даша, Саша, Паша, пиво и метод семантических таблиц с методом резолюций.

Блок 29. Хорновские дизъюнкты.

Блок 30. Вычислительные возможности метода резолюций.

Блок 31. Хорновские логические программы: синтаксис, декларативная семантика, правильные ответы.

Блок 32. Хорновские логические программы: списки.

Блок 33. Хорновские логические программы: операционная семантика, SLD-резолютивные вычисления, SLD-вычислимые ответы.

Блок 34. Хорновские логические программы: корректность операционной семантики.

Блок 35. Хорновские логические программы: полнота операционной семантики.

Блок 36. Хорновские логические программы: содержательное сравнение семантик.

Блок 37. Хорновские логические программы: переключательная лемма, сильная полнота операционной семантики, стандартное правило выбора подцели.

Блок 38. Хорновские логические программы: деревья SLD-резолютивных вычислений, стратегии вычисления и их полнота, стандартная стратегия вычисления.

Блок 39. Машины Тьюринга.

Блок 40. Моделирование машин Тьюринга хорновскими логическими программами.

Блок 41. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.

Блок 42. Теорема Чёрча.

Блок 43. Логические программы: встроенные предикаты и функции.

Блок 44. Логические программы: стековые вычисления.

Блок 45. Логические программы: управление вычислениями, оператор отсечения.

Блок 46. Отрицание в логическом программировании. Допущение замкнутости мира.

Блок 47. Логические программы: оператор отрицания, SLDNF-резолюция.

Блок 48. Модальные логики.

Блок 49. Эпистемические логики.

Блок 50. Темпоральные логики.

Блок 51. Интуиционистская логика.

Блок 52. Формальная верификация.

Блок 53. Модельные императивные программы. Постановка задачи верификации программ.

Блок 54. Логика Хоара. Автоматизация проверки правильности программ.

Блок 55. Проверка правильности распределённых систем. Пара слов о методе проверки моделей.

Блок 56. Размеченные системы переходов.

Блок 57. Спецификация систем при помощи темпоральных логик.

Блок 58. Алгоритм model checking для CTL.

Вне программы 1 Логические исчисления.

Вне программы 2. Натуральные исчисления.

Вне программы 3. Пара слов о лямбда-исчислении.

Вне программы 4. Изоморфизм Карри-Говарда.

Вне программы 5. Теорема Гёделя о полноте.

Вне программы 6. Формальная арифметика. Теорема Гёделя о неполноте.

Все слайды лекций к экзамену в одном файле.

Семинары

Задачи, обсуждающиеся на семинарах.

Расширенный сборник задач для самостоятельного решения.

Экзамен и контрольные работы

На контрольных работах и на экзамене будут задачи следующих видов со следующими техническими баллами за полное правильное решение (в случае ошибок решению даётся меньший балл в зависимости от количества и качества ошибок):

• Типовые задачи (4 балла):
  1. Формализовать в логике предикатов предложение, записанное на естественном языке (семинар 1).
  2. Обосновать общезначимость формулы логики предикатов методом семантических таблиц (семинар 2).
  3. Обосновать общезначимость формулы логики предикатов методом резолюций (семинары 3 и 4).
  4. Построить дерево SLD-резолютивных вычислений заданной логической программы (семинары 5-7).
• Логическая программа (8 баллов). Написанию таких программ посвящены семинары 5-7.
• Задачи с формулировками (3 балла). Такая задача состоит из трёх частей:
  1. Сформулировать утверждение, определение и т.п.
  2. Ответить на вопрос "на понимание", так или иначе связанный с формулировкой.
  3. Аргументировать (обосновать) ответ на вопрос.
• Задача на понимание (4 балла). В этой задаче содержится один или несколько (не более трёх) близких (смежных, взаимосвязанных, схожих и т.п.) вопросов на углублённое понимание материалов курса (в том числе доказательств), на каждый из которых требуется ответить с обоснованием.

Контрольные работы

На лекциях будет проведено три контрольных работы, каждая - письменно на одну пару за вычетом 15 минут от начала пары на раскладку вариантов, рассадку студентов и отмашку о начале работы.

В первой контрольной работе содержатся типовые задачи 1 и 2, одна задача с формулировкой и две задачи на понимание. Во второй контрольной работе содержатся типовая задача 3, две задачи с формулировкой и две задачи на понимание. В третьей контрольной работе содержатся типовая задача 4, логическая программа, одна задача с формулировкой и одна задача на понимание.

Экзамен

Экзамен проводится письменно, длительность - 150 минут. В варианте экзамена содержатся три группы задач, в каждой группе - столько же и такого же вида, как на соответствующей контрольной работе.

По итогам экзамена определяются 4 технических оценки:

1. Если на экзамене предпринята попытка решить задачи первой группы, то берётся сумма баллов за это решение, а иначе - сумма баллов за решение задач первой контрольной работы.
2. То же относительно второй группы и второй контрольной работы.
3. То же относительно третьей группы и третьей контрольной работы.
4. Баллы за особые заслуги. Эти баллы оговариваются индивидуально с желающими их заслужить. К особым заслугам относится, в частности, решение задач, записанных в слайдах лекций оранжевым цветом в чёрной рамке.

Полученные 4 технических оценки складываются, и в зависимости от этой суммы определяется оценка за экзамен:

Сумма	Оценка
Хотя бы 45	Отлично
34-44	Хорошо
23-33	Удовлетворительно
22 или меньше	Неудовлетворительно

Максимальные баллы за контрольные работы и за экзамен (без учёта особых заслуг):

• Первая контрольная: 19 баллов.
• Вторая контрольная: 18 баллов.
• Третья контрольная: 19 баллов.
• Экзамен (три контрольные вместе): 56 баллов.

Программа

Программа может уточняться по мере проведения занятий.

Классические логики

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

Метод резолюций в логике предикатов

10. Предварённая нормальная форма. Теорема о предварённой нормальной форме.
11. Сколемовская стандартная форма. Алгоритм сколемизации предварённой нормальной формы. Теорема о сколемизации.
12. Дизъюнкты. Сведение проблемы общезначимости формул к проблеме невыполнимости систем дизъюнктов.
13. Композиция подстановок. Унификатор. Наиболее общий унификатор. Задача унификации выражений логики предикатов.
14. Лемма о связке. Алгоритм унификации. Теорема об унификации.
15. Правило резолюции. Правило склейки. Резолютивный вывод. Теорема о корректности резолютивного вывода.
16. Эрбрановский универсум. Эрбрановский базис. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях. Теорема Эрбрана.
17. Лемма об основных дизъюнктах. Лемма о подъёме. Теорема о полноте резолютивного вывода.
18. Метод резолюций: общая схема, применение.
19. Стратегии резолютивного вывода. Семантическая резолюция. Входной вывод.
20. Хорновские дизъюнкты.
21. Резолютивный вывод как средство вычисления ответов на запросы.

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

22. Синтаксис хорновских логических программ: факты, правила, утверждения, программы, подцели, запросы.
23. Декларативная семантика хорновских логических программ, правильный ответ на запрос.
24. SLD-резолюция. SLD-резолютивное вычисление хорновской логической программы. Успешные, тупиковые и бесконечные вычисления программ. Операционная семантика программ, вычислимый ответ на запрос.
25. Корректность и полнота операционной семантики хорновских логических программ относительно декларативной.
26. Правило выбора подцели. Переключательная лемма, теорема о сильной полноте SLD-резолюции.
27. Дерево SLD-резолютивных вычислений. Стратегия вычисления хорновских логических программ, примеры полных и неполных стратегий. Стандартная стратегия вычисления.
28. Встроенные функции и предикаты в логических программах, их операционная семантика.
29. Управление вычислениями логических программ. Оператор отсечения, его операционная семантика.
30. Отрицание в логических программах. Гипотеза замкнутости мира. Оператор отрицания, его операционная семантика.
31. Машины Тьюринга, моделирование их логическими программами. Теорема Чёрча.

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

32. Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики. Логика линейного времени. Логика деревьев вычислений.
33. Интуиционистская логика. Модели Крипке для интуиционистской логики.
34. Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Полная и частичная корректность программ. Тройки Хоара. Логика Хоара. Корректность вывода в логике Хоара. Слабейшее предусловие. Инвариант цикла.
35. Размеченные системы переходов. Моделирование программ системами переходов. Логика деревьев вычислений (CTL): синтаксис, семантика, основные равносильности, применение для спецификации поведения распределённых систем. Задача проверки моделей (model checking) относительно CTL: формулировка, решающий алгоритм.

Литература

Основная

1. Клини С. Математическая логика. М.:Мир, 1973, 480 с.
2. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.:Мир, 1983. 360 с.
3. Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логике и теории алгоритмов. Москва, "Физико-математическая литература", 1995 г., 250 с.
4. Метакидес Г., Нероуд А., Принципы логики и логического программирования. Москва, "Факториал", 1998, 288 с.
5. Братко И. Программирование на Прологе для искусственного интеллекта. М.:Мир, 1990, 560 с.
6. Набебин А.А. Логика и Пролог в дискретной математике. М., Изд-во МЭИ, 1997.
7. Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: model checking. Изд-во МЦНМО, Москва, 2002, 405 с.

Дополнительная

1. Мендельсон Э. Введение в математическую логику. М.:Наука, 1984. 319 с.
2. Верещагин Н.К., Шень А. Языки и исчисления. 2004.
3. Успенский В.А., Верещагин Н.К., Плиско В.Е. Вводный курс математической логики. 2004. 128 с.
4. Лавров И.А. Математическая логика. Учебное пособие для вузов. М.: Академия, 2006.
5. Колмогоров А.Н., Драгалин А.Г. Математическая логика. Серия "Классический университетский учебник". Изд.3, 2006, 240 с.
6. Ершов Ю.Л., Палютин Е.А. Математическая логика - М.: 1979.
7. Непейвода Н. Н. Прикладная логика. Новосибирск. 2000 г.
8. Хоггер К., Введение в логическое программирование. М.:Мир, 1988. 348 с.
9. Клоксин У., Меллиш К. Программирование на языке Пролог. М.:Мир, 1987. 336 с.
10. Кларк К.Л., Маккейб Ф.Г. Микро-Пролог: введение в логическое программирование. Москва, "Радио и связь". 1987, 311 с.
11. Стерлинг Л., Шапиро Э., Искусство программирования на языке ПРОЛОГ. Москва, "Мир", 1990, 235 с.
12. Ковальский Р. Логика в решении проблем. М.: Наука, 1990. 277 с.
13. Логический подход к искусственному интеллекту (от модальной логики к логике баз данных). М.:Мир, 1998. 495 с.

Материалы для подготовки к государственному экзамену

Материалы составлены для выпуска 2025.

Вопрос 3. Логика 1-го порядка. Выполнимость и общезначимость. Общая схема метода резолюций.

Вопрос 4. Логическое программирование. Декаларативная семантика и операционная семантика, соотношение между ними. Стандартная стратегия выполнения логических программ.