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

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
 
(не показаны 99 промежуточные версии 1 участника)
Строка 1: Строка 1:
Обязательный курс для студентов 318 группы 6 семестра обучения, ''а также для студентов 241 группы (Математическая логика и теория алгоритмов)''. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].
+
Обязательный курс для студентов групп 318 и 319/2, ''а также 241 и 242 (Математическая логика и теория алгоритмов)''. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].
  
 +
Актуальность информации: весенний семестр 2020/2021 учебного года.
 +
 +
<!--
 
'''Объявления'''
 
'''Объявления'''
  
''В этом разделе будут выкладываться объявления о текущих изменениях в курсе и на странице курса''
+
''В этом разделе будут выкладываться объявления об изменениях на странице курса''
  
* 2019.04.26 17:20 Обновлена статистика предоставленных решений бонусных задач
+
* 2021.02.04 16:00 Страница курса подготовлена к весеннему семестру 2020/2021 учебного года
* 2019.04.21 20:30 Появилось условие бонусной задачи 8
+
-->
* 2019.04.21 20:22 Появились слайды лекций 12, 13
+
* 2019.02.05 14:05 Страница подготовлена к началу весеннего семестра 2018/2019 учебного года
+
  
 
= Слайды лекций =
 
= Слайды лекций =
Строка 14: Строка 15:
 
''Слайды будут выкладываться по мере проведения занятий''
 
''Слайды будут выкладываться по мере проведения занятий''
  
'''[[Media: Mathlog_318_lecture_1.pdf|Лекция 1]]''' (вводная). Что такое логика? Содержание лекций. История логики. Логические парадоксы.
+
'''[[Media: Mathlog_318_b1.pdf|Блок 1]]''' (вводный). Что такое логика. Содержание лекций. Несколько логических парадоксов.
  
'''[[Media: Mathlog_318_lecture_2.pdf|Лекция 2.]]''' Логика высказываний: синтаксис, семантика, выполнимость, общезначимость. Метод семантических таблиц в логике высказываний.
+
'''[[Media: Mathlog_318_b2.pdf|Блок 2]]'''. Логика высказываний: синтаксис, семантика, выполнимость, общезначимость.
  
'''[[Media: Mathlog_318_lecture_3.pdf|Лекция 3.]]''' Логика предикатов: синтаксис (термы, формулы), семантика (интерпретации, отношение выполнимости), выполнимость и общезначимость формул, модели.
+
'''[[Media: Mathlog_318_b3.pdf|Блок 3]]'''. Логика предикатов: синтаксис, семантика.
  
'''[[Media: Mathlog_318_lecture_4.pdf|Лекция 4.]]''' Логическое следствие. Проблема общезначимости формул. Подстановки. Метод семантических таблиц в логике предикатов. Корректность табличного вывода.
+
'''[[Media: Mathlog_318_b4.pdf|Блок 4]]'''. Как формализовать предложение на языке логики предикатов (пример).
  
'''[[Media: Mathlog_318_lecture_5.pdf|Лекция 5.]]''' Полнота табличного вывода в логике предикатов. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Теорема Чёрча. Автоматизация доказательства теорем.
+
'''[[Media: Mathlog_318_b5.pdf|Блок 5]]'''. Логика предикатов: выполнимые и общезначимые формулы; модели формул; логическое следствие; проблема общезначимости формул (постановка).
  
'''[[Media: Mathlog_318_lecture_6.pdf|Лекция 6.]]''' Общая схема метода резолюций. Равносильные формулы. Теорема о равносильной замене. Предварённая нормальная форма. Сколемовская стандартная форма. Системы дизъюнктов.
+
'''[[Media: Mathlog_318_b6.pdf|Блок 6]]'''. Логика предикатов: почему бы не проверять общезначимость формул "в лоб"?
  
'''[[Media: Mathlog_318_lecture_7.pdf|Лекция 7.]]''' Задача унификации. Алгоритм унификации атомарных формул.
+
'''[[Media: Mathlog_318_b7.pdf|Блок 7]]'''. Метод семантических таблиц в логике высказываний.
  
'''[[Media: Mathlog_318_lecture_8.pdf|Лекция 8.]]''' Резолютивный вывод. Корректность резолютивного вывода. Применение метода резолюций. Эрбрановские интерпретации. Теорема Эрбрана.
+
'''[[Media: Mathlog_318_b8.pdf|Блок 8]]'''. Метод семантических таблиц в логике предикатов: семантические таблицы.
  
'''[[Media: LectLog_10.pdf| Лекция 9. (Захаров В.А.)]]''' Полнота резолютивного вывода.
+
'''[[Media: Mathlog_318_b9.pdf|Блок 9]]'''. Подстановки (основные определения).
  
'''[[Media: Mathlog_318_lecture_10.pdf|Лекция 10.]]''' Аксиоматические теории. Основные свойства теорий (адекватность интерпретациям, непротиворечивость, разрешимость, полнота). Формальная арифметика. Арифметика Пеано. Теорема Гёделя о неполноте.
+
'''[[Media: Mathlog_318_b10.pdf|Блок 10]]'''. Метод семантических таблиц в логике предикатов: табличный вывод.
  
'''[[Media: Mathlog_318_lecture_11.pdf|Лекция 11.]]''' Выразимость в теориях и интерпретациях. Арифметика Пресбургера (определение, разрешимость, полнота, выразительные возможности).
+
'''[[Media: Mathlog_318_b11.pdf|Блок 11]]'''. Метод семантических таблиц в логике предикатов: корректность табличного вывода.
  
'''[[Media: Mathlog_318_lecture_12.pdf|Лекция 12.]]''' Логические исчисления. Исчисление высказываний гильбертовского типа. Корректность и полнота исчисления высказываний.
+
'''[[Media: Mathlog_318_b12.pdf|Блок 12]]'''. Метод семантических таблиц в логике предикатов: полнота табличного вывода.
  
'''[[Media: Mathlog_318_lecture_13.pdf|Лекция 13.]]''' Исчисление предикатов гильбертовского типа. Теорема Гёделя о полноте (формулировка). Натуральное исчисление высказываний, его корректность и полнота. Натуральное исчисление предикатов, его корректность и полнота. Натуральный вывод формул.
+
'''[[Media: Mathlog_318_b13.pdf|Блок 13]]'''. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Автоматизация доказательства теорем.
  
 +
'''[[Media: Mathlog_318_b14.pdf|Блок 14]]'''. Общая схема метода резолюций.
  
== Временный архив слайдов: 2017-2018 учебный год ==
+
'''[[Media: Mathlog_318_b15.pdf|Блок 15]]'''. Равносильность формул логики предикатов.
  
'''[[Media: Mathlog_318_lecture_9.pdf|Лекция 9.]]''' Полнота резолютивного вывода. Стратегии резолютивного вывода. Вычислительные возможности метода резолюций.
+
'''[[Media: Mathlog_318_b16.pdf|Блок 16]]'''. Предварённая нормальная форма (ПНФ).
  
'''[[Media: LectLog20.pdf|Лекция 10 (Захаров В.А.).]]''' Правильные программы. Императивные программы. Задача верификации программ. Логика Хоара. Автоматическая проверка правильности программ.
+
'''[[Media: Mathlog_318_b17.pdf|Блок 17]]'''. Сколемовская стандартная форма (ССФ).
  
'''[[Media: Mathlog_318_lecture_11_12.pdf|Лекция 11-12.]]''' Аксиоматические теории. Основные свойства теорий. Формальная арифметика. Арифметика Пеано. Теорема Гёделя о неполноте. Определимость. Арифметика Пресбургера.
+
'''[[Media: Mathlog_318_b18.pdf|Блок 18]]'''. Системы дизъюнктов.
  
