Математическая логика (318, 319/2, 241, 242) — различия между версиями

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
 
(не показана 51 промежуточная версия 2 участников)
Строка 1: Строка 1:
 +
[[Категория:Лекционные курсы кафедры МК]]
 +
 +
Актуальность информации: весенний семестр 2023/2024 учебного года.
 +
 
Обязательный курс для студентов групп 318 и 319/2, ''а также 241 и 242 (Математическая логика и теория алгоритмов)''. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].
 
Обязательный курс для студентов групп 318 и 319/2, ''а также 241 и 242 (Математическая логика и теория алгоритмов)''. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].
  
Актуальность информации: весенний семестр 2020/2021 учебного года.
+
= Слайды лекций =
  
<!--
+
[[Media: Mathlog_318_b1.pdf|Блок 1]] (вводный). Что такое логика. Несколько логических парадоксов. Чего ожидать в курсе.
'''Объявления'''
+
  
''В этом разделе будут выкладываться объявления об изменениях на странице курса''
+
[[Media: Mathlog_318_b2.pdf|Блок 2]]. Логика высказываний: синтаксис, семантика.
  
* 2021.02.04 16:00 Страница курса подготовлена к весеннему семестру 2020/2021 учебного года
+
[[Media: Mathlog_318_b3.pdf|Блок 3]]. Логика предикатов: синтаксис, семантика.
-->
+
  
= Слайды лекций =
+
[[Media: Mathlog_318_b4.pdf|Блок 4]]. Как формализовать предложение на языке логики предикатов (пример).
  
''Слайды будут выкладываться по мере проведения занятий''
+
[[Media: Mathlog_318_b5.pdf|Блок 5]]. Логика высказываний: выполнимые и общезначимые формулы.
  
'''[[Media: Mathlog_318_b1.pdf|Блок 1]]''' (вводный). Что такое логика. Содержание лекций. Несколько логических парадоксов.
+
[[Media: Mathlog_318_b6.pdf|Блок 6]]. Логика предикатов: выполнимые и общезначимые формулы; модели формул; логическое следствие; проблема общезначимости формул (постановка).
  
'''[[Media: Mathlog_318_b2.pdf|Блок 2]]'''. Логика высказываний: синтаксис, семантика, выполнимость, общезначимость.
+
[[Media: Mathlog_318_b7.pdf|Блок 7]]. Логика предикатов: можно ли проверить общезначимость формулы "в лоб"?
  
'''[[Media: Mathlog_318_b3.pdf|Блок 3]]'''. Логика предикатов: синтаксис, семантика.
+
[[Media: Mathlog_318_b8.pdf|Блок 8]]. Метод семантических таблиц: семантические таблицы.
  
'''[[Media: Mathlog_318_b4.pdf|Блок 4]]'''. Как формализовать предложение на языке логики предикатов (пример).
+
[[Media: Mathlog_318_b9.pdf|Блок 9]]. Подстановки (основные определения).
  
'''[[Media: Mathlog_318_b5.pdf|Блок 5]]'''. Логика предикатов: выполнимые и общезначимые формулы; модели формул; логическое следствие; проблема общезначимости формул (постановка).
+
[[Media: Mathlog_318_b10.pdf|Блок 10]]. Метод семантических таблиц: табличный вывод.
  
'''[[Media: Mathlog_318_b6.pdf|Блок 6]]'''. Логика предикатов: почему бы не проверять общезначимость формул "в лоб"?
+
[[Media: Mathlog_318_b11.pdf|Блок 11]]. Метод семантических таблиц: корректность табличного вывода.
  
'''[[Media: Mathlog_318_b7.pdf|Блок 7]]'''. Метод семантических таблиц в логике высказываний.
+
[[Media: Mathlog_318_b12.pdf|Блок 12]]. Метод семантических таблиц: полнота табличного вывода.
  
'''[[Media: Mathlog_318_b8.pdf|Блок 8]]'''. Метод семантических таблиц в логике предикатов: семантические таблицы.
+
[[Media: Mathlog_318_b13.pdf|Блок 13]]. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Автоматизация доказательства теорем.
  
'''[[Media: Mathlog_318_b9.pdf|Блок 9]]'''. Подстановки (основные определения).
+
[[Media: Mathlog_318_b14.pdf|Блок 14]]. Общая схема метода резолюций.
  
'''[[Media: Mathlog_318_b10.pdf|Блок 10]]'''. Метод семантических таблиц в логике предикатов: табличный вывод.
+
[[Media: Mathlog_318_b15.pdf|Блок 15]]. Равносильность формул.
  
'''[[Media: Mathlog_318_b11.pdf|Блок 11]]'''. Метод семантических таблиц в логике предикатов: корректность табличного вывода.
+
[[Media: Mathlog_318_b16.pdf|Блок 16]]. Предварённая нормальная форма (ПНФ).
  
'''[[Media: Mathlog_318_b12.pdf|Блок 12]]'''. Метод семантических таблиц в логике предикатов: полнота табличного вывода.
+
[[Media: Mathlog_318_b17.pdf|Блок 17]]. Сколемовская стандартная форма (ССФ).
  
'''[[Media: Mathlog_318_b13.pdf|Блок 13]]'''. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Автоматизация доказательства теорем.
+
[[Media: Mathlog_318_b18.pdf|Блок 18]]. Системы дизъюнктов.
  
'''[[Media: Mathlog_318_b14.pdf|Блок 14]]'''. Общая схема метода резолюций.
+
[[Media: Mathlog_318_b19.pdf|Блок 19]]. Композиция подстановок. Постановка задачи унификации.
  
'''[[Media: Mathlog_318_b15.pdf|Блок 15]]'''. Равносильность формул логики предикатов.
+
[[Media: Mathlog_318_b20.pdf|Блок 20]]. Алгоритм унификации атомарных формул.
  
'''[[Media: Mathlog_318_b16.pdf|Блок 16]]'''. Предварённая нормальная форма (ПНФ).
+
[[Media: Mathlog_318_b21.pdf|Блок 21]]. Монотонность и транзитивность отношения логического следования.
  
'''[[Media: Mathlog_318_b17.pdf|Блок 17]]'''. Сколемовская стандартная форма (ССФ).
+
[[Media: Mathlog_318_b22.pdf|Блок 22]]. Резолютивный вывод. Корректность резолютивного вывода.
  
'''[[Media: Mathlog_318_b18.pdf|Блок 18]]'''. Системы дизъюнктов.
+
[[Media: Mathlog_318_b23.pdf|Блок 23]]. Обоснование общезначимости формулы методом резолюций (пример).
  
