Математическая логика и логическое программирование (группа 318) — различия между версиями

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
 
(не показаны 29 промежуточные версии 1 участника)
Строка 1: Строка 1:
 
Обязательный курс для студентов групп 318 и 319/2, ''а также 241 и 242 (Математическая логика и теория алгоритмов)''. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].
 
Обязательный курс для студентов групп 318 и 319/2, ''а также 241 и 242 (Математическая логика и теория алгоритмов)''. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].
  
Актуальность информации: весенний семестр 2020/2021 учебного года.
+
Актуальность информации: весенний семестр 2021/2022 учебного года.
  
 
<!--
 
<!--
Строка 12: Строка 12:
  
 
= Слайды лекций =
 
= Слайды лекций =
 
''Слайды будут выкладываться по мере проведения занятий''
 
  
 
'''[[Media: Mathlog_318_b1.pdf|Блок 1]]''' (вводный). Что такое логика. Содержание лекций. Несколько логических парадоксов.
 
'''[[Media: Mathlog_318_b1.pdf|Блок 1]]''' (вводный). Что такое логика. Содержание лекций. Несколько логических парадоксов.
  
'''[[Media: Mathlog_318_b2.pdf|Блок 2]]'''. Логика высказываний: синтаксис, семантика, выполнимость, общезначимость.
+
'''[[Media: Mathlog_318_b2.pdf|Блок 2]]'''. Логика высказываний: синтаксис, семантика.
  
 
'''[[Media: Mathlog_318_b3.pdf|Блок 3]]'''. Логика предикатов: синтаксис, семантика.
 
'''[[Media: Mathlog_318_b3.pdf|Блок 3]]'''. Логика предикатов: синтаксис, семантика.
Строка 23: Строка 21:
 
'''[[Media: Mathlog_318_b4.pdf|Блок 4]]'''. Как формализовать предложение на языке логики предикатов (пример).
 
'''[[Media: Mathlog_318_b4.pdf|Блок 4]]'''. Как формализовать предложение на языке логики предикатов (пример).
  
'''[[Media: Mathlog_318_b5.pdf|Блок 5]]'''. Логика предикатов: выполнимые и общезначимые формулы; модели формул; логическое следствие; проблема общезначимости формул (постановка).
+
'''[[Media: Mathlog_318_b5.pdf|Блок 5]]'''. Логика высказываний: выполнимые и общезначимые формулы.
 +
 
 +
'''[[Media: Mathlog_318_b6.pdf|Блок 6]]'''. Логика предикатов: выполнимые и общезначимые формулы; модели формул; логическое следствие; проблема общезначимости формул (постановка).
 +
 
 +
'''[[Media: Mathlog_318_b7.pdf|Блок 7]]'''. Логика предикатов: можно ли проверить общезначимость формулы "в лоб"?
 +
 
 +
'''[[Media: Mathlog_318_b8.pdf|Блок 8]]'''. Логика высказываний: метод семантических таблиц.
 +
 
 +
'''[[Media: Mathlog_318_b9.pdf|Блок 9]]'''. Метод семантических таблиц в логике предикатов: семантические таблицы.
 +
 
 +
'''[[Media: Mathlog_318_b10.pdf|Блок 10]]'''. Подстановки (основные определения).
 +
 
 +
'''[[Media: Mathlog_318_b11.pdf|Блок 11]]'''. Метод семантических таблиц в логике предикатов: табличный вывод.
 +
 
 +
'''[[Media: Mathlog_318_b12.pdf|Блок 12]]'''. Метод семантических таблиц в логике предикатов: корректность табличного вывода.
 +
 
 +
'''[[Media: Mathlog_318_b13.pdf|Блок 13]]'''. Метод семантических таблиц в логике предикатов: полнота табличного вывода.
 +
 
 +
'''[[Media: Mathlog_318_b14.pdf|Блок 14]]'''. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Автоматизация доказательства теорем.
 +
 
 +
'''[[Media: Mathlog_318_b15.pdf|Блок 15]]'''. Общая схема метода резолюций.
 +
 
 +
'''[[Media: Mathlog_318_b16.pdf|Блок 16]]'''. Равносильность формул логики предикатов.
 +
 
 +
'''[[Media: Mathlog_318_b17.pdf|Блок 17]]'''. Предварённая нормальная форма (ПНФ).
 +
 
 +
'''[[Media: Mathlog_318_b18.pdf|Блок 18]]'''. Сколемовская стандартная форма (ССФ).
 +
 
 +
'''[[Media: Mathlog_318_b19.pdf|Блок 19]]'''. Системы дизъюнктов.
 +
 
 +
'''[[Media: Mathlog_318_b20.pdf|Блок 20]]'''. Композиция подстановок. Постановка задачи унификации.
 +
 
 +
'''[[Media: Mathlog_318_b21.pdf|Блок 21]]'''. Алгоритм унификации атомарных формул логики предикатов.
 +
 
 +