'''[[Media: Mathlog_318_lecture_14_15.pdf|Лекция 14-15.]]''' Модальные логики. Эпистемические логики. Темпоральные логики. Логика линейного времени (LTL). Логика деревьев вычислений (CTL). Верификация распределённых систем. Задача верификации для LTL. Табличный алгоритм верификации для LTL.
+
'''[[Media: Mathlog_318_b19.pdf|Блок 19]]'''. Композиция подстановок. Постановка задачи унификации.
  
== Временный архив слайдов: 2016-2017 учебный год ==
+
'''[[Media: Mathlog_318_b20.pdf|Блок 20]]'''. Алгоритм унификации атомарных формул логики предикатов.
  
'''[[Media: Mathlog_318_lecture_14.pdf|14]]''',
+
'''[[Media: Mathlog_318_b21.pdf|Блок 21]]'''. Резолютивный вывод. Корректность резолютивного вывода.
'''[[Media: Mathlog_318_lecture_16_17.pdf|16-17]]'''.
+
  
= Семинары =
+
'''[[Media: Mathlog_318_b22.pdf|Блок 22]]'''. Обоснование общезначимости формулы методом резолюций (пример).
  
''Материалы семинаров будут обновляться по мере проведения занятий''
+
'''[[Media: Mathlog_318_b23.pdf|Блок 23]]'''. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях.
  
Семинары 1-4 проводятся по [[Media:MatLog_tasks.pdf| этому сборнику задач.]]
+
'''[[Media: Mathlog_318_b24.pdf|Блок 24]]'''. Теорема Эрбрана. Полнота резолютивного вывода.
  
Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]]
+
'''[[Media: Mathlog_318_b25.pdf|Блок 25]]'''. Метод резолюций: заключительный пример.
  
[[Media:Mllp_318_seminar_definability.pdf| Материалы семинара 5 (выразимость).]]
+
'''[[Media: Mathlog_318_b26.pdf|Блок 26]]'''. Как устроены математические доказательства. Логические исчисления.
  
[[Media:Mathlog_318_seminar_natural_inference.pdf| Материалы семинара 6 (натуральное исчисление).]]
+
'''[[Media: Mathlog_318_b27.pdf|Блок 27]]'''. Натуральное исчисление высказываний: основные определения.
  
= Контрольная работа =
+
'''[[Media: Mathlog_318_b28.pdf|Блок 28]]'''. Натуральное исчисление высказываний: правило монотонности, закон исключённого третьего, корректность.
  
Формат проведения и длительность контрольной работы: письменно, 95 минут.
+
'''[[Media: Mathlog_318_b29.pdf|Блок 29]]'''. Натуральное исчисление высказываний: правило сечения, правило полного перебора, правило приведения к абсурду, полнота.
  
В рамках контрольной работы требуется решить
+
'''[[Media: Mathlog_318_b30.pdf|Блок 30]]'''. Натуральное исчисление предикатов: основные определения, корректность.
  
* '''три задачи''':
+
'''[[Media: Mathlog_318_b31.pdf|Блок 31]]'''. Гильбертовское исчисление предикатов. Теорема Гёделя о полноте (формулировка).
** построить формулу логики предикатов, адекватно описывающую высказывание, записанное на естественном языке;
+
** проверить общезначимость формулы логики предикатов, используя метод семантических таблиц
+
*** (правила табличного вывода будут выданы вместе с заданием контрольной);
+
** проверить общезначимость формулы логики предикатов, используя метод резолюций;
+
* '''девять теоретических вопросов''', проверяющих знание материала, изложенного в лекциях 2-9.
+
  
Контрольная работа оценивается по шкале '''от 0 до 15 баллов'''.
+
'''[[Media: Mathlog_318_b32.pdf|Блок 32]]'''. Натуральное исчисление предикатов: полнота.
Итоговые баллы за работу - это сумма баллов за задачи и теоретические вопросы.
+
  
Правильно решённая задача оценивается в '''2 балла'''.
+
'''[[Media: Mathlog_318_b33.pdf|Блок 33]]'''. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.
Задача, решённая с ошибками, может быть оценена числом баллов от 0 до 2 в зависимости от качества и количества ошибок.
+
  
Правильно решённый теоретический вопрос оценивается в '''1 балл'''.
+
'''[[Media: Mathlog_318_b34.pdf|Блок 34]]'''. Машины Тьюринга (МТ). Проблема останова МТ.
В каждом теоретическом вопросе предлагается несколько вариантов ответа.
+
Среди этих ответов может быть один, ни одного или несколько правильных.
+
Для правильного решения теоретического вопроса следует отметить '''все''' правильные ответы и только их.
+
Обоснование того, почему выбраны или не выбраны те или иные ответы, '''не требуется'''.
+
  
'''Группа 241:''' баллы, набранные за контрольную работу, суммируются с другими баллами, требуемыми для получения зачёта.
+
'''[[Media: Mathlog_318_b35.pdf|Блок 35]]'''. Теорема Чёрча.
  
'''Группа 318:''' по результатам контрольной работы определяется <span style="background:#DDFFDD">бонус</span> или <span style="background:#FFDDDD">штраф</span>, суммирующийся с баллами за экзаменационную работу:
+
'''[[Media: Mathlog_318_b36.pdf|Блок 36]]'''. Аксиоматические теории первого порядка. Проблема общезначимости формул в теории.
* набрано хотя бы 14 баллов: бонус <span style="background:#DDFFDD">+3 балла</span>;
+
* набрано хотя бы 12, но менее 14 баллов: бонус <span style="background:#DDFFDD">+2 балла</span>;
+
* набрано хотя бы 10, но менее 12 баллов: бонус <span style="background:#DDFFDD">+1 балл</span>;
+
* набрано хотя бы 8, но менее 10 баллов: бонус <span style="background:#DDFFDD">+0 баллов</span>;
+
* набрано хотя бы 6, но менее 8 баллов: штраф <span style="background:#FFDDDD">-1 балл</span>;
+
* набрано хотя бы 4, но менее 6 баллов: штраф <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>.
+
  
= Экзамен =
+
'''[[Media: Mathlog_318_b37.pdf|Блок 37]]'''. Основные свойства аксиоматических теорий.
  
Формат проведения и длительность экзамена: письменно, 120 минут.
+
'''[[Media: Mathlog_318_b38.pdf|Блок 38]]'''. Арифметические интерпретации и теории.
  
Экзаменационная работа оценивается по шкале '''от 0 до 30 баллов''' (''промежуточные баллы'').
+
'''[[Media: Mathlog_318_b39.pdf|Блок 39]]'''. Определения и выразимость.
Итоговые баллы за экзаменационную работу - это сумма промежуточных баллов, бонусов и штрафов по итогам контрольной работы, а также других бонусов, если удалось их получить.
+
В зависимости от полученных итоговых баллов за экзаменационную работу выставляется оценка за экзамен:
+
* набрано хотя бы 24 балла: '''отлично''';
+
* набрано хотя бы 18, но менее 24 баллов: '''хорошо''';
+
* набрано хотя бы 12, но менее 18 баллов: '''удовлетворительно''';
+
* набрано менее 12 баллов: '''неудовлетворительно'''.
+
  
