Математическая логика (318, 319/2, 241, 242)

Материал из Кафедра математической кибернетики
Версия от 12:25, 10 февраля 2026; PodymovVV (обсуждение | вклад)

(разн.) ← Предыдущая | Текущая версия (разн.) | Следующая → (разн.)
Перейти к: навигация, поиск


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

Обязательный курс для студентов групп 318 и 319/2, 241 и 242. Курс читает В. В. Подымов.

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

Блок 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. Натуральное исчисление предикатов: полнота.

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

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

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

Блок 37. Аксиоматические теории первого порядка. Проблема общезначимости формул в теории.

Блок 38. Основные свойства аксиоматических теорий.

Блок 39. Арифметические интерпретации и теории.

Блок 40. Определения и выразимость.

Блок 41. Формальная арифметика. Теорема Гёделя о неполноте.

Блок 42. Арифметика Пресбургера.

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

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

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

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

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

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

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

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

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

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

Блок 53. Алгоритм проверки моделей для CTL.

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

Семинары

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

Семинары 1-4 проводятся по этому сборнику задач.

Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к расширенному сборнику задач

Материалы семинара 5-6 (натуральное исчисление).

Контрольные работы, зачёт и экзамен

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

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

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

На лекциях будет проведено три контрольных работы, каждая - письменно, 80 минут (остальное время занятия резервируется для раскладки вариантов, рассадки студентов, отмашки о начале работы, сбора работ и прочего). Использование любых источников, кроме своей головы, запрещено.

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

Максимальная оценка за первую контрольную работу - 19 баллов, за вторую и третью - по 18 баллов, суммарная максимальная оценка за все контрольные работы - 55 баллов.

Зачёт

Чтобы получить зачёт, требуется получить два результата:

  1. Набрать хотя бы 11 баллов за типовые задачи.
  2. Набрать хотя бы 24 балла за всё, что есть в курсе.

В зачётную неделю будет дано две попытки переписывания контрольных работ. На каждой попытке можно переписать одну контрольную работу и/или любые типовые задачи.

В подсчёте баллов учитываются:

  • По каждой типовой задаче - максимальная набранная оценка по все попыткам её решить.
  • По нетиповым задачам каждой контрольной - максимальный суммарный балл за них по всем попыткам написания и переписывания контрольной.

Экзамен

Экзамен проводится письменно, длится 150 минут и состоит в переписывании любого количества контрольных работ. До экзамена каждый сдающий может изъявить желание сохранить оценки тех или иных контрольных работ. На самом экзамене обнуляются и пишутся заново все контрольные работы, по которым такое желание не было изъявлено.

Суммарный балл за все контрольные работы преобразуется в оценку следующим образом:

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

Бонусные баллы

Помимо контрольных работ, баллы даются за решение премиальных задач и за особые заслуги.

Премиальные задачи

Премиальные задачи объявляются по мере проведения занятий. Для каждой задачи определяются премия и номер контрольной работы.

Премии распределяются в каждой группе независимо от других. Например, "первый" означает "первый в 318, первый в 319/2, первый в 241 и первый в 242".

Премия добавляется к баллам за соответствующую контрольную работу, но не более максимальной оценки за контрольную работу. Сверх максимальной оценки премия обменивается на баллы по курсу 4:1 - каждые 4 объявленных премиальных балла преобразуются в 1 фактически полученный.

Премиальная задача сдаётся лектору устно - лично или удалённо (созвон). Время беседы обговаривается индивидуально. При подготовке решения можно пользоваться любыми материалами и источниками, при сдаче - только конспектами, книгами, слайдами и другими индивидуально одобренными материалами. Перед беседой приветствуется отправка фотографий решения или ссылок на источники - это позволит сразу перейти к вопросам на понимание написанного и сократит время беседы.

Особые заслуги

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

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

Программа будет обновляться согласно фактически прочитанному материалу

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

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

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

  1. Предварённая нормальная форма. Теорема о предварённой нормальной форме.
  2. Сколемовская стандартная форма. Алгоритм сколемизации предварённой нормальной формы. Теорема о сколемизации.
  3. Дизъюнкты. Сведение проблемы общезначимости формул к проблеме невыполнимости систем дизъюнктов.
  4. Подстановки. Композиция подстановок. Унификатор. Наиболее общий унификатор. Задача унификации выражений логики предикатов.
  5. Лемма о связке. Алгоритм унификации. Теорема об унификации.
  6. Правило резолюции. Правило склейки. Резолютивный вывод. Теорема о корректности резолютивного вывода.
  7. Эрбрановский универсум. Эрбрановский базис. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях. Теорема Эрбрана.
  8. Лемма об основных дизъюнктах. Лемма о подъёме. Теорема о полноте резолютивного вывода.
  9. Метод резолюций: общая схема, применение.

Логические исчисления

  1. Логические исчисления. Исчисления высказываний и исчисления предикатов. Выводимость и доказуемость формул.
  2. Натуральное исчисление высказываний. Правило монотонности. Закон исключённого третьего. Правило сечения. Правило полного перебора. Правило приведения к абсурду. Корректность и полнота исчисления.
  3. Натуральное исчисление предикатов. Корректность и полнота исчисления.
  4. Исчисление предикатов гильбертовского типа. Теорема Гёделя о полноте (формулировка).

Аксиоматические теории

  1. Аксиоматические теории первого порядка: основные определения, проблема общезначимости формул в теории.
  2. Основные свойства аксиоматических теорий: непротиворечивость, элементарность, полнота, разрешимость.
  3. Определения и выразимость в интерпретациях. Теорема о подстановке определения.
  4. Формальная арифметика. Теорема Гёделя о неполноте (формулировка и схема доказательства).
  5. Арифметика Пресбургера, её разрешимость и выразительность.

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

  1. Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики. Логика линейного времени. Логика деревьев вычислений.
  2. Интуиционистская логика.
  3. Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Полная и частичная корректность программ. Тройки Хоара. Логика Хоара. Корректность вывода в логике Хоара. Слабейшее предусловие. Инвариант цикла.
  4. Размеченные системы переходов. Моделирование программ системами переходов. Логика деревьев вычислений (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 с.
Источник — «https://mk.cs.msu.ru/index.php?title=Математическая_логика_(318,_319/2,_241,_242)&oldid=12505»