'''[[Media: Mathlog_318_b22.pdf|Блок 22]]'''. Резолютивный вывод. Корректность резолютивного вывода.
 +
 
 +
'''[[Media: Mathlog_318_b23.pdf|Блок 23]]'''. Обоснование общезначимости формулы методом резолюций (пример).
 +
 
 +
'''[[Media: Mathlog_318_b24.pdf|Блок 24]]'''. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях.
 +
 
 +
'''[[Media: Mathlog_318_b25.pdf|Блок 25]]'''. Теорема Эрбрана. Полнота резолютивного вывода.
 +
 
 +
'''[[Media: Mathlog_318_b26.pdf|Блок 26]]'''. Даша, Саша, Паша, пиво и метод семантических таблиц с методом резолюций.
 +
 
 +
'''[[Media: Mathlog_318_b27.pdf|Блок 27]]'''. Как устроены математические доказательства. Логические исчисления.
 +
 
 +
'''[[Media: Mathlog_318_b28.pdf|Блок 28]]'''. Натуральное исчисление высказываний: основные определения.
 +
 
 +
'''[[Media: Mathlog_318_b29.pdf|Блок 29]]'''. Натуральное исчисление высказываний: правило монотонности, закон исключённого третьего, корректность.
 +
 
 +
'''[[Media: Mathlog_318_b30.pdf|Блок 30]]'''. Натуральное исчисление высказываний: правило сечения, правило полного перебора, правило приведения к абсурду, полнота.
 +
 
 +
'''[[Media: Mathlog_318_b31.pdf|Блок 31]]'''. Натуральное исчисление предикатов: основные определения, корректность.
 +
 
 +
'''[[Media: Mathlog_318_b32.pdf|Блок 32]]'''. Гильбертовское исчисление предикатов. Теорема Гёделя о полноте (формулировка).
 +
 
 +
'''[[Media: Mathlog_318_b33.pdf|Блок 33]]'''. Натуральное исчисление предикатов: полнота.
 +
 
 +
'''[[Media: Mathlog_318_b34.pdf|Блок 34]]'''. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.
 +
 
 +
'''[[Media: Mathlog_318_b35.pdf|Блок 35]]'''. Машины Тьюринга (МТ).
  
'''[[Media: Mathlog_318_b6.pdf|Блок 6]]'''. Логика предикатов: почему бы не проверять общезначимость формул "в лоб"?
+
'''[[Media: Mathlog_318_b36.pdf|Блок 36]]'''. Теорема Чёрча.
  
'''[[Media: Mathlog_318_b7.pdf|Блок 7]]'''. Метод семантических таблиц в логике высказываний.
+
'''[[Media: Mathlog_318_b37.pdf|Блок 37]]'''. Аксиоматические теории первого порядка. Проблема общезначимости формул в теории.
  
'''[[Media: Mathlog_318_b8.pdf|Блок 8]]'''. Метод семантических таблиц в логике предикатов: семантические таблицы.
+
'''[[Media: Mathlog_318_b38.pdf|Блок 38]]'''. Основные свойства аксиоматических теорий.
  
'''[[Media: Mathlog_318_b9.pdf|Блок 9]]'''. Подстановки (основные определения).
+
'''[[Media: Mathlog_318_b39.pdf|Блок 39]]'''. Арифметические интерпретации и теории.
  
'''[[Media: Mathlog_318_b10.pdf|Блок 10]]'''. Метод семантических таблиц в логике предикатов: табличный вывод.
+
'''[[Media: Mathlog_318_b40.pdf|Блок 40]]'''. Определения и выразимость.
  
'''[[Media: Mathlog_318_b11.pdf|Блок 11]]'''. Метод семантических таблиц в логике предикатов: корректность табличного вывода.
+
'''[[Media: Mathlog_318_b41.pdf|Блок 41]]'''. Формальная арифметика. Теорема Гёделя о неполноте.
  
'''[[Media: Mathlog_318_b12.pdf|Блок 12]]'''. Метод семантических таблиц в логике предикатов: полнота табличного вывода.
+
'''[[Media: Mathlog_318_b42.pdf|Блок 42]]'''. Арифметика Пресбургера.
  
'''[[Media: Mathlog_318_b13.pdf|Блок 13]]'''. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Автоматизация доказательства теорем.
+
'''[[Media: Mathlog_318_b43.pdf|Блок 43]]'''. Модальные логики.
  
'''[[Media: Mathlog_318_b14.pdf|Блок 14]]'''. Общая схема метода резолюций.
+
'''[[Media: Mathlog_318_b44.pdf|Блок 44]]'''. Эпистемические логики.
  
'''[[Media: Mathlog_318_b15.pdf|Блок 15]]'''. Равносильность формул логики предикатов.
+
'''[[Media: Mathlog_318_b45.pdf|Блок 45]]'''. Темпоральные логики.
  