Промежуточные баллы складываются из баллов, полученных за решение каждой задачи в работе.
+
'''[[Media: Mathlog_318_b40.pdf|Блок 40]]'''. Формальная арифметика. Теорема Гёделя о неполноте.
Описание задач и оценки за их безошибочное решение:
+
* '''Задача 1 (3 балла)''': предложить формулу логики предикатов, адекватно описывающую заданное утверждение, записанное на естественном языке.
+
* '''Задача 2 (3 балла)''': проверить общезначимость формулы логики предикатов методом семантических таблиц.
+
* '''Задача 3 (3 балла)''': проверить общезначимость формулы логики предикатов методом резолюций.
+
* '''Задача 4 (3 балла)''': предложить аксиому, определяющую арифметическое понятие в заданной сигнатуре.
+
* '''Задача 5 (3 балла)''': предложить доказательство формулы в натуральном исчислении предикатов.
+
* '''Задачи 6-8 (2 балла за каждую)''' состоят из двух частей: а) сформулировать теорему или определение, рассказанные в лекциях; б) ответить на вопрос, так или иначе связанный с первой частью, '''без пояснений''' (как правило - "да" или "нет", либо привести какой-либо пример).
+
* '''Задачи 9-11 (3 балла за каждую)''': из предложенных вариантов ответа на заданный вопрос выбрать правильные (один, несколько или ни одного), правильность каждого выбранного ответа обосновать ('''невыбранные ответы обосновывать не нужно''').
+
  
= Зачёт =
+
'''[[Media: Mathlog_318_b41.pdf|Блок 41]]'''. Арифметика Пресбургера.
  
После завершения лекций будет проведена вторая контрольная работа. Эта работа будет содержать
+
'''[[Media: Mathlog_318_b42.pdf|Блок 42]]'''. Модальные логики.
* Две задачи, идентичные задачам 4, 5 экзамена, каждая из которых оценивается в 2 балла.
+
* Пять теоретических вопросов по лекциям, проведённым после контрольной работы, аналогичные теоретическим вопросам первой контрольной работы. Каждый теоретический вопрос оценивается в 1 балл.
+
  
Для получения зачёта необходимо набрать не менее '''16 баллов''' по итогам двух контрольных работ и сдачи других заданий.
+
'''[[Media: Mathlog_318_b43.pdf|Блок 43]]'''. Эпистемические логики.
  
Не получившим зачёт по результатам второй контрольной работы будут предоставлены дополнительные попытки получения зачёта. На этих попытках:
+
'''[[Media: Mathlog_318_b44.pdf|Блок 44]]'''. Темпоральные логики.
* Сохраняются баллы за каждую задачу, суммарный балл за теоретические вопросы первой контрольной работы, суммарный балл за теоретические вопросы второй контрольной работы.
+
* Предоставляется возможность поднять каждый из этих баллов, решив соответствующие части новых вариантов контрольных работ.
+
  
= Дополнительные бонусы к экзамену и зачёту =
+
'''[[Media: Mathlog_318_b45.pdf|Блок 45]]'''. Что ещё интересного есть в логике. Формальная верификация.
  
Общее условие сдачи задач на дополнительные бонусы:
+
'''[[Media: Mathlog_318_b46.pdf|Блок 46]]'''. Императивные программы. Формальная верификаци программ. Логика Хоара.
* принцип сдачи задач:
+
** идеи и выкладки, не требующие технических деталей, - устно;
+
** если выкладки не воспроизводятся или не воспринимаются устно, то письменно;
+
* при подготовке и сдаче можно пользоваться любыми материалами;
+
* при сдаче проверяется понимание каждой детали решения задачи - следует быть к этому готовым;
+
* задача считается решённой, если не осталось неотвеченных вопросов по обоснованию всех шагов решения задачи.
+
  
'''Бонусы за решение задач сформулированы для одной учебной группы''' и получаются внутри одной группы независимо от другой (например, "''первый предоставивший решение''" трактуется как "''первый предоставивший решение из группы 318, а также первый предоставивший решение из группы 241''".
+
'''[[Media: Mathlog_318_b47.pdf|Блок 47]]'''. Проверка моделей относительно логики деревьев вычислений (CTL model checking).
  
''Задачи будут появляться по мере проведения занятий''
+
== Слайды прошлых лет ==
  
== Полнота табличного вывода в логике предикатов ==
+
'''[[Media: Mathlog_318_lecture_1.pdf|Лекция]]''' (вводная). Что такое логика? Содержание лекций. История логики. Логические парадоксы.
  
=== Описание задачи ===
+
'''[[Media: Mathlog_318_lecture_2.pdf|Лекция.]]''' Логика высказываний: синтаксис, семантика, выполнимость, общезначимость. Метод семантических таблиц в логике высказываний.
  
Адаптировать доказательство теоремы о полноте табличного вывода в логике предикатов к более общему случаю:
+
'''[[Media: Mathlog_318_lecture_3.pdf|Лекция.]]''' Логика предикатов: синтаксис (термы, формулы), семантика (интерпретации, отношение выполнимости).
* сигнатура алфавита состоит из
+
** не более чем счётно-бесконечного числа констант,
+
** не более чем счётно-бесконечного числа функциональных символов каждой местности,
+
** не более чем счётно-бесконечного числа предикатных символов каждой местности;
+
* формулы исходной таблицы могут содержать свободные переменные;
+
* исходная таблица содержит не более чем счётно-бесконечное число формул.
+
  
Бонусы за решение задачи:
+
'''[[Media: Mathlog_318_lecture_4_5.pdf|Лекция.]]''' Выполнимые и общезначимые формулы. Модели. Логическое следствие. Проблема общезначимости формул. Подстановки. Метод семантических таблиц в логике предикатов. Корректность табличного вывода.
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+3 балла</span>
+
* '''второй''' и '''третий''' предоставившие решение: <span style="background:#DDFFDD">+2 балла</span>
+
  
=== Количество предоставленных решений ===
+
'''[[Media: Mathlog_318_lecture_6.pdf|Лекция.]]''' Полнота табличного вывода в логике предикатов. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Равносильные формулы. Теорема о равносильной замене.
  
'''Группа 318:''' 0
+
'''[[Media: Mathlog_318_lecture_7.pdf|Лекция.]]''' Общая схема метода резолюций. Предварённая нормальная форма. Сколемовская стандартная форма. Системы дизъюнктов. Задача унификации.
  
'''Группа 241:''' 0
+
'''[[Media: Mathlog_318_lecture_8.pdf|Лекция.]]''' Алгоритм унификации атомарных формул. Теорема об унификации.
  
== Утверждения об отношении равносильности ==
+
'''[[Media: Mathlog_318_lecture_9.pdf|Лекция.]]''' Резолютивный вывод. Корректность резолютивного вывода. Применение метода резолюций. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях. Теорема Эрбрана.
  
=== Описание задачи ===
+
'''[[Media: Mathlog_318_lecture_10.pdf|Лекция.]]''' Полнота резолютивного вывода. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.
  
Обосновать утверждения об отношении равносильности в лекции 6 с доказательством, помеченным словом "Самостоятельно".
+
'''[[Media: Mathlog_318_lecture_11.pdf|Лекция.]]''' Машины Тьюринга. Теорема Чёрча. Как устроены математические доказательства. Логические исчисления.
  
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение задачи
+
'''[[Media: Mathlog_318_lecture_12_13.pdf|Лекция.]]''' Натуральное исчисление высказываний. Натуральное исчисление предикатов. Исчисление предикатов гильбертовского типа.
  
=== Количество предоставленных решений ===
+
'''[[Media: Mathlog_318_lecture_14.pdf|Лекция.]]''' Модальные логики. Эпистемические логики. Темпоральные логики.
  
'''Группа 318:''' 1
+
'''[[Media: Mathlog_318_lecture_15.pdf|Лекция.]]''' Формальная верификация программ. Императивные программы. Корректность императивных программ. Логика Хоара. Автоматизация проверки правильности программ.
  
'''Группа 241:''' 1
+
'''[[Media: Mathlog_318_lecture_16.pdf|Лекция.]]''' Верификация распределённых систем. Логика линейного времени (LTL). Размеченные системы переходов. Задача верификации (model checking) для LTL.
  
== Фундированность троек чисел ==
+
'''[[Media: Mathlog_318_lecture_17.pdf|Лекция.]]''' Табличный алгоритм верификации для LTL. Замыкание Фишера-Ладнера. Системы Хинтикки.
  
=== Описание задачи ===
+
'''[[Media: Mathlog_318_lecture_11_12.pdf|Лекция.]]''' Аксиоматические теории. Основные свойства теорий. Формальная арифметика. Арифметика Пеано. Теорема Гёделя о неполноте. Определимость. Арифметика Пресбургера.
  
Доказать фундированность троек неотрицательных целых чисел относительно лексикографического порядка (лемма в лекции 7, сформулированная в рамках доказательства завершаемости алгоритма унификации, обоснование которой помечено словами "Попробуйте сами").
+
'''[[Media: Mathlog_318_lecture_16_17.pdf|Лекция.]]'''.
  
Бонусы за решение задачи:
+
= Семинары =
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+2 балла</span>
+
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+1 балл</span>
+
  
=== Количество предоставленных решений ===
+
''Материалы семинаров будут обновляться по мере проведения занятий''
  
'''Группа 318:''' 1
+
Семинары 1-4 проводятся по [[Media:MatLog_tasks.pdf| этому сборнику задач.]]
  
'''Группа 241:''' 2 (все баллы розданы)
+
Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]]
  
