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

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

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

Слайды лекций

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

Сборники задач для семинаров

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

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

Материалы прошлого года

Лектором был Захаров В.А..

Материалы, в том числе слайды и видеозаписи лекций, - по ссылке в папке "ЗахаровВА".

Коллоквиум

Коллоквиум проводится по материалам лекций и семинарских занятий, охватывающих вопросы 1-19 программы курса, письменно на одном из лекционных занятий, длительность - одна пара (90 минут). Вариант коллоквиума содержит 12 задач:

• 3 типовые задачи:
  1. Формализовать в логике предикатов с заданной сигнатурой заданное предложение, записанное на естественном языке.
  2. Обосновать общезначимость заданной формулы логики предикатов методом семантических таблиц.
  3. Обосновать общезначимость заданной формулы логики предикатов методом резолюций.
• 9 теоретических задач в форме теста с множественным выбором:
  • среди предложенных вариантов ответа требуется выбрать и отметить правильные (один, ни одного или несколько, в том числе, быть может, все),
  • обосновывать выбор не требуется.

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

Техническими баллами, набранными за коллоквиум, определяется добавка (бонус или штраф) к техническим баллам за экзаменационную работу:

• хотя бы 14 на коллоквиуме: +3 балла на экзамене;
• хотя бы 12, но менее 14: +2 балла;
• хотя бы 10, но менее 12: +1 балл;
• хотя бы 8, но менее 10: +0 баллов;
• хотя бы 6, но менее 8: -1 балл;
• хотя бы 4, но менее 6: -2 балла;
• менее 4: -3 балла;
• коллоквиум пропущен по неуважительной причине: -3 балла;
• коллоквум пропущен по уважительной причине: +0 баллов.

Экзамен

Экзамен проводится письменно, длительность - 150 минут. Вариант экзамена содержит 14 задач:

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

Правильно написанная логическая программа оценивается в 6 баллов. Правильное решение типовой задачи оценивается в 3 балла. Правильное решение вопроса на формулировку оценивается в 2 балла. Правильное решение вопроса на обоснование оценивается в 3 балла. Наибольший возможный балл за решение варианта экзамена - 40.

Баллы, полученные за решение варианта экзамена, складываются с бонусом/штрафом за коллоквиум. По полученной сумме определяется оценка:

• хотя бы 32 балла: отлично;
• хотя бы 24 балла, но менее 32: хорошо.
• хотя бы 16 баллов, но менее 24: удовлетворительно.
• менее 16 баллов: неудовлетворительно.

Программа

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

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

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: формулировка, решающий алгоритм.

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

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

Литература

Основная

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 с.