'''[[Media: Mathlog_318_b16.pdf|Блок 16]]'''. Предварённая нормальная форма (ПНФ).
+
'''[[Media: Mathlog_318_b46.pdf|Блок 46]]'''. Что ещё интересного есть в логике. Формальная верификация.
  
'''[[Media: Mathlog_318_b17.pdf|Блок 17]]'''. Сколемовская стандартная форма (ССФ).
+
'''[[Media: Mathlog_318_b47.pdf|Блок 47]]'''. Императивные программы. Формальная верификация программ. Логика Хоара.
  
'''[[Media: Mathlog_318_b18.pdf|Блок 18]]'''. Системы дизъюнктов.
+
'''[[Media: Mathlog_318_b48.pdf|Блок 48]]'''. Проверка моделей относительно логики деревьев вычислений (CTL model checking).
  
'''[[Media: Mathlog_318_b19.pdf|Блок 19]]'''. Композиция подстановок. Постановка задачи унификации.
+
''Слайды будут обновляться по мере проведения занятий''
  
 
== Слайды прошлых лет ==
 
== Слайды прошлых лет ==
Строка 97: Строка 155:
 
Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]]
 
Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]]
  
[[Media:Mathlog_318_seminar_natural_inference.pdf| Материалы семинара 5 (натуральное исчисление).]]
+
[[Media:Mathlog_318_seminar_natural_inference.pdf| Материалы семинара 5-6 (натуральное исчисление).]]
  
= Экзамен =
+
= Контрольные работы =
  
Формат проведения и длительность экзамена: письменно, 120 минут.
+
Контрольные работы проводятся письменно, длительность каждой - 90 минут.
  
Экзаменационная работа оценивается по шкале от 0 до 33 технических баллов.
+
В контрольных работах встретятся 4 типовые задачи со следующими темами:
К оценке за эту работу прибавляются технические баллы, полученные за работу в семестре (выполнение премиальных задач).
+
# Формализовать в логике предикатов предложение, записанное на естественном языке.
Согласно набранной сумме технических баллов выставляется оценка:
+
# Обосновать общезначимость формулы логики предикатов методом семантических таблиц.
* хотя бы 27: '''отлично''';
+
# Обосновать общезначимость формулы логики предикатов методом резолюций.
* хотя бы 21, но менее 27: '''хорошо''';
+
# ''Задача на тему доказательства общезначимости формулы логики предикатов в натуральном исчислении, точная формулировка будет позже''.
* хотя бы 15, но менее 21: '''удовлетворительно''';
+
* менее 15: '''неудовлетворительно'''.
+
  
Баллы за экзаменационную работу складываются из баллов за каждую задачу, предложенную в работе:
+
Оценка решений типовых задач:
* Каждая из задач 1-5 оценивается в 3 балла. Темы задач:
+
* Максимальная оценка - 4 балла.
*# Формализовать в логике предикатов предложение, записанное на естественном языке.
+
* Если решение в целом верно, но содержит редкие ошибки серьёзнее опечаток, то оно оценивается в 3 балла.
*# Проверить общезначимость формулы логики предикатов методом семантических таблиц.
+
* Если решение содержит серьёзные ошибки, но имеет структуру, в целом разумно соотносящуюся с правильной, то задача оценивается в 2 балла.
*# Проверить общезначимость формулы логики предикатов методом резолюций.
+
* Если в решении обнаружены правильные элементы, но в малом количестве, то задача оценивается в 1 балл.
*# ''По теме логических исчислений, точная формулировка определится позже''.
+
 
*# ''По теме аксиоматических теорий, точная формулировка определится позже''.
+
Теоретические вопросы даются в форме теста с множественным выбором: из предложенных вариантов ответа требуется выбрать правильные (один, несколько или ни одного), обоснование не требуется.
* Каждая из задач 6-8 оценивается в 2 балла и состоит из двух частей:
+
Правильно решённый теоретический вопрос оценивается в 1 балл.
*# Сформулировать утверждение, определение и т.п.
+
 
*# Ответить на вопрос "на понимание", так или иначе связанный с формулировкой.
+
'''Первая контрольная работа''' будет содержать 3 типовые задачи (по темам 1-3) и 9 теоретических вопросов (по прочитанным лекциям).
* Каждая из задач 9-12 оценивается в 3 балла и устроена так:
+
 
** Из нескольких предложенных вариантов ответа выбрать правильные (один, несколько или ни одного) и '''обосновать''' выбранные ответы.
+
'''Вторая контрольная работа''' будет содержать все типовые задачи и 5 теоретических вопросов (по темам, не попавшим в первую контрольную работу).
** Невыбранные ответы обосновывать не нужно.
+
 
 +
'''Остальные контрольные работы''' будут содержать все типовые задачи и 14 теоретических вопросов (по всем темам лекций).
  
 
= Зачёт =
 
= Зачёт =
  
 
На зачёте оцениваются результаты, относящиеся к решению типовых задач, знанию теории и работе в семестре.
 
На зачёте оцениваются результаты, относящиеся к решению типовых задач, знанию теории и работе в семестре.
 