== Изоморфизм и элементарная эквивалентность интерпретаций ==
+
[[Media:Mathlog_318_seminar_natural_inference.pdf| Материалы семинара 5 (натуральное исчисление).]]
  
=== Описание задачи ===
+
[[Media:Mllp_318_seminar_definability.pdf| Материалы семинара 6 (выразимость).]]
  
Доказать утверждение на слайде 24 лекции 10 о соотношении понятий изоморфизма и элементарной эквивалентности интерпретаций.
+
= Экзамен =
  
Бонусы за решение задачи:
+
Формат проведения и длительность экзамена: письменно, 120 минут.
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+2 балла</span>
+
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+1 балл</span>
+
  
=== Количество предоставленных решений ===
+
Экзаменационная работа оценивается по шкале от 0 до 33 технических баллов.
 +
К оценке за эту работу прибавляются технические баллы, полученные за работу в семестре (выполнение премиальных задач).
 +
Согласно набранной сумме технических баллов выставляется оценка:
 +
* хотя бы 27: '''отлично''';
 +
* хотя бы 21, но менее 27: '''хорошо''';
 +
* хотя бы 15, но менее 21: '''удовлетворительно''';
 +
* менее 15: '''неудовлетворительно'''.
  
'''Группа 318:''' 0
+
Баллы за экзаменационную работу складываются из баллов за каждую задачу, предложенную в работе:
 +
* Каждая из задач 1-5 оценивается в 3 балла. Темы задач:
 +
*# Формализовать в логике предикатов предложение, записанное на естественном языке.
 +
*# Проверить общезначимость формулы логики предикатов методом семантических таблиц.
 +
*# Проверить общезначимость формулы логики предикатов методом резолюций.
 +
*# Доказать общезначимость формулы логики предикатов в натуральном исчислении.
 +
*# Предложить аксиому, определяющую заданное понятие в заданной интерпретации.
 +
* Каждая из задач 6-8 оценивается в 2 балла и состоит из двух частей:
 +
*# Сформулировать утверждение, определение и т.п.
 +
*# Ответить на вопрос "на понимание", так или иначе связанный с формулировкой.
 +
* Каждая из задач 9-12 оценивается в 3 балла и устроена так:
 +
** Из нескольких предложенных вариантов ответа выбрать правильные (один, несколько или ни одного) и '''обосновать''' выбранные ответы.
 +
** Невыбранные ответы обосновывать не нужно.
  
'''Группа 241:''' 0
+
= Зачёт =
  
== Теорема Гёделя о неполноте ==
+
На зачёте оцениваются результаты, относящиеся к решению типовых задач, знанию теории и работе в семестре.
  
=== Описание задачи ===
+
В курсе встретится 5 типовых задач:
 +
# Формализовать в логике предикатов предложение, записанное на естественном языке.
 +
# Проверить общезначимость формулы логики предикатов методом семантических таблиц.
 +
# Проверить общезначимость формулы логики предикатов методом резолюций.
 +
# Доказать общезначимость формулы логики предикатов в натуральном исчислении.
 +
# Предложить аксиому, определяющую заданное понятие в заданной интерпретации.
  
Доказать теорему Гёделя о неполноте ('''лекция 10'''): либо адаптировать доказательство в лекции к общему случаю и доказать лемму о диагонали и утверждение об арифметизуемости графика, либо предоставить независимое доказательство.
+
При проставлении зачёта учитывается 7 технических оценок:
 +
* Пять оценок за типовые задачи, по одной за каждую задачу. Максимальная оценка за каждую задачу - 3 балла.
 +
* Оценка за знание теории. Максимум - 15 баллов.
 +
* Оценка за решение премиальных задач.
  
Бонусы за решение задачи:
+
Для получения зачёта требуется достичь следующих результатов:
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+14 баллов</span>
+
# Хорошо решить типовые задачи:
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+11 баллов</span>
+
#* четыре задачи не менее чем на 2 балла, или
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+8 баллов</span>
+
#* две задачи на 3 балла и одну задачу на не менее чем 2 балла.
 +
#** "3 балла" = "правильно"
 +
#** "не менее чем 2 балла" = "правильно или с незначительными недочётами"
 +
# Набрать хотя бы 20 баллов суммарно за всё (типовые задачи, теория, премиальные задачи).
  
=== Количество предоставленных решений ===
+
В курсе планируются две контрольные работы: первая - в середине семестра, вторая - после завершения лекций.
 +
Контрольные работы и попытки зачёта проводятся письменно, длительность каждого мероприятия - 90 минут (одна пара).
  
'''Группа 318:''' 0
+
== Сдача типовых задач ==
  
'''Группа 241:''' 2
+
Для решения каждой типовой задачи будет предложено несколько попыток.
 +
При проставлении зачёта учитывается '''максимальная''' оценка за задачу среди всех попыток её решить.
  
== Арифметика Пресбургера и математическая индукция ==
+
На первой контрольной работе будут предложены типовые задачи 1-3.
 +
На второй контрольной работе и на каждой попытке зачёта будут предложены все типовые задачи.
  
=== Описание задачи ===
+
== Сдача теории ==
 +
 
 +
Теоретические вопросы даются в форме теста с множественным выбором: из предложенных вариантов ответа требуется выбрать правильные (один, несколько или ни одного), обоснование не требуется.
 +
Правильно решённый теоретический вопрос оценивается в 1 балл.
 +
 
 +
На первой контрольной работе будет предложено 9 теоретических вопросов.
 +
На второй контрольной работе будет предложено 6 теоретических вопросов.
 +
Оценка за знание теории складывается из оценок за эти 15 теоретических вопросов.
 +
 
 +
На каждой попытке зачёта также будет предложено 15 теоретических вопросов.
 +
При проставлении зачёта учитывается '''максимальная''' оценка среди полученных за контрольные работы и за каждую из попыток зачёта.
 +
 
 +
= Премиальные задачи =
 +
 
 +
''По ходу проведения курса в подразделах этого раздела будут появляться премиальные задачи''
 +
 
 +
Общие условия сдачи решений премиальных задач:
 +
* Можно как прислать письменное решение, так и обсудить решение устно. Если прислано письменное решение и к нему есть вопросы, то для их решения может потребоваться дополнительное устное обсуждение.
 +
* При подготовке решения и во время его сдачи можно пользоваться любыми материалами.
 +
* При сдаче может быть проверено понимание '''каждой''' детали предложенного решения - следует быть к этому готовым.
 +
* Решение принимается, когда по нему не остаётся неотвеченных вопросов.
  