'''[[Media: Mathlog_318_b19.pdf|Блок 19]]'''. Композиция подстановок. Постановка задачи унификации.
+
[[Media: Mathlog_318_b24.pdf|Блок 24]]. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях.
  
'''[[Media: Mathlog_318_b20.pdf|Блок 20]]'''. Алгоритм унификации атомарных формул логики предикатов.
+
[[Media: Mathlog_318_b25.pdf|Блок 25]]. Теорема Эрбрана. Полнота резолютивного вывода.
  
'''[[Media: Mathlog_318_b21.pdf|Блок 21]]'''. Резолютивный вывод. Корректность резолютивного вывода.
+
[[Media: Mathlog_318_b26.pdf|Блок 26]]. Даша, Саша, Паша, пиво и метод семантических таблиц с методом резолюций.
  
'''[[Media: Mathlog_318_b22.pdf|Блок 22]]'''. Обоснование общезначимости формулы методом резолюций (пример).
+
[[Media: Mathlog_318_b27.pdf|Блок 27]]. Как устроены математические доказательства. Логические исчисления.
  
'''[[Media: Mathlog_318_b23.pdf|Блок 23]]'''. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях.
+
[[Media: Mathlog_318_b28.pdf|Блок 28]]. Натуральное исчисление высказываний: основные определения.
  
'''[[Media: Mathlog_318_b24.pdf|Блок 24]]'''. Теорема Эрбрана. Полнота резолютивного вывода.
+
[[Media: Mathlog_318_b29.pdf|Блок 29]]. Натуральное исчисление высказываний: правило монотонности, закон исключённого третьего, корректность.
  
'''[[Media: Mathlog_318_b25.pdf|Блок 25]]'''. Метод резолюций: заключительный пример.
+
[[Media: Mathlog_318_b30.pdf|Блок 30]]. Натуральное исчисление высказываний: правило сечения, правило полного перебора, правило приведения к абсурду, полнота.
  
'''[[Media: Mathlog_318_b26.pdf|Блок 26]]'''. Как устроены математические доказательства. Логические исчисления.
+
[[Media: Mathlog_318_b31.pdf|Блок 31]]. Натуральное исчисление предикатов: основные определения, корректность.
  
'''[[Media: Mathlog_318_b27.pdf|Блок 27]]'''. Натуральное исчисление высказываний: основные определения.
+
[[Media: Mathlog_318_b32.pdf|Блок 32]]. Гильбертовское исчисление предикатов. Теорема Гёделя о полноте (формулировка).
  
'''[[Media: Mathlog_318_b28.pdf|Блок 28]]'''. Натуральное исчисление высказываний: правило монотонности, закон исключённого третьего, корректность.
+
''Слайды будут появляться по мере чтения лекций.''
  
'''[[Media: Mathlog_318_b29.pdf|Блок 29]]'''. Натуральное исчисление высказываний: правило сечения, правило полного перебора, правило приведения к абсурду, полнота.
+
== Прошлогодние слайды ==
  
'''[[Media: Mathlog_318_b30.pdf|Блок 30]]'''. Натуральное исчисление предикатов: основные определения, корректность.
+
[[Media: Mathlog_318_b33.pdf|Блок 33]]. Натуральное исчисление предикатов: полнота.
  
'''[[Media: Mathlog_318_b31.pdf|Блок 31]]'''. Гильбертовское исчисление предикатов. Теорема Гёделя о полноте (формулировка).
+
[[Media: Mathlog_318_b34.pdf|Блок 34]]. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.
  
'''[[Media: Mathlog_318_b32.pdf|Блок 32]]'''. Натуральное исчисление предикатов: полнота.
+
[[Media: Mathlog_318_b35.pdf|Блок 35]]. Машины Тьюринга (МТ).
  
'''[[Media: Mathlog_318_b33.pdf|Блок 33]]'''. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.
+
[[Media: Mathlog_318_b36.pdf|Блок 36]]. Теорема Чёрча.
  
'''[[Media: Mathlog_318_b34.pdf|Блок 34]]'''. Машины Тьюринга (МТ). Проблема останова МТ.
+
[[Media: Mathlog_318_b37.pdf|Блок 37]]. Аксиоматические теории первого порядка. Проблема общезначимости формул в теории.
  
'''[[Media: Mathlog_318_b35.pdf|Блок 35]]'''. Теорема Чёрча.
+
[[Media: Mathlog_318_b38.pdf|Блок 38]]. Основные свойства аксиоматических теорий.
  
'''[[Media: Mathlog_318_b36.pdf|Блок 36]]'''. Аксиоматические теории первого порядка. Проблема общезначимости формул в теории.
+
[[Media: Mathlog_318_b39.pdf|Блок 39]]. Арифметические интерпретации и теории.
  
'''[[Media: Mathlog_318_b37.pdf|Блок 37]]'''. Основные свойства аксиоматических теорий.
+
[[Media: Mathlog_318_b40.pdf|Блок 40]]. Определения и выразимость.
  
'''[[Media: Mathlog_318_b38.pdf|Блок 38]]'''. Арифметические интерпретации и теории.
+
[[Media: Mathlog_318_b41.pdf|Блок 41]]. Формальная арифметика. Теорема Гёделя о неполноте.
  
'''[[Media: Mathlog_318_b39.pdf|Блок 39]]'''. Определения и выразимость.
+
[[Media: Mathlog_318_b42.pdf|Блок 42]]. Арифметика Пресбургера.
  
'''[[Media: Mathlog_318_b40.pdf|Блок 40]]'''. Формальная арифметика. Теорема Гёделя о неполноте.
+
[[Media: Mathlog_318_b43.pdf|Блок 43]]. Модальные логики.
  
'''[[Media: Mathlog_318_b41.pdf|Блок 41]]'''. Арифметика Пресбургера.
+
[[Media: Mathlog_318_b44.pdf|Блок 44]]. Эпистемические логики.
  
'''[[Media: Mathlog_318_b42.pdf|Блок 42]]'''. Модальные логики.
+
[[Media: Mathlog_318_b45.pdf|Блок 45]]. Темпоральные логики.
  
'''[[Media: Mathlog_318_b43.pdf|Блок 43]]'''. Эпистемические логики.
+
[[Media: Mathlog_318_b46.pdf|Блок 46]]. Интуиционистская логика.
  
'''[[Media: Mathlog_318_b44.pdf|Блок 44]]'''. Темпоральные логики.
+
[[Media: Mathlog_318_b47.pdf|Блок 47]]. Формальная верификация.
  