+
При проставлении зачёта учитывается 6 технических оценок:
В курсе встретится 5 типовых задач:
+
* Четыре оценки за типовые задачи, по одной за каждую задачу.
# Формализовать в логике предикатов предложение, записанное на естественном языке.
+
* Оценка за знание теории. Максимум - 14 баллов.
# Проверить общезначимость формулы логики предикатов методом семантических таблиц.
+
# Проверить общезначимость формулы логики предикатов методом резолюций.
+
# ''По теме логических исчислений, точная формулировка определится позже''.
+
# ''По теме аксиоматических теорий, точная формулировка определится позже''.
+
 
+
При проставлении зачёта учитывается 7 технических оценок:
+
* Пять оценок за типовые задачи, по одной за каждую задачу. Максимальная оценка за каждую задачу - 3 балла.
+
* Оценка за знание теории. Максимум - 15 баллов.
+
 
* Оценка за решение премиальных задач.
 
* Оценка за решение премиальных задач.
  
 
Для получения зачёта требуется достичь следующих результатов:
 
Для получения зачёта требуется достичь следующих результатов:
# '''Решить хотя бы 4 типовые задачи на 2 балла''' (т.е. правильно или с незначительными недочётами).
+
# Набрать хотя бы 11 баллов за типовые задачи.
# '''Набрать хотя бы 20 баллов''' суммарно за всё (типовые задачи, теория, премиальные задачи).
+
# Набрать хотя бы 20 баллов суммарно за всё (типовые задачи, теория, премиальные задачи).
  