Указать все места в доказательстве разрешимости арифметики Пресбургера ('''лекция 11'''), в которых существенно используется наличие схемы аксиом индукции в этой арифметике, и объяснить способ использования.
+
'''Бонусы за решение задач сформулированы для одной учебной группы''' и получаются внутри одной группы независимо от другой.
 +
Например, "''первый''" трактуется как "''первый из группы 318, а также первый из группы 319/2, а также ...''".
 +
 
 +
== (1) Свойства семантических таблиц в логике высказываний ==
 +
 
 +
Доказать три утверждения в блоке 7, доказательство которых помечено словами "А попробуйте сами", '''или''' два утверждения в блоке 8, помеченные теми же словами.
 +
 
 +
Бонус за решение задачи: <span style="background:#DDFFDD">+1 балл</span> первым '''двум''' предоставившим решение задачи
 +
 
 +
== (2) Полнота табличного вывода в логике предикатов ==
 +
 
 +
Адаптировать доказательство теоремы о полноте табличного вывода в логике предикатов к более общему случаю:
 +
* сигнатура алфавита состоит из
 +
** не более чем счётного числа констант,
 +
** не более чем счётного числа функциональных символов произвольных местностей,
 +
** не более чем счётного числа предикатных символов произвольных местностей;
 +
* формулы исходной таблицы могут содержать свободные переменные;
 +
* исходная таблица содержит не более чем счётное число формул.
  
 
Бонусы за решение задачи:
 
Бонусы за решение задачи:
* '''первый''' предоставивший решение: <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>
+
  
=== Количество предоставленных решений ===
+
== (3) Утверждения об отношении равносильности ==
  
'''Группа 318:''' 0
+
Обосновать два утверждения об отношении равносильности в блоке 15, помеченные словами "Попробуйте самостоятельно" рядом со словом "Доказательство".
  
'''Группа 241:''' 0
+
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение задачи
  
== Определение экспоненты ==
+
== (4) Сколемизация ==
  
=== Описание задачи ===
+
Обосновать или опровергнуть
 +
* необходимость ("=>") и
 +
* достаточность ("<=")
 +
теоремы о сколемизации, в которой свойство выполнимости заменено на свойство общезначимости (как сказано в вопросе под теоремой).
  
Предложить (с обоснованием) определение одноместной функции 2^x (два в степени икс) в арифметической интерпретации на целых неотрицательных числах с сигнатурой <{0}, {+, x, s}, {=}> (семинар 5, задача 1, пункт 19).
+
Бонус за решение задачи:
 +
* '''первый''' сдавший: <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">+5 баллов</span>
+
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+4 балла</span>
+
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+3 балла</span>
+
  
=== Количество предоставленных решений ===
+
== (7) Фундированность троек чисел ==
  
'''Группа 318:''' 1
+
Доказать фундированность троек неотрицательных целых чисел относительно лексикографического порядка (лемма в блоке 20, обоснование которой помечено словами "Попробуйте сами").
  
'''Группа 241:''' 0
+
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение задачи
  
== Теорема Гёделя о полноте ==
+
== (8) Про эрбрановские интерпретации ==
  
=== Описание задачи ===
+
Останется ли справедливой теорема об эрбрановских интерпретациях, если вместо "Система дизъюнктов" в её формулировке написать "Формула логики предикатов"?
 +
Ответ обосновать.
 +
 
 +
Бонус за решение задачи:
 +
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
 +
* '''второй''' сдавший: <span style="background:#DDFFDD">+2 балла</span>
 +
 
 +
== (9) Полная стратегия построения успешного резолютивного вывода ==
 +
 
 +
Предложить (с обоснованием) список правил построения резолютивного вывода, гарантирующих получение пустого дизъюнкта из конечной невыполнимой системы дизъюнктов.
  
Доказать теорему Гёделя о полноте (см. '''лекцию 13''').
+
(Как это делалось, например, в доказательстве теоремы о полноте табличного вывода.)
  
 
Бонусы за решение задачи:
 
Бонусы за решение задачи:
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+9 баллов</span>
+
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+6 баллов</span>
+
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+6 баллов</span>
+
  
=== Количество предоставленных решений ===
+
== (10) Вычислительные возможности метода резолюций ==
  
'''Группа 318:''' 0
+
Ответить (с обоснованием и для достаточно широкого семейства резолютивных выводов) на вопрос, поставленный в конце "заключительного примера для метода резолюций" блока 25.
  
'''Группа 241:''' 0
+
Бонусы за решение задачи:
 +
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
 +
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
  
<!--
+
== (11) Исчисление семантических таблиц ==
  
== Полнота семантической резолюции ==
+
Определить (с пояснениями) аксиомы и правила вывода логического исчисления со следующими свойствами:
 +
* формулы исчисления - семантические таблицы логики предикатов;
 +
* таблица доказуема в исчислении тогда и только тогда, когда для неё существует успешный табличный вывод;
 +
* из доказательства для таблицы T в исчислении можно получить успешный табличный вывод для T, расположив таблицы в вершинах дерева согласно применению правил исчисления.
  
=== Описание задачи ===
+
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение задачи
  
Доказать теорему полноты семантической резолюции (лекция 9).
+
== (12) Корректность натурального исчисления предикатов ==
 +
 
 +
Выбрать одно из четырёх правил вывода НИП для кванторов (введение/удаление существования/всеобщности) и обосновать корректность этого правила согласно разобранному в доказательстве теоремы о корректности НИВ.
 +
 
 +
Для каждого из правил принимается только одно решение, и от одного студента принимается решение только для одного правила.
 +
Бонус за решение: <span style="background:#DDFFDD">+1 балл</span>
 +
 
 +
== (13) Теорема Гёделя о полноте ==
 +
 
 +
Доказать теорему Гёделя о полноте, сформулированную в блоке 31, для исчисления, изложенного в этом же блоке.
  
 
Бонусы за решение задачи:
 
Бонусы за решение задачи:
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+3 балла</span>
+
* '''первый''' сдавший: <span style="background:#DDFFDD">+10 баллов</span>
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+2 балла</span>
+
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+7 баллов</span>
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+1 балла</span>
+
  
=== Количество предоставленных решений ===
+
== (14) Непротиворечивая конечная полная теория ==
  
'''Группа 318:''' 0
+
Привести пример (с обоснованием) непротиворечивой конечной полной аксиоматической теории первого порядка.
  
'''Группа 241:''' 0
+
Бонус за решение задачи:
 +
* '''первый''' сдавший: <span style="background:#DDFFDD">+2 балла</span>
 +
* '''второй''' сдавший: <span style="background:#DDFFDD">+1 балл</span>
  
== Свойства шкал Крипке ==
+
== (15) О подстановке определения ==
  
=== Описание задачи ===
+
Оформить пропущенные части доказательства теоремы о подстановке определения: доказательство для функции кси и часть доказательства, скрытая в отсылке к теореме о равносильной замене.
  
Доказать утверждения о рефлексивности, транзитивности и симметричности шкал Крипке, сформулированные в разделе "Эпистемические логики" '''лекции 14-15'''  
+
Бонус за решение задачи:
 +
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
 +
* '''второй''' сдавший: <span style="background:#DDFFDD">+2 балла</span>
  
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение.
+
== (16) Теорема Гёделя о неполноте ==
  
=== Количество предоставленных решений ===
+
Доказать теорему Гёделя о неполноте в формулировке, представленной в блоке 40: либо адаптировать представленный там эскиз доказательства к общему случаю и доказать леммы об арифметизации и о диагонали, либо предоставить независимое доказательство.
  
'''Группа 318:''' 1
+
Бонусы за решение задачи:
 +
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+14 баллов</span>
 +
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+11 баллов</span>
 +
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+8 баллов</span>
  