== Слайды прошлых лет ==
+
[[Media: Mathlog_318_b48.pdf|Блок 48]]. Модельные императивные программы. Постановка задачи верификации программ.
  
'''[[Media: Mathlog_318_lecture_1.pdf|Лекция]]''' (вводная). Что такое логика? Содержание лекций. История логики. Логические парадоксы.
+
[[Media: Mathlog_318_b49.pdf|Блок 49]]. Логика Хоара. Автоматизация проверки правильности программ.
  
'''[[Media: Mathlog_318_lecture_2.pdf|Лекция.]]''' Логика высказываний: синтаксис, семантика, выполнимость, общезначимость. Метод семантических таблиц в логике высказываний.
+
[[Media: Mathlog_318_b50.pdf|Блок 50]]. Проверка правильности распределённых систем. Пара слов о методе model checking.
  
'''[[Media: Mathlog_318_lecture_3.pdf|Лекция.]]''' Логика предикатов: синтаксис (термы, формулы), семантика (интерпретации, отношение выполнимости).
+
[[Media: Mathlog_318_b51.pdf|Блок 51]]. Размеченные системы переходов.
  
'''[[Media: Mathlog_318_lecture_4_5.pdf|Лекция.]]''' Выполнимые и общезначимые формулы. Модели. Логическое следствие. Проблема общезначимости формул. Подстановки. Метод семантических таблиц в логике предикатов. Корректность табличного вывода.
+
[[Media: Mathlog_318_b52.pdf|Блок 52]]. Спецификация систем при помощи темпоральных логик.
  
'''[[Media: Mathlog_318_lecture_6.pdf|Лекция.]]''' Полнота табличного вывода в логике предикатов. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Равносильные формулы. Теорема о равносильной замене.
+
[[Media: Mathlog_318_b53.pdf|Блок 53]]. Алгоритм model checking для CTL.
  
'''[[Media: Mathlog_318_lecture_7.pdf|Лекция.]]''' Общая схема метода резолюций. Предварённая нормальная форма. Сколемовская стандартная форма. Системы дизъюнктов. Задача унификации.
+
= Семинары =
  
'''[[Media: Mathlog_318_lecture_8.pdf|Лекция.]]''' Алгоритм унификации атомарных формул. Теорема об унификации.
+
''Материалы семинаров будут обновляться по мере проведения занятий''
  
'''[[Media: Mathlog_318_lecture_9.pdf|Лекция.]]''' Резолютивный вывод. Корректность резолютивного вывода. Применение метода резолюций. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях. Теорема Эрбрана.
+
Семинары 1-4 проводятся по [[Media:MatLog_tasks.pdf| этому сборнику задач.]]
  
'''[[Media: Mathlog_318_lecture_10.pdf|Лекция.]]''' Полнота резолютивного вывода. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.
+
Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]]
  
'''[[Media: Mathlog_318_lecture_11.pdf|Лекция.]]''' Машины Тьюринга. Теорема Чёрча. Как устроены математические доказательства. Логические исчисления.
+
[[Media:Mathlog_318_seminar_natural_inference.pdf| Материалы семинара 5-6 (натуральное исчисление).]]
  
'''[[Media: Mathlog_318_lecture_12_13.pdf|Лекция.]]''' Натуральное исчисление высказываний. Натуральное исчисление предикатов. Исчисление предикатов гильбертовского типа.
+
= Контрольные работы =
  
'''[[Media: Mathlog_318_lecture_14.pdf|Лекция.]]''' Модальные логики. Эпистемические логики. Темпоральные логики.
+
Контрольные работы проводятся письменно, длительность каждой - 90 минут.
  
'''[[Media: Mathlog_318_lecture_15.pdf|Лекция.]]''' Формальная верификация программ. Императивные программы. Корректность императивных программ. Логика Хоара. Автоматизация проверки правильности программ.
+
В контрольных работах встретятся 4 типовые задачи со следующими темами:
 +
# Формализовать в логике предикатов предложение, записанное на естественном языке.
 +
# Обосновать общезначимость формулы логики предикатов методом семантических таблиц.
 +
# Обосновать общезначимость формулы логики предикатов методом резолюций.
 +
# Доказать формулу в натуральном исчислении предикатов.
  
'''[[Media: Mathlog_318_lecture_16.pdf|Лекция.]]''' Верификация распределённых систем. Логика линейного времени (LTL). Размеченные системы переходов. Задача верификации (model checking) для LTL.
+
Оценка решений типовых задач:
 +
* Максимальная оценка - 4 балла.
 +
* Если решение в целом верно, но содержит редкие ошибки серьёзнее опечаток, то оно оценивается в 3 балла.
 +
* Если решение содержит серьёзные ошибки, но имеет структуру, в целом разумно соотносящуюся с правильной, то задача оценивается в 2 балла.
 +
* Если в решении обнаружены правильные элементы, в заметном, но всё же малом количестве, то задача оценивается в 1 балл.
  
'''[[Media: Mathlog_318_lecture_17.pdf|Лекция.]]''' Табличный алгоритм верификации для LTL. Замыкание Фишера-Ладнера. Системы Хинтикки.
+
Теоретические вопросы даются в форме теста с множественным выбором: из предложенных вариантов ответа требуется выбрать правильные (один, несколько или ни одного), обоснование не требуется.
 +
Правильно решённый теоретический вопрос оценивается в 1 балл.
  
'''[[Media: Mathlog_318_lecture_11_12.pdf|Лекция.]]''' Аксиоматические теории. Основные свойства теорий. Формальная арифметика. Арифметика Пеано. Теорема Гёделя о неполноте. Определимость. Арифметика Пресбургера.
+
'''Первая контрольная работа''' будет содержать
 +
* 3 типовые задачи по темам 1-3 и
 +
* 9 теоретических вопросов по прочитанным лекциям.
  
'''[[Media: Mathlog_318_lecture_16_17.pdf|Лекция.]]'''.
+
'''Вторая контрольная работа''' будет содержать
 +
* 4 типовые задачи по всем темам и
 +
* 5 теоретических вопросов по лекциям, не попавшим в первую контрольную работу.
  
= Семинары =
+
'''Остальные контрольные работы''' будут содержать
 +
* 4 типовые задачи по всем темам и
 +
* 14 теоретических вопросов по всем лекциям.
  
''Материалы семинаров будут обновляться по мере проведения занятий''
+
= Зачёт =
  