В курсе планируются две контрольные работы: первая - в середине семестра, вторая - после завершения лекций.
+
Баллы за типовые задачи и за теорию набираются на [[#Контрольные работы|контрольных работах]].
Контрольные работы и попытки зачёта проводятся письменно, длительность каждого мероприятия - 90 минут (одна пара).
+
 
+
== Сдача типовых задач ==
+
  
 
Для решения каждой типовой задачи будет предложено несколько попыток.
 
Для решения каждой типовой задачи будет предложено несколько попыток.
 
При проставлении зачёта учитывается '''максимальная''' оценка за задачу среди всех попыток её решить.
 
При проставлении зачёта учитывается '''максимальная''' оценка за задачу среди всех попыток её решить.
  
На первой контрольной работе будут предложены типовые задачи 1-3.
+
При проставлении зачёта учитывается '''максимальная''' оценка среди полученных за первые две контрольные работы (суммарно) и за каждую из следующих контрольных работ.
На второй контрольной работе и на каждой попытке зачёта будут предложены все типовые задачи.
+
  
== Сдача теории ==
+
= Экзамен =
  
Теоретические вопросы даются в форме теста с множественным выбором: из предложенных вариантов ответа требуется выбрать правильные (один, несколько или ни одного), обоснование не требуется.
+
Формат проведения и длительность экзамена: письменно, 120 минут.
Правильно решённый теоретический вопрос оценивается в 1 балл.
+
  
На первой контрольной работе будет предложено 9 теоретических вопросов.
+
Экзаменационная работа оценивается по шкале от 0 до 30 технических баллов.
На второй контрольной работе будет предложено 6 теоретических вопросов.
+
К этим техническим баллам прибавляются баллы за выполнение премиальных задач и поощрение/штраф за [[#Контрольная работа|контрольную работу]].
Оценка за знание теории складывается из оценок за эти 15 теоретических вопросов.
+
Согласно набранной сумме технических баллов выставляется оценка:
 +
* хотя бы 24: '''отлично''';
 +
* хотя бы 18, но менее 24: '''хорошо''';
 +
* хотя бы 12, но менее 18: '''удовлетворительно''';
 +
* менее 12: '''неудовлетворительно'''.
  
На каждой попытке зачёта также будет предложено 15 теоретических вопросов.
+
Баллы за экзаменационную работу складываются из баллов за каждую задачу, предложенную в работе:
При проставлении зачёта учитывается '''максимальная''' оценка среди полученных за контрольные работы и за каждую из попыток зачёта.
+
* Каждая из задач 1-4 оценивается в 3 балла. Темы задач:
 +
*# Формализовать в логике предикатов предложение, записанное на естественном языке.
 +
*# Проверить общезначимость формулы логики предикатов методом семантических таблиц.
 +
*# Проверить общезначимость формулы логики предикатов методом резолюций.
 +
*# ''Задача на тему доказательства общезначимости формулы логики предикатов в натуральном исчислении, точная формулировка будет позже''.
 +
* Каждая из задач 5-7 оценивается в 2 балла и состоит из двух частей:
 +
*# Сформулировать утверждение, определение и т.п.
 +
*# Ответить на вопрос "на понимание", так или иначе связанный с формулировкой.
 +
* Каждая из задач 8-11 оценивается в 3 балла и устроена так:
 +
** Из нескольких предложенных вариантов ответа выбрать правильные (один, несколько или ни одного) и '''обосновать''' выбранные ответы.
 +
** Невыбранные ответы обосновывать не нужно.
  
= Премиальные задачи =
+
== Контрольная работа ==
  
''По ходу проведения курса в подразделах этого раздела будут появляться премиальные задачи''
+
На оценку за экзамен влияет первая [[#Контрольные работы|контрольная работа]].
 +
Максимальная техническая оценка за эту работу - 21 балл.
 +
В зависимости от технических баллов, набранных за первую контрольную работу, определяется поощрение или штраф к техническим баллам за экзамен:
 +
* набрано хотя бы 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:#DDFFDD">+0 баллов</span>;
 +
* набрано хотя бы 7, но менее 10 баллов: штраф <span style="background:#FFDDDD">-1 балл</span>;
 +
* набрано хотя бы 4, но менее 7 баллов: штраф <span style="background:#FFDDDD">-2 балла</span>;
 +
* набрано менее 4 баллов: штраф <span style="background:#FFDDDD">-3 балла</span>;
 +
* контрольная работа пропущена по неуважительной причине: штраф <span style="background:#FFDDDD">-3 балла</span>;
 +
* контрольная работа пропущена по уважительной причине: бонус <span style="background:#DDFFDD">+0 баллов</span>.
 +
 
 +
= Премиальные задачи =
  
 
Общие условия сдачи решений премиальных задач:
 
Общие условия сдачи решений премиальных задач:
Строка 180: Строка 251:
 
'''Бонусы за решение задач сформулированы для одной учебной группы''' и получаются внутри одной группы независимо от другой.
 
'''Бонусы за решение задач сформулированы для одной учебной группы''' и получаются внутри одной группы независимо от другой.
 
Например, "''первый''" трактуется как "''первый из группы 318, а также первый из группы 319/2, а также ...''".
 
Например, "''первый''" трактуется как "''первый из группы 318, а также первый из группы 319/2, а также ...''".
 +
 +
Условия задач и статистика принятых решений доступны [https://docs.google.com/spreadsheets/d/1AwsansGZtYx-m7xwpBfmh6UL11dVHiNAyIsIBMC7bAI/edit?usp=sharing по этой ссылке]
 +
 +
<!--
  
 
== (1) Свойства семантических таблиц в логике высказываний ==
 
== (1) Свойства семантических таблиц в логике высказываний ==
  
Доказать три утверждения в блоке 7, доказательство которых помечено словами "А попробуйте сами", '''или''' два утверждения в блоке 8, помеченные теми же словами.
+
Доказать три утверждения в блоке 8, доказательство которых помечено словами "А попробуйте сами", '''или''' два утверждения в блоке 9, помеченные теми же словами.
  
 
Бонус за решение задачи: <span style="background:#DDFFDD">+1 балл</span> первым '''двум''' предоставившим решение задачи
 
Бонус за решение задачи: <span style="background:#DDFFDD">+1 балл</span> первым '''двум''' предоставившим решение задачи
Строка 232: Строка 307:
 
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
 
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
  
 +
== (7) Фундированность троек чисел ==
  
<!--
+
Доказать фундированность троек неотрицательных целых чисел относительно лексикографического порядка (лемма в блоке 20, обоснование которой помечено словами "Попробуйте сами").
  
== (3) Фундированность троек чисел ==
+
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение задачи
  
Доказать фундированность троек неотрицательных целых чисел относительно лексикографического порядка (лемма в лекции 8, сформулированная в рамках доказательства завершаемости алгоритма унификации, обоснование которой помечено словами "Попробуйте сами").
+
== (8) Про эрбрановские интерпретации ==
  
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение задачи
+
Останется ли справедливой теорема об эрбрановских интерпретациях, если вместо "Система дизъюнктов" в её формулировке написать "Формула логики предикатов"?
 +
Ответ обосновать.
 +
 
 +
Бонус за решение задачи:
 +
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
 +
* '''второй''' сдавший: <span style="background:#DDFFDD">+2 балла</span>
 +
 
 +
== (9) Полная стратегия построения успешного резолютивного вывода ==
  
== (4) Стратегия построения резолютивного вывода ==
+
Предложить (с обоснованием) список правил построения резолютивного вывода, гарантирующих получение пустого дизъюнкта из конечной невыполнимой системы дизъюнктов.
  
Сформулировать (с обоснованием) список правил, которых достаточно придерживаться, чтобы в резолютивном выводе, строящемся произвольно в рамках этих правил для противоречивой системы дизъюнктов, рано или поздно появился пустой дизъюнкт.
+
(Как это делалось, например, в доказательстве теоремы о полноте табличного вывода.)
  
 
Бонусы за решение задачи:
 
Бонусы за решение задачи:
Строка 249: Строка 332:
 
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
 
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
  
== (5) Вычислительные возможности метода резолюций ==
+
== (10) Вычислительные возможности метода резолюций ==
  
Сформулировать и обосновать утверждение, дающее ответ на вопрос, поставленный в конце "заключительного примера для метода резолюций" лекции 10.
+
Ответить (с обоснованием и для достаточно широкого семейства резолютивных выводов) на вопрос, поставленный в конце "заключительного примера для метода резолюций" блока 25.
  
 
Бонусы за решение задачи:
 
Бонусы за решение задачи:
Строка 257: Строка 340:
 
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
 
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
  
== (6) Исчисление семантических таблиц ==
+
== (11) Исчисление семантических таблиц ==
  
Определить аксиомы и правила вывода логического исчисления со следующими свойствами:
+
Определить (с пояснениями) аксиомы и правила вывода логического исчисления со следующими свойствами:
 
* формулы исчисления - семантические таблицы логики предикатов;
 
* формулы исчисления - семантические таблицы логики предикатов;
* таблица выводима в исчислении тогда и только тогда, когда для неё существует успешный табличный вывод,
+
* таблица доказуема в исчислении тогда и только тогда, когда для неё существует успешный табличный вывод;
* из доказательства для таблицы T можно получить успешный табличный вывод для T, взяв некоторое неразмеченное дерево и доразметив вершины этого дерева таблицами из доказательства.
+
* из доказательства для таблицы T в исчислении можно получить успешный табличный вывод для T, расположив таблицы в вершинах дерева согласно применению правил исчисления.
  
 
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение задачи
 
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение задачи
  
== (7) Корректность натурального исчисления ==
+
== (12) Корректность натурального исчисления предикатов ==
  
Выбрать одно из 4-х правил работы с кванторами в натуральном исчислении (введение/удаление существования/всеобщности) и обосновать корректность этого правила: если формулы над чертой общезначимы, то и формула под чертой общезначима (см. лекцию 12-13).
+
Выбрать одно из четырёх правил вывода НИП для кванторов (введение/удаление существования/всеобщности) и обосновать корректность этого правила согласно разобранному в доказательстве теоремы о корректности НИВ.
  
 
Для каждого из правил принимается только одно решение, и от одного студента принимается решение только для одного правила.
 
Для каждого из правил принимается только одно решение, и от одного студента принимается решение только для одного правила.
 
Бонус за решение: <span style="background:#DDFFDD">+1 балл</span>
 
Бонус за решение: <span style="background:#DDFFDD">+1 балл</span>
  
== (8) Теорема Гёделя о полноте ==
+
== (13) Теорема Гёделя о полноте ==
  
Доказать теорему Гёделя о полноте (см. лекцию 12-13).
+
Доказать теорему Гёделя о полноте, сформулированную в блоке 31, для исчисления, изложенного в этом же блоке.
  
 
Бонусы за решение задачи:
 
Бонусы за решение задачи:
Строка 281: Строка 364:
 
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+7 баллов</span>
 
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+7 баллов</span>
  
== (9) Свойства шкал Крипке ==
+
== (14) Непротиворечивая конечная полная теория ==
  
Доказать утверждения о рефлексивности, транзитивности и симметричности шкал Крипке, сформулированные в разделе "Эпистемические логики" '''лекции 14'''
+
Привести пример (с обоснованием) непротиворечивой конечной полной аксиоматической теории первого порядка.
  
 
Бонус за решение задачи:
 
Бонус за решение задачи:
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
+
* '''первый''' сдавший: <span style="background:#DDFFDD">+2 балла</span>
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
+
* '''второй''' сдавший: <span style="background:#DDFFDD">+1 балл</span>
  
== (10) Задача о трёх мудрецах ==
+
== (15) О подстановке определения ==
  
Записать и пояснить ход рассуждений мудрецов в ''задаче о трёх мудрецах'' ('''лекция 14''') в терминах эпистемической логики.
+
Оформить пропущенные части доказательства теоремы о подстановке определения: доказательство для функции кси и часть доказательства, скрытая в отсылке к теореме о равносильной замене.
  
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''трём''' предоставившим решение.
+
Бонус за решение задачи:
 +
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
 +
* '''второй''' сдавший: <span style="background:#DDFFDD">+2 балла</span>
  
== (11) Корректность логики Хоара ==
+
== (16) Теорема Гёделя о неполноте ==
  
Доказать корректность одного из правил логики Хоара ('''лекция 15, лемма о корректности правил'''), кроме правил для пустой команды и для присваивания.
+
Доказать теорему Гёделя о неполноте в формулировке, представленной в блоке 40: либо адаптировать представленный там эскиз доказательства к общему случаю и доказать леммы об арифметизации и о диагонали, либо предоставить независимое доказательство.
  
Для каждого из правил принимается только одно решение, и от одного студента принимается решение только для одного правила.
+
Бонусы за решение задачи:
Бонус за решение: <span style="background:#DDFFDD">+2 балла</span>
+
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+14 баллов</span>
 +
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+11 баллов</span>
 +
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+8 баллов</span>
  
== (12) Слабейшие предусловия ==
+
== (17) Арифметика Пресбургера ==
  
Доказать теорему о слабейшем предусловии ('''лекция 15''').
+
Доказать полноту системы аксиом арифметики Пресбургера, представленной на последнем слайде блока 41.
  
 
Бонусы за решение задачи:
 
Бонусы за решение задачи:
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
+
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+4 балла</span>
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
+
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+3 балла</span>
 +
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+2 балл</span>
  
== (13) Законы темпоральных логик ==
+
== (18) Определение экспоненты ==
  
В '''лекции 16''' на слайде под заголовком "законы дистрибутивности" выбрать пару строк (1+2, 3+4, 5+6 или 7+8) и доказать либо опровергнуть равносильность в каждой из этих двух строк.
+
Предложить (с обоснованием) определение одноместной функции 2^x (два в степени икс) в арифметической интерпретации на целых неотрицательных числах с сигнатурой <{0}, {+, x, s}, {=}> (семинар 5, задача 1, пункт 21).
  
Для каждой пары строк принимается только одно решение, и от одного студента принимается решение только для одной пары строк.
+
''Если в обосновании будут содержаться китайская теорема об остатках, малая теорема Ферма или что-либо другое нетривиальное, то обоснование этого - часть решения''
Бонус за решение: <span style="background:#DDFFDD">+1 балл</span>
+
 
+
== (14) Табличный алгоритм верификации для LTL ==
+
 
+
Ответить на существенную часть вопросов, сформулированных на последнем слайде последней лекции (17)
+
 
+
Бонус за решение задачи: '''обсуждается индивидуально'''.
+
-->
+
 
+
<!--
+
 
+
== Изоморфизм и элементарная эквивалентность интерпретаций ==
+
 
+
=== Описание задачи ===
+
 
+
Доказать утверждение на слайде 24 лекции 10 о соотношении понятий изоморфизма и элементарной эквивалентности интерпретаций.
+
  
 
Бонусы за решение задачи:
 
Бонусы за решение задачи:
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+2 балла</span>
+
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+4 баллов</span>
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+1 балл</span>
+
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+3 балла</span>
 +
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+2 балла</span>
  
=== Количество предоставленных решений ===
+
== (19) Свойства шкал Крипке ==
  
'''Группа 318:''' 1
+
Доказать утверждения о рефлексивности, транзитивности и симметричности шкал Крипке, сформулированные в блоке 43.
  
== <s>Теорема Гёделя о неполноте</s> ==
+
Бонус за решение задачи:
 +
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
 +
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
  
=== Описание задачи ===
+
== (20) Задача о трёх мудрецах ==
  
Доказать теорему Гёделя о неполноте ('''лекция 10'''): либо адаптировать доказательство в лекции к общему случаю и доказать лемму о диагонали и утверждение об арифметизуемости графика, либо предоставить независимое доказательство.
+
Записать и пояснить ход рассуждений мудрецов в ''задаче о трёх мудрецах'', представленной в конце блока 43, в терминах эпистемической логики.
  
Бонусы за решение задачи:
+
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''трём''' предоставившим решение.
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+14 баллов</span>
+
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+11 баллов</span>
+
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+8 баллов</span>
+
  
=== Количество предоставленных решений ===
+
== (21) Корректность логики Хоара ==
  
'''Группа 318:''' 3 (все баллы розданы)
+
Доказать корректность одного из правил логики Хоара ('''блок 46, лемма о корректности правил'''), кроме правил для пустой команды и для присваивания.
  
== Арифметика Пресбургера и математическая индукция ==
+
Для каждого из правил принимается только одно решение, и от одного студента принимается решение только для одного правила.
 +
Бонус за решение: <span style="background:#DDFFDD">+2 балла</span>
  
=== Описание задачи ===
+
== (22) Слабейшие предусловия ==
  
Указать все места в доказательстве разрешимости арифметики Пресбургера ('''лекция 11'''), в которых существенно используется наличие схемы аксиом индукции в этой арифметике, и объяснить способ использования.
+
Доказать теорему о слабейшем предусловии ('''лекция 15''').
  
 
Бонусы за решение задачи:
 
Бонусы за решение задачи:
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+3 балла</span>
+
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+2 балла</span>
+
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+1 балл</span>
+
  
=== Количество предоставленных решений ===
+
== (23) Упрощение ctl-формул ==
  
'''Группа 318:''' 0
+
Доказать один из зелёных пунктов утверждения об упрощении ctl-формул в '''блоке 47'''.
  
== <s>Определение экспоненты</s> ==
+
Для каждого пункта принимается только одно решение, и от одного студента принимается решение только для одного пункта.
 +
Бонус за решение: <span style="background:#DDFFDD">+1 балл</span>
  
=== Описание задачи ===
+
== (24) Алгоритм проверки выполнимости ctl-формулы на системе переходов ==
  
Предложить (с обоснованием) определение одноместной функции 2^x (два в степени икс) в арифметической интерпретации на целых неотрицательных числах с сигнатурой <{0}, {+, x, s}, {=}> (семинар 5, задача 1, пункт 19).
+
Ответить (с обоснованием) на вопрос в самом конце '''блока 47''' о корректности и сложности алгоритма проверки выполнимости ctl-формулы на системе переходов. 
 
+
''Если в обосновании будут содержаться китайская теорема об остатках, малая теорема Ферма или что-либо другое нетривиальное, то обоснование этого - часть решения''
+
  
 
Бонусы за решение задачи:
 
Бонусы за решение задачи:
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+5 баллов</span>
+
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+4 баллов</span>
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+4 балла</span>
+
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+3 балла</span>
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+3 балла</span>
+
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+2 балла</span>
  
=== Количество предоставленных решений ===
+
== (14) Табличный алгоритм верификации для LTL ==
  
'''Группа 318:''' 3 (все баллы розданы)
+
Ответить на существенную часть вопросов, сформулированных на последнем слайде последней лекции (17)
  
 +
Бонус за решение задачи: '''обсуждается индивидуально'''.
 +
-->
 +
 +
<!--
 
== Полнота семантической резолюции ==
 
== Полнота семантической резолюции ==
  

Текущая версия на 19:14, 15 мая 2022

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

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


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

Блок 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. Проверка моделей относительно логики деревьев вычислений (CTL model checking).

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

Слайды прошлых лет

Лекция (вводная). Что такое логика? Содержание лекций. История логики. Логические парадоксы.

Лекция. Логика высказываний: синтаксис, семантика, выполнимость, общезначимость. Метод семантических таблиц в логике высказываний.

Лекция. Логика предикатов: синтаксис (термы, формулы), семантика (интерпретации, отношение выполнимости).

Лекция. Выполнимые и общезначимые формулы. Модели. Логическое следствие. Проблема общезначимости формул. Подстановки. Метод семантических таблиц в логике предикатов. Корректность табличного вывода.

Лекция. Полнота табличного вывода в логике предикатов. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Равносильные формулы. Теорема о равносильной замене.

Лекция. Общая схема метода резолюций. Предварённая нормальная форма. Сколемовская стандартная форма. Системы дизъюнктов. Задача унификации.

Лекция. Алгоритм унификации атомарных формул. Теорема об унификации.

Лекция. Резолютивный вывод. Корректность резолютивного вывода. Применение метода резолюций. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях. Теорема Эрбрана.

Лекция. Полнота резолютивного вывода. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.

Лекция. Машины Тьюринга. Теорема Чёрча. Как устроены математические доказательства. Логические исчисления.

Лекция. Натуральное исчисление высказываний. Натуральное исчисление предикатов. Исчисление предикатов гильбертовского типа.

Лекция. Модальные логики. Эпистемические логики. Темпоральные логики.

Лекция. Формальная верификация программ. Императивные программы. Корректность императивных программ. Логика Хоара. Автоматизация проверки правильности программ.

Лекция. Верификация распределённых систем. Логика линейного времени (LTL). Размеченные системы переходов. Задача верификации (model checking) для LTL.

Лекция. Табличный алгоритм верификации для LTL. Замыкание Фишера-Ладнера. Системы Хинтикки.

Лекция. Аксиоматические теории. Основные свойства теорий. Формальная арифметика. Арифметика Пеано. Теорема Гёделя о неполноте. Определимость. Арифметика Пресбургера.

Лекция..

Семинары

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

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

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

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

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

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

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

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

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

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

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

Первая контрольная работа будет содержать 3 типовые задачи (по темам 1-3) и 9 теоретических вопросов (по прочитанным лекциям).

Вторая контрольная работа будет содержать все типовые задачи и 5 теоретических вопросов (по темам, не попавшим в первую контрольную работу).

Остальные контрольные работы будут содержать все типовые задачи и 14 теоретических вопросов (по всем темам лекций).

Зачёт

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

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

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

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

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

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

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

Экзамен

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

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

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

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

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

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

На оценку за экзамен влияет первая контрольная работа. Максимальная техническая оценка за эту работу - 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. Равносильные формулы. Теорема о равносильной замене.

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

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

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

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

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

  1. Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики. Логика линейного времени. Логика деревьев вычислений.
  2. Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Корректность и частичная корректность программ. Тройки Хоара. Логика Хоара. Корректность вывода в логике Хоара. Слабейшее предусловие. Инвариант цикла.
  3. Верификация распределённых систем. Логика линейного времени: синтаксис, семантика. Основные равносильности в логике линейного времени. Применение темпоральных логик для спецификации поведения распределённых систем.
  4. Размеченные системы переходов. Моделирование программ системами переходов. Семантика чередующихся вычислений. Задача верификации (проверки моделей; model checking) для логики линейного времени.
  5. Табличный алгоритм верификации для логики линейного времени. Упрощение формул. Замыкание Фишера-Ладнера. Согласованные предположения. Система Хинтикки. Сведение задачи верификации к графовым задачам.

Рекомендованная литература

Основная литература

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