'''Группа 241:''' 2 (''решения больше не принимаются'')
+
== (17) Арифметика Пресбургера ==
  
== Мудрецы ==
+
Доказать полноту системы аксиом арифметики Пресбургера, представленной на последнем слайде блока 41.
  
=== Описание задачи ===
+
Бонусы за решение задачи:
 +
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+4 балла</span>
 +
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+3 балла</span>
 +
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+2 балл</span>
  
Описать и содержательно пояснить законы рассуждений и ход рассуждений мудрецов в ''задаче о трёх мудрецах'' ('''лекция 14-15''') в терминах эпистемической логики.
+
== (18) Определение экспоненты ==
  
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение.
+
Предложить (с обоснованием) определение одноместной функции 2^x (два в степени икс) в арифметической интерпретации на целых неотрицательных числах с сигнатурой <{0}, {+, x, s}, {=}> (семинар 5, задача 1, пункт 21).
  
=== Количество предоставленных решений ===
+
''Если в обосновании будут содержаться китайская теорема об остатках, малая теорема Ферма или что-либо другое нетривиальное, то обоснование этого - часть решения''
  
'''Группа 318:''' 0
+
Бонусы за решение задачи:
 +
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+4 баллов</span>
 +
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+3 балла</span>
 +
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+2 балла</span>
  
'''Группа 241:''' 0
+
== (19) Свойства шкал Крипке ==
  
== Законы темпоральных логик ==
+
Доказать утверждения о рефлексивности, транзитивности и симметричности шкал Крипке, сформулированные в блоке 43.
  
=== Описание задачи ===
+
Бонус за решение задачи:
 +
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
 +
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
  
* Выбрать один темпоральный оператор логики линейного времени.
+
== (20) Задача о трёх мудрецах ==
** Если выбран оператор U, то также выбрать ''право'' или ''лево''.
+
* Доказать или опровергнуть два закона дистрибутивности, сформулированные для выбранного оператора в '''лекции 14-15'''.
+
** Если выбран оператор U, то это два закона дистрибутивности для ''правого'' или ''левого'' аргумента, в зависимости от сделанного выбора.
+
  
Бонус за решение задачи: <span style="background:#DDFFDD">+1 балл</span> '''каждому''' предоставившему решение.
+
Записать и пояснить ход рассуждений мудрецов в ''задаче о трёх мудрецах'', представленной в конце блока 43, в терминах эпистемической логики.
  