Семинары 1-4 проводятся по [[Media:MatLog_tasks.pdf| этому сборнику задач.]]
+
На зачёте оцениваются результаты, относящиеся к решению типовых задач, знанию теории и работе в семестре.
 +
При проставлении зачёта учитывается 6 технических оценок:
 +
* Четыре оценки за типовые задачи, по одной за каждую задачу.
 +
* Оценка за знание теории. Максимум - 14 баллов.
 +
* Оценка за решение премиальных задач.
  
Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]]
+
Для получения зачёта требуется получить два результата:
 +
# Набрать хотя бы 11 баллов за типовые задачи.
 +
# Набрать хотя бы 20 баллов суммарно за всё (типовые задачи, теория, премиальные задачи).
  
[[Media:Mathlog_318_seminar_natural_inference.pdf| Материалы семинара 5 (натуральное исчисление).]]
+
Баллы за типовые задачи и за теорию набираются на [[#Контрольные работы|контрольных работах]].
  
[[Media:Mllp_318_seminar_definability.pdf| Материалы семинара 6 (выразимость).]]
+
Для решения каждой типовой задачи будет предложено несколько попыток.
 +
При проставлении зачёта учитывается '''максимальная''' оценка за задачу среди всех попыток её решить.
 +
 
 +
При проставлении зачёта учитывается '''максимальная''' оценка за теорию среди полученных
 +
* суммарно за первые две контрольные работы и
 +
* за каждую из следующих контрольных работ.
  
 
= Экзамен =
 
= Экзамен =
Строка 155: Строка 183:
 
Формат проведения и длительность экзамена: письменно, 120 минут.
 
Формат проведения и длительность экзамена: письменно, 120 минут.
  
Экзаменационная работа оценивается по шкале от 0 до 33 технических баллов.
+
Экзаменационная работа содержит 10 задач и оценивается по шкале от 0 до 37 технических баллов.
К оценке за эту работу прибавляются технические баллы, полученные за работу в семестре (выполнение премиальных задач).
+
К этим техническим баллам прибавляются баллы за выполнение премиальных задач и поощрение/штраф за [[#Контрольная работа|контрольную работу]].
 
Согласно набранной сумме технических баллов выставляется оценка:
 
Согласно набранной сумме технических баллов выставляется оценка:
* хотя бы 27: '''отлично''';
+
* хотя бы 30: '''отлично''';
* хотя бы 21, но менее 27: '''хорошо''';
+
* хотя бы 23, но менее 30: '''хорошо''';
* хотя бы 15, но менее 21: '''удовлетворительно''';
+
* хотя бы 16, но менее 23: '''удовлетворительно''';
* менее 15: '''неудовлетворительно'''.
+
* менее 16: '''неудовлетворительно'''.
  
 
Баллы за экзаменационную работу складываются из баллов за каждую задачу, предложенную в работе:
 
Баллы за экзаменационную работу складываются из баллов за каждую задачу, предложенную в работе:
* Каждая из задач 1-5 оценивается в 3 балла. Темы задач:
+
* Каждая из задач 1-4 оценивается в 4 балла. Темы задач:
 
*# Формализовать в логике предикатов предложение, записанное на естественном языке.
 
*# Формализовать в логике предикатов предложение, записанное на естественном языке.
*# Проверить общезначимость формулы логики предикатов методом семантических таблиц.
+
*# Обосновать общезначимость формулы логики предикатов методом семантических таблиц.
*# Проверить общезначимость формулы логики предикатов методом резолюций.
+
*# Обосновать общезначимость формулы логики предикатов методом резолюций.
*# ''По теме логических исчислений, точная формулировка определится позже''.
+
*# Доказать формулу в натуральном исчислении предикатов.
*# ''По теме аксиоматических теорий, точная формулировка определится позже''.
+
* Каждая из задач 5-7 оценивается в 3 балла и состоит из трёх частей:
* Каждая из задач 6-8 оценивается в 2 балла и состоит из двух частей:
+
 
*# Сформулировать утверждение, определение и т.п.
 
*# Сформулировать утверждение, определение и т.п.
 
*# Ответить на вопрос "на понимание", так или иначе связанный с формулировкой.
 
*# Ответить на вопрос "на понимание", так или иначе связанный с формулировкой.
* Каждая из задач 9-12 оценивается в 3 балла и устроена так:
+
*# Аргументировать (обосновать) ответ на вопрос.
 +
* Каждая из задач 8-10 оценивается в 4 балла и устроена так:
 
** Из нескольких предложенных вариантов ответа выбрать правильные (один, несколько или ни одного) и '''обосновать''' выбранные ответы.
 
** Из нескольких предложенных вариантов ответа выбрать правильные (один, несколько или ни одного) и '''обосновать''' выбранные ответы.
 
** Невыбранные ответы обосновывать не нужно.
 
** Невыбранные ответы обосновывать не нужно.
  
= Зачёт =
+
== Контрольная работа ==
  
На зачёте оцениваются результаты, относящиеся к решению типовых задач, знанию теории и работе в семестре.
+
На оценку за экзамен влияет первая [[#Контрольные работы|контрольная работа]].
 
+
Максимальная техническая оценка за эту работу - 21 балл.
В курсе встретится 5 типовых задач:
+
В зависимости от технических баллов, набранных за первую контрольную работу, определяется поощрение или штраф к техническим баллам за экзамен:
# Формализовать в логике предикатов предложение, записанное на естественном языке.
+
* Набрано хотя бы 19 баллов: бонус <span style="background:#DDFFDD">+3 балла</span>;
# Проверить общезначимость формулы логики предикатов методом семантических таблиц.
+
* Набрано хотя бы 16, но менее 19 баллов: бонус <span style="background:#DDFFDD">+2 балла</span>;
# Проверить общезначимость формулы логики предикатов методом резолюций.
+
* Набрано хотя бы 13, но менее 16 баллов: бонус <span style="background:#DDFFDD">+1 балл</span>;
# ''По теме логических исчислений, точная формулировка определится позже''.
+
* Набрано хотя бы 10, но менее 13 баллов: <span style="background:#CCCCCC">0 баллов</span>;
# ''По теме аксиоматических теорий, точная формулировка определится позже''.
+
* Набрано хотя бы 7, но менее 10 баллов: штраф <span style="background:#FFDDDD">-1 балл</span>;
 
+
* Набрано хотя бы 4, но менее 7 баллов: штраф <span style="background:#FFDDDD">-2 балла</span>;
При проставлении зачёта учитывается 7 технических оценок:
+
* Набрано менее 4 баллов: штраф <span style="background:#FFDDDD">-3 балла</span>;
* Пять оценок за типовые задачи, по одной за каждую задачу. Максимальная оценка за каждую задачу - 3 балла.
+
* Неявка без уважительной причины: штраф <span style="background:#FFDDDD">-3 балла</span>;
* Оценка за знание теории. Максимум - 15 баллов.
+
* Неявка по уважительной причине: <span style="background:#CCCCCC">0 баллов</span>.
* Оценка за решение премиальных задач.
+
 
+
Для получения зачёта требуется достичь следующих результатов:
+
# Хорошо решить типовые задачи:
+
#* четыре задачи не менее чем на 2 балла, или
+
#* две задачи на 3 балла и одну задачу на не менее чем 2 балла.
+
#** "3 балла" = "правильно"
+
#** "не менее чем 2 балла" = "правильно или с незначительными недочётами"
+
# Набрать хотя бы 20 баллов суммарно за всё (типовые задачи, теория, премиальные задачи).
+
 
+
В курсе планируются две контрольные работы: первая - в середине семестра, вторая - после завершения лекций.
+
Контрольные работы и попытки зачёта проводятся письменно, длительность каждого мероприятия - 90 минут (одна пара).
+
 
+
== Сдача типовых задач ==
+
 
+
Для решения каждой типовой задачи будет предложено несколько попыток.
+
При проставлении зачёта учитывается '''максимальная''' оценка за задачу среди всех попыток её решить.
+
 
+
На первой контрольной работе будут предложены типовые задачи 1-3.
+
На второй контрольной работе и на каждой попытке зачёта будут предложены все типовые задачи.
+
 
+
== Сдача теории ==
+
 
+
Теоретические вопросы даются в форме теста с множественным выбором: из предложенных вариантов ответа требуется выбрать правильные (один, несколько или ни одного), обоснование не требуется.
+
Правильно решённый теоретический вопрос оценивается в 1 балл.
+
 
+
На первой контрольной работе будет предложено 9 теоретических вопросов.
+
На второй контрольной работе будет предложено 6 теоретических вопросов.
+
Оценка за знание теории складывается из оценок за эти 15 теоретических вопросов.
+
 
+
На каждой попытке зачёта также будет предложено 15 теоретических вопросов.
+
При проставлении зачёта учитывается '''максимальная''' оценка среди полученных за контрольные работы и за каждую из попыток зачёта.
+
  
 
= Премиальные задачи =
 
= Премиальные задачи =
 
''По ходу проведения курса в подразделах этого раздела будут появляться премиальные задачи''
 
  
 
Общие условия сдачи решений премиальных задач:
 
Общие условия сдачи решений премиальных задач:
* Можно как прислать письменное решение, так и обсудить решение устно. Если прислано письменное решение и к нему есть вопросы, то для их решения может потребоваться дополнительное устное обсуждение.  
+
* Можно как прислать письменное решение, так и обсудить решение устно. Если прислано письменное решение и к нему есть вопросы, то для ответов на эти вопросы может потребоваться дополнительное устное обсуждение.  
 
* При подготовке решения и во время его сдачи можно пользоваться любыми материалами.
 
* При подготовке решения и во время его сдачи можно пользоваться любыми материалами.
 
* При сдаче может быть проверено понимание '''каждой''' детали предложенного решения - следует быть к этому готовым.
 
* При сдаче может быть проверено понимание '''каждой''' детали предложенного решения - следует быть к этому готовым.
 
* Решение принимается, когда по нему не остаётся неотвеченных вопросов.
 
* Решение принимается, когда по нему не остаётся неотвеченных вопросов.
  
'''Бонусы за решение задач сформулированы для одной учебной группы''' и получаются внутри одной группы независимо от другой.
+
'''Бонусы за решение задач формулируются для одной учебной группы''' и распределяются внутри одной группы независимо от другой.
Например, "''первый''" трактуется как "''первый из группы 318, а также первый из группы 319/2, а также ...''".
+
Например, "''первый''" трактуется как "''первый в группе 318, а также первый в группе 319/2, а также ...''".
 
+
== (1) Свойства семантических таблиц в логике высказываний ==
+
 
+
Доказать три утверждения в блоке 7, доказательство которых помечено словами "А попробуйте сами", '''или''' два утверждения в блоке 8, помеченные теми же словами.
+
 
+
Бонус за решение задачи: <span style="background:#DDFFDD">+1 балл</span> первым '''двум''' предоставившим решение задачи
+
 
+
== (2) Полнота табличного вывода в логике предикатов ==
+
 
+
Адаптировать доказательство теоремы о полноте табличного вывода в логике предикатов к более общему случаю:
+
* сигнатура алфавита состоит из
+
** не более чем счётного числа констант,
+
** не более чем счётного числа функциональных символов произвольных местностей,
+
** не более чем счётного числа предикатных символов произвольных местностей;
+
* формулы исходной таблицы могут содержать свободные переменные;
+
* исходная таблица содержит не более чем счётное число формул.
+
 
+
Бонусы за решение задачи:
+
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
+
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
+
 
+
== (3) Утверждения об отношении равносильности ==
+
 
+
Обосновать два утверждения об отношении равносильности в блоке 15, помеченные словами "Попробуйте самостоятельно" рядом со словом "Доказательство".
+
 
+
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение задачи
+
 
+
== (4) Сколемизация ==
+
 
+
Обосновать или опровергнуть
+
* необходимость ("=>") и
+
* достаточность ("<=")
+
теоремы о сколемизации, в которой свойство выполнимости заменено на свойство общезначимости (как сказано в вопросе под теоремой).
+
 
+
Бонус за решение задачи:
+
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
+
* '''второй''' сдавший: <span style="background:#DDFFDD">+2 балла</span>
+
 
+
== (5) Первая головоломка о мощностях интерпретаций ==
+
 
+
Придумать (с обоснованием) необщезначимое предложение, истинное в любой интерпретации, содержащей не более чем 4 предмета.
+
 
+
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение задачи
+
 
+
== (6) Вторая головоломка о мощностях интерпретаций ==
+
 
+
Доказать, что если предложение истинно в любой интерпретации, содержащей не менее чем 4 предмета, то оно общезначимо.
+
 
+
Бонусы за решение задачи:
+
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
+
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
+
 
+
== (7) Фундированность троек чисел ==
+
 
+
Доказать фундированность троек неотрицательных целых чисел относительно лексикографического порядка (лемма в блоке 20, обоснование которой помечено словами "Попробуйте сами").
+
 
+
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение задачи
+
 
+
== (8) Про эрбрановские интерпретации ==
+
 
+
Останется ли справедливой теорема об эрбрановских интерпретациях, если вместо "Система дизъюнктов" в её формулировке написать "Формула логики предикатов"?
+
Ответ обосновать.
+
 
+
Бонус за решение задачи:
+
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
+
* '''второй''' сдавший: <span style="background:#DDFFDD">+2 балла</span>
+
 
+
== (9) Полная стратегия построения успешного резолютивного вывода ==
+
 
+
Предложить (с обоснованием) список правил построения резолютивного вывода, гарантирующих получение пустого дизъюнкта из конечной невыполнимой системы дизъюнктов.
+
 
+
(Как это делалось, например, в доказательстве теоремы о полноте табличного вывода.)
+
 
+
Бонусы за решение задачи:
+
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
+
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
+
 
+
== (10) Вычислительные возможности метода резолюций ==
+
 
+
Ответить (с обоснованием и для достаточно широкого семейства резолютивных выводов) на вопрос, поставленный в конце "заключительного примера для метода резолюций" блока 25.
+
 
+
Бонусы за решение задачи:
+
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
+
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
+
 
+
== (11) Исчисление семантических таблиц ==
+
 
+
Определить (с пояснениями) аксиомы и правила вывода логического исчисления со следующими свойствами:
+
* формулы исчисления - семантические таблицы логики предикатов;
+
* таблица доказуема в исчислении тогда и только тогда, когда для неё существует успешный табличный вывод;
+
* из доказательства для таблицы T в исчислении можно получить успешный табличный вывод для T, расположив таблицы в вершинах дерева согласно применению правил исчисления.
+
 
+
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение задачи
+
 
+
== (12) Корректность натурального исчисления предикатов ==
+
 
+
Выбрать одно из четырёх правил вывода НИП для кванторов (введение/удаление существования/всеобщности) и обосновать корректность этого правила согласно разобранному в доказательстве теоремы о корректности НИВ.
+
 
+
Для каждого из правил принимается только одно решение, и от одного студента принимается решение только для одного правила.
+
Бонус за решение: <span style="background:#DDFFDD">+1 балл</span>
+
 
+
== (13) Теорема Гёделя о полноте ==
+
 
+
Доказать теорему Гёделя о полноте, сформулированную в блоке 31, для исчисления, изложенного в этом же блоке.
+
 
+
Бонусы за решение задачи:
+
* '''первый''' сдавший: <span style="background:#DDFFDD">+10 баллов</span>
+
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+7 баллов</span>
+
 
+
== (14) Непротиворечивая конечная полная теория ==
+
 
+
Привести пример (с обоснованием) непротиворечивой конечной полной аксиоматической теории первого порядка.
+
 
+
Бонус за решение задачи:
+
* '''первый''' сдавший: <span style="background:#DDFFDD">+2 балла</span>
+
* '''второй''' сдавший: <span style="background:#DDFFDD">+1 балл</span>
+
 
+
== (15) О подстановке определения ==
+
 
+
Оформить пропущенные части доказательства теоремы о подстановке определения: доказательство для функции кси и часть доказательства, скрытая в отсылке к теореме о равносильной замене.
+
 
+
Бонус за решение задачи:
+
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
+
* '''второй''' сдавший: <span style="background:#DDFFDD">+2 балла</span>
+
 
+
== (16) Теорема Гёделя о неполноте ==
+
 
+
Доказать теорему Гёделя о неполноте в формулировке, представленной в блоке 40: либо адаптировать представленный там эскиз доказательства к общему случаю и доказать леммы об арифметизации и о диагонали, либо предоставить независимое доказательство.
+
 
+
Бонусы за решение задачи:
+
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+14 баллов</span>
+
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+11 баллов</span>
+
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+8 баллов</span>
+
 
+
== (17) Арифметика Пресбургера ==
+
 
+
Доказать полноту системы аксиом арифметики Пресбургера, представленной на последнем слайде блока 41.
+
 
+
Бонусы за решение задачи:
+
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+4 балла</span>
+
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+3 балла</span>
+
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+2 балл</span>
+
 
+
== (18) Определение экспоненты ==
+
 
+
Предложить (с обоснованием) определение одноместной функции 2^x (два в степени икс) в арифметической интерпретации на целых неотрицательных числах с сигнатурой <{0}, {+, x, s}, {=}> (семинар 5, задача 1, пункт 21).
+
 
+
''Если в обосновании будут содержаться китайская теорема об остатках, малая теорема Ферма или что-либо другое нетривиальное, то обоснование этого - часть решения''
+
 
+
Бонусы за решение задачи:
+
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+4 баллов</span>
+
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+3 балла</span>
+
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+2 балла</span>
+
 
+
== (19) Свойства шкал Крипке ==
+
 
+
Доказать утверждения о рефлексивности, транзитивности и симметричности шкал Крипке, сформулированные в блоке 43.
+
 
+
Бонус за решение задачи:
+
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
+
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
+
 
+
== (20) Задача о трёх мудрецах ==
+
 
+
Записать и пояснить ход рассуждений мудрецов в ''задаче о трёх мудрецах'', представленной в конце блока 43, в терминах эпистемической логики.
+
 
+
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''трём''' предоставившим решение.
+
 
+
<!--
+
 
+
== (11) Корректность логики Хоара ==
+
 
+
Доказать корректность одного из правил логики Хоара ('''лекция 15, лемма о корректности правил'''), кроме правил для пустой команды и для присваивания.
+
 
+
Для каждого из правил принимается только одно решение, и от одного студента принимается решение только для одного правила.
+
Бонус за решение: <span style="background:#DDFFDD">+2 балла</span>
+
 
+
== (12) Слабейшие предусловия ==
+
 
+
Доказать теорему о слабейшем предусловии ('''лекция 15''').
+
 
+
Бонусы за решение задачи:
+
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
+
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
+
 
+
== (13) Законы темпоральных логик ==
+
 
+
В '''лекции 16''' на слайде под заголовком "законы дистрибутивности" выбрать пару строк (1+2, 3+4, 5+6 или 7+8) и доказать либо опровергнуть равносильность в каждой из этих двух строк.
+
 
+
Для каждой пары строк принимается только одно решение, и от одного студента принимается решение только для одной пары строк.
+
Бонус за решение: <span style="background:#DDFFDD">+1 балл</span>
+
 
+
== (14) Табличный алгоритм верификации для LTL ==
+
 
+
Ответить на существенную часть вопросов, сформулированных на последнем слайде последней лекции (17)
+
 
+
Бонус за решение задачи: '''обсуждается индивидуально'''.
+
-->
+
 
+
<!--
+
== Полнота семантической резолюции ==
+
 
+
=== Описание задачи ===
+
 
+
Доказать теорему полноты семантической резолюции (лекция 9).
+
 
+
Бонусы за решение задачи:
+
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+3 балла</span>
+
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+2 балла</span>
+
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+1 балла</span>
+
 
+
=== Количество предоставленных решений ===
+
 
+
'''Группа 318:''' 0
+
 
+
'''Группа 241:''' 0
+
 
+
== Законы темпоральной логики ==
+
 
+
Все пункты задачи относятся к ''законам темпоральной логики'' ('''лекция 17''').
+
 
+
* Выбрать одну пару двойственных левых частей для предполагаемых законов дистрибутивности (1+2, 3+4, 5+6, 7+8), сформулировать правые части, описывающие дистрибутивность операций в естественном понимании, и доказать и/или опровергнуть полученные законы.
+
* Доказать закон неподвижной точки для одного из операторов U, R.
+
* Сформулировать закон, ''не более тривиальный'', чем законы дистрибутивности для темпоральных операторов, и доказать его.
+
 
+
Один сдающий может выбрать только '''один''' закон (или пару законов дистрибутивности), '''не выбранный ранее''' другими сдавшими. <span style="background:#DDFFDD">+1 балл</span> каждому решившему.
+
 
+
''Статистика:''
+
 
+
* решены законы дистрибутивности 1+2, 3+4
+
* один решивший: законы из разных пар, поэтому пары остаются незанятыми
+
 
+
== Model checking для LTL ==
+
 
+
Доказать (додоказать) утверждение, представленное в слайдах '''лекции 18'''.
+
 
+
* Утверждение на слайде 18 (106): однозначное задание согласованных предположений атомарными высказываниями и Next-time-формулами. <span style="background:#DDFFDD">+2 балла</span> каждому решившему.
+
* Обоснование табличного метода model checking, достаточность, индуктивный переход, Until-формула: предложить обоснование для этого случая. <span style="background:#DDFFDD">+3 балла</span> каждому решившему.
+
  
-->
+
Условия задач и статистика принятых решений будут обновляться и доводиться до слушателей по мере чтения курса.
  
 
= Программа курса =
 
= Программа курса =
  
''Программа будет обновляться по ходу чтения курса''
+
''Программа будет обновляться согласно фактически прочитанному материалу''
  
 
== Классические логики ==
 
== Классические логики ==
 
<ol>
 
<ol>
<li> Логика высказываний: синтаксис, семантика; выполнимость, невыполнимость, общезначимость формул. Проблема общезначимости формул логики высказываний.
+
<li> Логика высказываний: синтаксис, семантика; выполнимость и общезначимость формул. Проблема общезначимости формул логики высказываний.
 
<li> Метод семантических таблиц в логике высказываний: семантическая таблица, табличный вывод, теорема о табличном выводе.
 
<li> Метод семантических таблиц в логике высказываний: семантическая таблица, табличный вывод, теорема о табличном выводе.
 
<li> Логика предикатов: синтаксис (термы, формулы, свободные и связанные переменные), семантика (интерпретации, отношение выполнимости).
 
<li> Логика предикатов: синтаксис (термы, формулы, свободные и связанные переменные), семантика (интерпретации, отношение выполнимости).
<li> Выполнимость, общезначимость и противоречивость формул логики предикатов. Модели. Логическое следование. Теорема о логическом следствии. Проблема общезначимости формул логики предикатов.
+
<li> Выполнимость и общезначимость формул логики предикатов. Модели. Логическое следование. Теорема о логическом следствии. Проблема общезначимости формул логики предикатов.
 
<li> Пример выполнимой формулы логики предикатов, не имеющей конечных моделей.
 
<li> Пример выполнимой формулы логики предикатов, не имеющей конечных моделей.
 
<li> Метод семантических таблиц в логике предикатов: семантическая таблица, табличный вывод, теорема о табличной проверке общезначимости, теоремы о корректности и полноте табличного вывода.
 
<li> Метод семантических таблиц в логике предикатов: семантическая таблица, табличный вывод, теорема о табличной проверке общезначимости, теоремы о корректности и полноте табличного вывода.
<li> Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Теорема Чёрча.
+
<li> Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева.
 +
<li> Машины Тьюринга. Теорема Чёрча.
 
<li> Равносильные формулы. Теорема о равносильной замене.
 
<li> Равносильные формулы. Теорема о равносильной замене.
 
</ol>
 
</ol>
  
 
== Метод резолюций в логике предикатов ==
 
== Метод резолюций в логике предикатов ==
<ol start="9">
+
<ol start="10">
 
<li> Предварённая нормальная форма. Теорема о предварённой нормальной форме.
 
<li> Предварённая нормальная форма. Теорема о предварённой нормальной форме.
 
<li> Сколемовская стандартная форма. Алгоритм сколемизации предварённой нормальной формы. Теорема о сколемизации.
 
<li> Сколемовская стандартная форма. Алгоритм сколемизации предварённой нормальной формы. Теорема о сколемизации.
<li> Дизъюнкты. Сведение проблемы общезначимости формул к проблеме противоречивости систем дизъюнктов.
+
<li> Дизъюнкты. Сведение проблемы общезначимости формул к проблеме невыполнимости систем дизъюнктов.
 
<li> Подстановки. Композиция подстановок. Унификатор. Наиболее общий унификатор. Задача унификации выражений логики предикатов.
 
<li> Подстановки. Композиция подстановок. Унификатор. Наиболее общий унификатор. Задача унификации выражений логики предикатов.
 
<li> Лемма о связке. Алгоритм унификации. Теорема об унификации.
 
<li> Лемма о связке. Алгоритм унификации. Теорема об унификации.
Строка 507: Строка 264:
  
 
== Логические исчисления ==
 
== Логические исчисления ==
<ol start="18">
+
<ol start="19">
<li> Логические исчисления. Исчисления высказываний и исчисления предикатов. Доказуемость (выводимость) формул.
+
<li> Логические исчисления. Исчисления высказываний и исчисления предикатов. Выводимость и доказуемость формул.
<li> Натуральное исчисление высказываний. Корректность и полнота исчисления.
+
<li> Натуральное исчисление высказываний. Правило монотонности. Закон исключённого третьего. Правило сечения. Правило полного перебора. Правило приведения к абсурду. Корректность и полнота исчисления.
 
<li> Натуральное исчисление предикатов. Корректность и полнота исчисления.
 
<li> Натуральное исчисление предикатов. Корректность и полнота исчисления.
<li> Исчисление предикатов гильбертовского типа. Теорема Гёделя о полноте.
+
<li> Исчисление предикатов гильбертовского типа. Теорема Гёделя о полноте (формулировка).
 +
</ol>
 +
 
 +
== Аксиоматические теории ==
 +
<ol start="23">
 +
<li> Аксиоматические теории первого порядка: основные определения, проблема общезначимости формул в теории.
 +
<li> Основные свойства аксиоматических теорий: непротиворечивость, элементарность, полнота, разрешимость.
 +
<li> Определения и выразимость в интерпретациях. Теорема о подстановке определения.
 +
<li> Формальная арифметика. Теорема Гёделя о неполноте (формулировка и схема доказательства).
 +
<li> Арифметика Пресбургера, её разрешимость и выразительность.
 
</ol>
 
</ol>
  
 
== Неклассические прикладные логики ==
 
== Неклассические прикладные логики ==
<ol start="22">
+
<ol start="28">
 
<li> Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики. Логика линейного времени. Логика деревьев вычислений.
 
<li> Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики. Логика линейного времени. Логика деревьев вычислений.
<li> Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Корректность и частичная корректность программ. Тройки Хоара. Логика Хоара. Корректность вывода в логике Хоара. Слабейшее предусловие. Инвариант цикла.
+
<li> Интуиционистская логика.
<li> Верификация распределённых систем. Логика линейного времени: синтаксис, семантика. Основные равносильности в логике линейного времени. Применение темпоральных логик для спецификации поведения распределённых систем.
+
<li> Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Полная и частичная корректность программ. Тройки Хоара. Логика Хоара. Корректность вывода в логике Хоара. Слабейшее предусловие. Инвариант цикла.
<li> Размеченные системы переходов. Моделирование программ системами переходов. Семантика чередующихся вычислений. Задача верификации (проверки моделей; model checking) для логики линейного времени.
+
<li> Размеченные системы переходов. Моделирование программ системами переходов. Логика деревьев вычислений (CTL): синтаксис, семантика, основные равносильности, применение для спецификации поведения распределённых систем. Задача проверки моделей (model checking) относительно CTL: формулировка, решающий алгоритм.
<li> Табличный алгоритм верификации для логики линейного времени. Упрощение формул. Замыкание Фишера-Ладнера. Согласованные предположения. Система Хинтикки. Сведение задачи верификации к графовым задачам.
+
 
</ol>
 
</ol>
  

Текущая версия на 15:16, 26 марта 2024


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

Обязательный курс для студентов групп 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. Проверка правильности распределённых систем. Пара слов о методе model checking.

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

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

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

Семинары

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

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

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

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

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

Контрольные работы проводятся письменно, длительность каждой - 90 минут.

В контрольных работах встретятся 4 типовые задачи со следующими темами:

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

Оценка решений типовых задач:

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

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

Первая контрольная работа будет содержать

  • 3 типовые задачи по темам 1-3 и
  • 9 теоретических вопросов по прочитанным лекциям.

Вторая контрольная работа будет содержать

  • 4 типовые задачи по всем темам и
  • 5 теоретических вопросов по лекциям, не попавшим в первую контрольную работу.

Остальные контрольные работы будут содержать

  • 4 типовые задачи по всем темам и
  • 14 теоретических вопросов по всем лекциям.

Зачёт

На зачёте оцениваются результаты, относящиеся к решению типовых задач, знанию теории и работе в семестре. При проставлении зачёта учитывается 6 технических оценок:

  • Четыре оценки за типовые задачи, по одной за каждую задачу.
  • Оценка за знание теории. Максимум - 14 баллов.
  • Оценка за решение премиальных задач.

Для получения зачёта требуется получить два результата:

  1. Набрать хотя бы 11 баллов за типовые задачи.
  2. Набрать хотя бы 20 баллов суммарно за всё (типовые задачи, теория, премиальные задачи).

Баллы за типовые задачи и за теорию набираются на контрольных работах.

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

При проставлении зачёта учитывается максимальная оценка за теорию среди полученных

  • суммарно за первые две контрольные работы и
  • за каждую из следующих контрольных работ.

Экзамен

Формат проведения и длительность экзамена: письменно, 120 минут.

Экзаменационная работа содержит 10 задач и оценивается по шкале от 0 до 37 технических баллов. К этим техническим баллам прибавляются баллы за выполнение премиальных задач и поощрение/штраф за контрольную работу. Согласно набранной сумме технических баллов выставляется оценка:

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

Баллы за экзаменационную работу складываются из баллов за каждую задачу, предложенную в работе:

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

Контрольная работа

На оценку за экзамен влияет первая контрольная работа. Максимальная техническая оценка за эту работу - 21 балл. В зависимости от технических баллов, набранных за первую контрольную работу, определяется поощрение или штраф к техническим баллам за экзамен:

  • Набрано хотя бы 19 баллов: бонус +3 балла;
  • Набрано хотя бы 16, но менее 19 баллов: бонус +2 балла;
  • Набрано хотя бы 13, но менее 16 баллов: бонус +1 балл;
  • Набрано хотя бы 10, но менее 13 баллов: 0 баллов;
  • Набрано хотя бы 7, но менее 10 баллов: штраф -1 балл;
  • Набрано хотя бы 4, но менее 7 баллов: штраф -2 балла;
  • Набрано менее 4 баллов: штраф -3 балла;
  • Неявка без уважительной причины: штраф -3 балла;
  • Неявка по уважительной причине: 0 баллов.

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

Общие условия сдачи решений премиальных задач:

  • Можно как прислать письменное решение, так и обсудить решение устно. Если прислано письменное решение и к нему есть вопросы, то для ответов на эти вопросы может потребоваться дополнительное устное обсуждение.
  • При подготовке решения и во время его сдачи можно пользоваться любыми материалами.
  • При сдаче может быть проверено понимание каждой детали предложенного решения - следует быть к этому готовым.
  • Решение принимается, когда по нему не остаётся неотвеченных вопросов.

Бонусы за решение задач формулируются для одной учебной группы и распределяются внутри одной группы независимо от другой. Например, "первый" трактуется как "первый в группе 318, а также первый в группе 319/2, а также ...".

Условия задач и статистика принятых решений будут обновляться и доводиться до слушателей по мере чтения курса.

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

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

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

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