Ограничение: доказательство или опровержение каждого закона дистрибутивности принимается только один раз.
+
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''трём''' предоставившим решение.
  
=== Операторы, для которых решения уже предоставлены ===
+
== (21) Корректность логики Хоара ==
  
'''Группа 318:''' -
+
Доказать корректность одного из правил логики Хоара ('''блок 46, лемма о корректности правил'''), кроме правил для пустой команды и для присваивания.
  
'''Группа 241:''' '''F'''
+
Для каждого из правил принимается только одно решение, и от одного студента принимается решение только для одного правила.
 +
Бонус за решение: <span style="background:#DDFFDD">+2 балла</span>
  
== Табличный алгоритм верификации для LTL ==
+
== (22) Слабейшие предусловия ==
  
=== Описание задачи ===
+
Доказать теорему о слабейшем предусловии ('''лекция 15''').
  
Ответить на существенную часть вопросов, сформулированных на последнем слайде '''лекции 14-15'''
+
Бонусы за решение задачи:
 +
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
 +
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
  
Бонус за решение задачи: '''обсуждается индивидуально'''.
+
== (23) Упрощение ctl-формул ==
  
 +
Доказать один из зелёных пунктов утверждения об упрощении ctl-формул в '''блоке 47'''.
  
== Теорема о разрешимости доопределения теории ==
+
Для каждого пункта принимается только одно решение, и от одного студента принимается решение только для одного пункта.
 +
Бонус за решение: <span style="background:#DDFFDD">+1 балл</span>
  
=== Описание задачи ===
+
== (24) Алгоритм проверки выполнимости ctl-формулы на системе переходов ==
  
Завершить доказательство этой теоремы, предложенное в '''лекции 11''', или предложить своё доказательство
+
Ответить (с обоснованием) на вопрос в самом конце '''блока 47''' о корректности и сложности алгоритма проверки выполнимости ctl-формулы на системе переходов. 
  
 
Бонусы за решение задачи:
 
Бонусы за решение задачи:
* '''первый''' предоставивший решение: <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">+1 балл</span>
+
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+2 балла</span>
  
=== Количество предоставленных решений ===
+
<!--
  
'''Группа 318:''' 0
+
== (14) Табличный алгоритм верификации для LTL ==
  
<s>'''Группа 241:''' 0</s> (''уже не актуально'')
+
Ответить на существенную часть вопросов, сформулированных на последнем слайде последней лекции (17)
  
== Логика Хоара ==
+
Бонус за решение задачи: '''обсуждается индивидуально'''.
 +
-->
 +
 
 +
<!--
 +
== Полнота семантической резолюции ==
  
 
=== Описание задачи ===
 
=== Описание задачи ===
  
Доказать корректность одного из правил логики Хоара ('''лекция 16-17''').
+
Доказать теорему полноты семантической резолюции (лекция 9).
  
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> за доказательство корректности каждого правила, кроме SKIP и AS. За задачу можно получить '''не более двух баллов'''. Доказательство корректности каждого правила принимается '''не более одного раза''' в группе.
+
Бонусы за решение задачи:
 +
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+3 балла</span>
 +
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+2 балла</span>
 +
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+1 балла</span>
  
 
=== Количество предоставленных решений ===
 
=== Количество предоставленных решений ===
Строка 396: Строка 466:
 
'''Группа 318:''' 0
 
'''Группа 318:''' 0
  
<s>'''Группа 241:''' INF, IF</s> (''уже не актуально'')
+
'''Группа 241:''' 0
  
 
== Законы темпоральной логики ==
 
== Законы темпоральной логики ==
Строка 424: Строка 494:
 
= Программа курса =
 
= Программа курса =
  
''Программа будет уточняться по мере проведения занятий''
+
''Программа будет обновляться по ходу чтения курса''
  
 
== Классические логики ==
 
== Классические логики ==
Строка 451: Строка 521:
 
</ol>
 
</ol>
  
== Аксиоматические теории и исчисления ==
+
== Логические исчисления ==
 
<ol start="18">
 
<ol start="18">
<li> Аксиомы, теоремы и теории. Выполнимость, противоречивость и общезначимость формул в теории. Проблема общезначимости формул логики предикатов в теории.
+
<li> Логические исчисления. Исчисления высказываний и исчисления предикатов. Доказуемость (выводимость) формул.
<li> Основные свойства интерпретаций: непротиворечивость, полнота, разрешимость, адекватность интерпретациям.
+
<li> Натуральное исчисление высказываний. Корректность и полнота исчисления.
<li> Формальная арифметика. Арифметика Пеано. Теорема Гёделя о неполноте.
+
<li> Натуральное исчисление предикатов. Корректность и полнота исчисления.
<li> Выразимость символов сигнатуры в интерпретациях. Теорема о расширении теории. Теорема о подстановке определения.
+
<li> Арифметика Пресбургера.
+
<li> Логические исчисления. Исчисления предикатов. Доказуемость (выводимость) формул.
+
<li> Исчисление высказываний гильбертовского типа. Корректность и полнота исчисления.
+
 
<li> Исчисление предикатов гильбертовского типа. Теорема Гёделя о полноте.
 
<li> Исчисление предикатов гильбертовского типа. Теорема Гёделя о полноте.
<li> Натуральное исчисление высказываний. Корректность и полнота исчисления.
 
<li> Натуральное исчисление предикатов. Корректность и полнота исчисления. Натуральный вывод формул.
 
 
</ol>
 
</ol>
  
 
== Неклассические прикладные логики ==
 
== Неклассические прикладные логики ==
<ol start="28">
+
<ol start="22">
 
<li> Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики. Логика линейного времени. Логика деревьев вычислений.
 
<li> Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики. Логика линейного времени. Логика деревьев вычислений.
<li> Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Корректность и частичная корректность программ. Тройки Хоара. Логика Хоара. Теорема корректности вывода в логике Хоара. Слабейшее предусловие. Инвариант цикла.
+
<li> Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Корректность и частичная корректность программ. Тройки Хоара. Логика Хоара. Корректность вывода в логике Хоара. Слабейшее предусловие. Инвариант цикла.
 
<li> Верификация распределённых систем. Логика линейного времени: синтаксис, семантика. Основные равносильности в логике линейного времени. Применение темпоральных логик для спецификации поведения распределённых систем.
 
<li> Верификация распределённых систем. Логика линейного времени: синтаксис, семантика. Основные равносильности в логике линейного времени. Применение темпоральных логик для спецификации поведения распределённых систем.
 
<li> Размеченные системы переходов. Моделирование программ системами переходов. Семантика чередующихся вычислений. Задача верификации (проверки моделей; model checking) для логики линейного времени.
 
<li> Размеченные системы переходов. Моделирование программ системами переходов. Семантика чередующихся вычислений. Задача верификации (проверки моделей; model checking) для логики линейного времени.
 
<li> Табличный алгоритм верификации для логики линейного времени. Упрощение формул. Замыкание Фишера-Ладнера. Согласованные предположения. Система Хинтикки. Сведение задачи верификации к графовым задачам.
 
<li> Табличный алгоритм верификации для логики линейного времени. Упрощение формул. Замыкание Фишера-Ладнера. Согласованные предположения. Система Хинтикки. Сведение задачи верификации к графовым задачам.
 
</ol>
 
</ol>
 
<!--
 
 
== Аксиоматические теории первого порядка ==
 
<ol start="21">
 
<li> Аксиомы. Аксиоматическая теория первого порядка: определение; выполнимость, общезначимость и противоречивость формул в теории. Проблемы общезначимости и выполнимости формул логики предикатов в теории.
 
<li> Основные свойства теорий: непротиворечивость, разрешимость, категоричность, полнота. Изоморфизм и элементарная эквивалентность интерпретаций. Связь изоморфизма интерпретаций, элементарной эквивалентности интерпретаций и полноты теорий.
 
<li> Теория частичных порядков. Теория равенства: непротиворечивость, разрешимость, некатегоричность.
 
<li> Исчисление предикатов: схемы аксиом, правило modus ponens, правило обобщения, логический вывод. Теорема Гёделя о полноте. Аксиоматические теории и исчисления.
 
<li> Формальная арифметика. Теорема Гёделя о неполноте. Нумерации Гёделя. Арифметизуемые отношения.
 
<li> Арифметика Пресбургера: непротиворечивость, разрешимость, полнота.
 
<li> Бескванторные теории первого порядка. Теории с равенством. Преимущества проблемы выполнимости формул в теории перед проблемой общезначимости.
 
<li> Теория равенства с неинтерпретируемыми функциями, разрешимость теории: сведение проблемы выполнимости в теории к проблеме выполнимости булевых формул.
 
<li> Линейная арифметика. Виды линейных арифметик. NP-полнота линейной целочисленной арифметики.
 
<li> Комбинация решающих алгоритмов для проблем выполнимости формул в теориях и в логике высказываний. Остовная проверка выполнимости формул в теориях. Интеграция алгоритмов проверки выполнимости формул в теориях в алгоритм DPLL.
 
</ol>
 
 
== Аксиоматическая теория множеств ==
 
<ol start="31">
 
<li> Наивная теория множеств. Сравнение мощностей множеств. Кардинальные числа в наивной теории множеств.
 
<li> Теорема Кантора. Теорема об объединении множества, неограниченного по мощности. Теорема Кантора-Бернштейна.
 
<li> Примеры кардинальных чисел. Конечность множеств мощности меньше счётной. Континуум-гипотеза в наивной теории множеств.
 
<li> Выразительные возможности наивной теории множеств: натуральные числа, кортежи, функции. Парадоксы теории множеств.
 
<li> Аксиоматические теории множеств. Теория Цермело-Френкеля: аксиомы и схемы аксиом, доказательство существования основных множеств наивной теории, исключение основных парадоксов теории множеств. Вопросы непротиворечивости теории Цермело-Френкеля.
 
<li> Определимость функций и отношений в теории. Применение определений для расширения теории.
 
<li> Аксиома выбора. Непротиворечивость теорий Цермело-Френкеля с аксиомой выбора и её отрицанием.
 
<li> Ординальные числа. Основные свойства ординальных чисел. Арифметика ординальных чисел.
 
<li> Теорема Цермело. Кардинальные числа в теории Цермело-Френкеля с аксиомой выбора.
 
<li> Континуум-гипотеза в теории Цермело-Френкеля с аксиомой выбора. Непротиворечивость теорий Цермело-Френкеля с аксиомой выбора и континуум-гипотезой, её отрицанием.
 
</ol>
 
 
== Неклассические прикладные логики ==
 
<ol start="41">
 
<li> Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики.
 
<li> Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Корректность и частичная корректность программ. Тройки Хоара. Логика Хоара. Теорема корректности вывода в логике Хоара.
 
<li> Верификация распределённых систем. Логика линейного времени: синтаксис, семантика. Основные равносильности в логике линейного времени. Применение темпоральных логик для спецификации поведения распределённых систем.
 
<li> Размеченные системы переходов. Моделирование программ системами переходов. Семантика чередующихся вычислений. Задача проверки выполнимости формул логики линейного времени на размеченных системах переходов.
 
<li> Позитивная форма формул логики линейного времени. Замыкание Фишера-Ладнера. Согласованные множества формул. Системы Хинтикки. Табличный метод проверки выполнимости формул логики линейного времени на размеченных системах переходов.
 
</ol>
 
 
-->
 
  
 
= Рекомендованная литература =
 
= Рекомендованная литература =

Текущая версия на 03:09, 17 мая 2021

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

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


Содержание

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

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

Блок 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. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.

Блок 34. Машины Тьюринга (МТ). Проблема останова МТ.

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

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

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

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

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

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

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

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

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

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

Блок 45. Что ещё интересного есть в логике. Формальная верификация.

Блок 46. Императивные программы. Формальная верификаци программ. Логика Хоара.

Блок 47. Проверка моделей относительно логики деревьев вычислений (CTL model checking).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Лекция..

Семинары

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

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

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

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

Материалы семинара 6 (выразимость).

Экзамен

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

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

  • хотя бы 27: отлично;
  • хотя бы 21, но менее 27: хорошо;
  • хотя бы 15, но менее 21: удовлетворительно;
  • менее 15: неудовлетворительно.

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

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

Зачёт

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

В курсе встретится 5 типовых задач:

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

При проставлении зачёта учитывается 7 технических оценок:

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

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

  1. Хорошо решить типовые задачи:
    • четыре задачи не менее чем на 2 балла, или
    • две задачи на 3 балла и одну задачу на не менее чем 2 балла.
      • "3 балла" = "правильно"
      • "не менее чем 2 балла" = "правильно или с незначительными недочётами"
  2. Набрать хотя бы 20 баллов суммарно за всё (типовые задачи, теория, премиальные задачи).

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

Сдача типовых задач

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

На первой контрольной работе будут предложены типовые задачи 1-3. На второй контрольной работе и на каждой попытке зачёта будут предложены все типовые задачи.

Сдача теории

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

На первой контрольной работе будет предложено 9 теоретических вопросов. На второй контрольной работе будет предложено 6 теоретических вопросов. Оценка за знание теории складывается из оценок за эти 15 теоретических вопросов.

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

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

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

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

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

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

(1) Свойства семантических таблиц в логике высказываний

Доказать три утверждения в блоке 7, доказательство которых помечено словами "А попробуйте сами", или два утверждения в блоке 8, помеченные теми же словами.

Бонус за решение задачи: +1 балл первым двум предоставившим решение задачи

(2) Полнота табличного вывода в логике предикатов

Адаптировать доказательство теоремы о полноте табличного вывода в логике предикатов к более общему случаю:

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

Бонусы за решение задачи:

  • первый сдавший: +3 балла
  • второй и третий сдавшие: +2 балла

(3) Утверждения об отношении равносильности

Обосновать два утверждения об отношении равносильности в блоке 15, помеченные словами "Попробуйте самостоятельно" рядом со словом "Доказательство".

Бонус за решение задачи: +2 балла первым двум предоставившим решение задачи

(4) Сколемизация

Обосновать или опровергнуть

  • необходимость ("=>") и
  • достаточность ("<=")

теоремы о сколемизации, в которой свойство выполнимости заменено на свойство общезначимости (как сказано в вопросе под теоремой).

Бонус за решение задачи:

  • первый сдавший: +3 балла
  • второй сдавший: +2 балла

(5) Первая головоломка о мощностях интерпретаций

Придумать (с обоснованием) необщезначимое предложение, истинное в любой интерпретации, содержащей не более чем 4 предмета.

Бонус за решение задачи: +2 балла первым двум предоставившим решение задачи

(6) Вторая головоломка о мощностях интерпретаций

Доказать, что если предложение истинно в любой интерпретации, содержащей не менее чем 4 предмета, то оно общезначимо.

Бонусы за решение задачи:

  • первый сдавший: +3 балла
  • второй и третий сдавшие: +2 балла

(7) Фундированность троек чисел

Доказать фундированность троек неотрицательных целых чисел относительно лексикографического порядка (лемма в блоке 20, обоснование которой помечено словами "Попробуйте сами").

Бонус за решение задачи: +2 балла первым двум предоставившим решение задачи

(8) Про эрбрановские интерпретации

Останется ли справедливой теорема об эрбрановских интерпретациях, если вместо "Система дизъюнктов" в её формулировке написать "Формула логики предикатов"? Ответ обосновать.

Бонус за решение задачи:

  • первый сдавший: +3 балла
  • второй сдавший: +2 балла

(9) Полная стратегия построения успешного резолютивного вывода

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

(Как это делалось, например, в доказательстве теоремы о полноте табличного вывода.)

Бонусы за решение задачи:

  • первый сдавший: +3 балла
  • второй и третий сдавшие: +2 балла

(10) Вычислительные возможности метода резолюций

Ответить (с обоснованием и для достаточно широкого семейства резолютивных выводов) на вопрос, поставленный в конце "заключительного примера для метода резолюций" блока 25.

Бонусы за решение задачи:

  • первый сдавший: +3 балла
  • второй и третий сдавшие: +2 балла

(11) Исчисление семантических таблиц

Определить (с пояснениями) аксиомы и правила вывода логического исчисления со следующими свойствами:

  • формулы исчисления - семантические таблицы логики предикатов;
  • таблица доказуема в исчислении тогда и только тогда, когда для неё существует успешный табличный вывод;
  • из доказательства для таблицы T в исчислении можно получить успешный табличный вывод для T, расположив таблицы в вершинах дерева согласно применению правил исчисления.

Бонус за решение задачи: +2 балла первым двум предоставившим решение задачи

(12) Корректность натурального исчисления предикатов

Выбрать одно из четырёх правил вывода НИП для кванторов (введение/удаление существования/всеобщности) и обосновать корректность этого правила согласно разобранному в доказательстве теоремы о корректности НИВ.

Для каждого из правил принимается только одно решение, и от одного студента принимается решение только для одного правила. Бонус за решение: +1 балл

(13) Теорема Гёделя о полноте

Доказать теорему Гёделя о полноте, сформулированную в блоке 31, для исчисления, изложенного в этом же блоке.

Бонусы за решение задачи:

  • первый сдавший: +10 баллов
  • второй и третий сдавшие: +7 баллов

(14) Непротиворечивая конечная полная теория

Привести пример (с обоснованием) непротиворечивой конечной полной аксиоматической теории первого порядка.

Бонус за решение задачи:

  • первый сдавший: +2 балла
  • второй сдавший: +1 балл

(15) О подстановке определения

Оформить пропущенные части доказательства теоремы о подстановке определения: доказательство для функции кси и часть доказательства, скрытая в отсылке к теореме о равносильной замене.

Бонус за решение задачи:

  • первый сдавший: +3 балла
  • второй сдавший: +2 балла

(16) Теорема Гёделя о неполноте

Доказать теорему Гёделя о неполноте в формулировке, представленной в блоке 40: либо адаптировать представленный там эскиз доказательства к общему случаю и доказать леммы об арифметизации и о диагонали, либо предоставить независимое доказательство.

Бонусы за решение задачи:

  • первый предоставивший решение: +14 баллов
  • второй предоставивший решение: +11 баллов
  • третий предоставивший решение: +8 баллов

(17) Арифметика Пресбургера

Доказать полноту системы аксиом арифметики Пресбургера, представленной на последнем слайде блока 41.

Бонусы за решение задачи:

  • первый предоставивший решение: +4 балла
  • второй предоставивший решение: +3 балла
  • третий предоставивший решение: +2 балл

(18) Определение экспоненты

Предложить (с обоснованием) определение одноместной функции 2^x (два в степени икс) в арифметической интерпретации на целых неотрицательных числах с сигнатурой <{0}, {+, x, s}, {=}> (семинар 5, задача 1, пункт 21).

Если в обосновании будут содержаться китайская теорема об остатках, малая теорема Ферма или что-либо другое нетривиальное, то обоснование этого - часть решения

Бонусы за решение задачи:

  • первый предоставивший решение: +4 баллов
  • второй предоставивший решение: +3 балла
  • третий предоставивший решение: +2 балла

(19) Свойства шкал Крипке

Доказать утверждения о рефлексивности, транзитивности и симметричности шкал Крипке, сформулированные в блоке 43.

Бонус за решение задачи:

  • первый сдавший: +3 балла
  • второй и третий сдавшие: +2 балла

(20) Задача о трёх мудрецах

Записать и пояснить ход рассуждений мудрецов в задаче о трёх мудрецах, представленной в конце блока 43, в терминах эпистемической логики.

Бонус за решение задачи: +2 балла первым трём предоставившим решение.

(21) Корректность логики Хоара

Доказать корректность одного из правил логики Хоара (блок 46, лемма о корректности правил), кроме правил для пустой команды и для присваивания.

Для каждого из правил принимается только одно решение, и от одного студента принимается решение только для одного правила. Бонус за решение: +2 балла

(22) Слабейшие предусловия

Доказать теорему о слабейшем предусловии (лекция 15).

Бонусы за решение задачи:

  • первый сдавший: +3 балла
  • второй и третий сдавшие: +2 балла

(23) Упрощение ctl-формул

Доказать один из зелёных пунктов утверждения об упрощении ctl-формул в блоке 47.

Для каждого пункта принимается только одно решение, и от одного студента принимается решение только для одного пункта. Бонус за решение: +1 балл

(24) Алгоритм проверки выполнимости ctl-формулы на системе переходов

Ответить (с обоснованием) на вопрос в самом конце блока 47 о корректности и сложности алгоритма проверки выполнимости ctl-формулы на системе переходов.

Бонусы за решение задачи:

  • первый предоставивший решение: +4 баллов
  • второй предоставивший решение: +3 балла
  • третий предоставивший решение: +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 с.