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

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
 
(не показаны 33 промежуточных версий 1 участника)
Строка 5: Строка 5:
 
''В этом разделе будут выкладываться объявления о текущих изменениях в курсе и на странице курса''
 
''В этом разделе будут выкладываться объявления о текущих изменениях в курсе и на странице курса''
  
* 2020.04.14 12:50 Обновлена информация о принятых решениях бонусных задач
+
* 2020.07.03 01:00 Обновлена информация о принятых решениях бонусных задач
* 2020.04.14 12:50 Удалена бонусная задача 6 (материал, необходимый для её понимания, исключён из лекций)
+
* 2020.05.24 19:09 Появилась последняя бонусная задача (14)
* 2020.04.11 18:38 Появились бонусные задача 4, 5
+
* 2020.05.24 19:04 Выложены слайды последней лекции (17)
* 2020.04.11 18:12 Выложены слайды лекции 10
+
* 2020.05.08 11:46 Обновлены правила проведения экзамена и зачёта
 +
* 2020.05.03 22:05 Обновлены материалы семинара 5
 +
* 2020.04.17 15:50 Статистика предоставленных решений бонусных задач переехала из подразделов 6.1, 6.2, ... в единую таблицу в разделе 6
 
* 2020.02.10 13:05 Страница подготовлена к началу весеннего семестра 2019/2020 учебного года
 
* 2020.02.10 13:05 Страница подготовлена к началу весеннего семестра 2019/2020 учебного года
  
Строка 33: Строка 35:
 
'''[[Media: Mathlog_318_lecture_10.pdf|Лекция 10.]]''' Полнота резолютивного вывода. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.
 
'''[[Media: Mathlog_318_lecture_10.pdf|Лекция 10.]]''' Полнота резолютивного вывода. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.
  
== Временный архив слайдов: 2018-2019 учебный год ==
+
'''[[Media: Mathlog_318_lecture_11.pdf|Лекция 11.]]''' Машины Тьюринга. Теорема Чёрча. Как устроены математические доказательства. Логические исчисления.
  
'''[[Media: Mathlog_318_lecture_11.pdf|Лекция 11.]]''' Выразимость в теориях и интерпретациях. Арифметика Пресбургера (определение, разрешимость, полнота, выразительные возможности).
+
'''[[Media: Mathlog_318_lecture_12_13.pdf|Лекция 12-13.]]''' Натуральное исчисление высказываний. Натуральное исчисление предикатов. Исчисление предикатов гильбертовского типа.
 
+
'''[[Media: Mathlog_318_lecture_12.pdf|Лекция 12.]]''' Логические исчисления. Исчисление высказываний гильбертовского типа. Корректность и полнота исчисления высказываний.
+
 
+
'''[[Media: Mathlog_318_lecture_13.pdf|Лекция 13.]]''' Исчисление предикатов гильбертовского типа. Теорема Гёделя о полноте (формулировка). Натуральное исчисление высказываний, его корректность и полнота. Натуральное исчисление предикатов, его корректность и полнота. Натуральный вывод формул.
+
  
 
'''[[Media: Mathlog_318_lecture_14.pdf|Лекция 14.]]''' Модальные логики. Эпистемические логики. Темпоральные логики.
 
'''[[Media: Mathlog_318_lecture_14.pdf|Лекция 14.]]''' Модальные логики. Эпистемические логики. Темпоральные логики.
Строка 48: Строка 46:
  
 
'''[[Media: Mathlog_318_lecture_17.pdf|Лекция 17.]]''' Табличный алгоритм верификации для LTL. Замыкание Фишера-Ладнера. Системы Хинтикки.
 
'''[[Media: Mathlog_318_lecture_17.pdf|Лекция 17.]]''' Табличный алгоритм верификации для LTL. Замыкание Фишера-Ладнера. Системы Хинтикки.
 +
 +
== Временный архив слайдов: 2018-2019 учебный год ==
 +
 +
'''[[Media: Mathlog_318_lecture_12.pdf|Лекция 12.]]''' Логические исчисления. Исчисление высказываний гильбертовского типа. Корректность и полнота исчисления высказываний.
 +
 +
'''[[Media: Mathlog_318_lecture_13.pdf|Лекция 13.]]''' Исчисление предикатов гильбертовского типа. Теорема Гёделя о полноте (формулировка). Натуральное исчисление высказываний, его корректность и полнота. Натуральное исчисление предикатов, его корректность и полнота. Натуральный вывод формул.
  
 
== Временный архив слайдов: 2017-2018 учебный год ==
 
== Временный архив слайдов: 2017-2018 учебный год ==
Строка 67: Строка 71:
 
Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]]
 
Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]]
  
[[Media:Mllp_318_seminar_definability.pdf| Материалы семинара 5 (выразимость).]]
+
[[Media:Mathlog_318_seminar_natural_inference.pdf| Материалы семинара 5 (натуральное исчисление).]]
 
+
[[Media:Mathlog_318_seminar_natural_inference.pdf| Материалы семинара 6 (натуральное исчисление).]]
+
  
 
= Контрольная работа =
 
= Контрольная работа =
 
''Прошлогодняя информация, в скором времени обновится.''
 
  
 
Формат проведения и длительность контрольной работы: письменно, 95 минут.
 
Формат проведения и длительность контрольной работы: письменно, 95 минут.
Строка 81: Строка 81:
 
* '''три задачи''':
 
* '''три задачи''':
 
** построить формулу логики предикатов, адекватно описывающую высказывание, записанное на естественном языке;
 
** построить формулу логики предикатов, адекватно описывающую высказывание, записанное на естественном языке;
** проверить общезначимость формулы логики предикатов, используя метод семантических таблиц
+
** доказать общезначимость формулы логики предикатов, используя метод семантических таблиц
 
*** (правила табличного вывода будут выданы вместе с заданием контрольной);
 
*** (правила табличного вывода будут выданы вместе с заданием контрольной);
** проверить общезначимость формулы логики предикатов, используя метод резолюций;
+
** доказать общезначимость формулы логики предикатов, используя метод резолюций;
* '''девять теоретических вопросов''', проверяющих знание материала, изложенного в лекциях 2-9.
+
* '''девять теоретических вопросов''', проверяющих знание материала, изложенного в лекциях вплоть до конца обсуждения метода резолюций.
  
 
Контрольная работа оценивается по шкале '''от 0 до 15 баллов'''.
 
Контрольная работа оценивается по шкале '''от 0 до 15 баллов'''.
Строка 98: Строка 98:
 
Обоснование того, почему выбраны или не выбраны те или иные ответы, '''не требуется'''.
 
Обоснование того, почему выбраны или не выбраны те или иные ответы, '''не требуется'''.
  
'''Группа 241:''' баллы, набранные за контрольную работу, суммируются с другими баллами, требуемыми для получения зачёта.
+
'''Группы 241, 242:''' баллы, набранные за контрольную работу, суммируются с другими баллами, требуемыми для получения зачёта.
  
 
'''Группа 318:''' по результатам контрольной работы определяется <span style="background:#DDFFDD">бонус</span> или <span style="background:#FFDDDD">штраф</span>, суммирующийся с баллами за экзаменационную работу:
 
'''Группа 318:''' по результатам контрольной работы определяется <span style="background:#DDFFDD">бонус</span> или <span style="background:#FFDDDD">штраф</span>, суммирующийся с баллами за экзаменационную работу:
Строка 112: Строка 112:
  
 
= Экзамен =
 
= Экзамен =
 
''Прошлогодняя информация, в скором времени обновится.''
 
  
 
Формат проведения и длительность экзамена: письменно, 120 минут.
 
Формат проведения и длительность экзамена: письменно, 120 минут.
  
Экзаменационная работа оценивается по шкале '''от 0 до 30 баллов''' (''промежуточные баллы'').
+
Экзаменационная работа оценивается по шкале '''от 0 до 27 баллов''' (''промежуточные баллы'').
 
Итоговые баллы за экзаменационную работу - это сумма промежуточных баллов, бонусов и штрафов по итогам контрольной работы, а также других бонусов, если удалось их получить.
 
Итоговые баллы за экзаменационную работу - это сумма промежуточных баллов, бонусов и штрафов по итогам контрольной работы, а также других бонусов, если удалось их получить.
 
В зависимости от полученных итоговых баллов за экзаменационную работу выставляется оценка за экзамен:
 
В зависимости от полученных итоговых баллов за экзаменационную работу выставляется оценка за экзамен:
* набрано хотя бы 24 балла: '''отлично''';
+
* набрано хотя бы 22 балла: '''отлично''';
* набрано хотя бы 18, но менее 24 баллов: '''хорошо''';
+
* набрано хотя бы 16, но менее 22 баллов: '''хорошо''';
* набрано хотя бы 12, но менее 18 баллов: '''удовлетворительно''';
+
* набрано хотя бы 10, но менее 16 баллов: '''удовлетворительно''';
* набрано менее 12 баллов: '''неудовлетворительно'''.
+
* набрано менее 10 баллов: '''неудовлетворительно'''.
  
 
Промежуточные баллы складываются из баллов, полученных за решение каждой задачи в работе.
 
Промежуточные баллы складываются из баллов, полученных за решение каждой задачи в работе.
Строка 130: Строка 128:
 
* '''Задача 2 (3 балла)''': проверить общезначимость формулы логики предикатов методом семантических таблиц.
 
* '''Задача 2 (3 балла)''': проверить общезначимость формулы логики предикатов методом семантических таблиц.
 
* '''Задача 3 (3 балла)''': проверить общезначимость формулы логики предикатов методом резолюций.
 
* '''Задача 3 (3 балла)''': проверить общезначимость формулы логики предикатов методом резолюций.
* '''Задача 4 (3 балла)''': предложить аксиому, определяющую арифметическое понятие в заданной сигнатуре.
+
* '''Задача 4 (3 балла)''': предложить доказательство общезначимости формулы логики предикатов в натуральном исчислении.
* '''Задача 5 (3 балла)''': предложить доказательство формулы или соответствующей секвенции в натуральном исчислении предикатов.
+
* '''Задачи 5-7 (2 балла за каждую)''' состоят из двух частей: а) сформулировать теорему или определение, рассказанные в лекциях; б) ответить на вопрос, так или иначе связанный с первой частью, '''без пояснений''' (как правило - "да" или "нет", либо привести какой-либо пример).
* '''Задачи 6-8 (2 балла за каждую)''' состоят из двух частей: а) сформулировать теорему или определение, рассказанные в лекциях; б) ответить на вопрос, так или иначе связанный с первой частью, '''без пояснений''' (как правило - "да" или "нет", либо привести какой-либо пример).
+
* '''Задачи 8-10 (3 балла за каждую)''': из предложенных вариантов ответа на заданный вопрос выбрать правильные (один, несколько или ни одного), правильность каждого выбранного ответа обосновать ('''невыбранные ответы обосновывать не нужно''').
* '''Задачи 9-11 (3 балла за каждую)''': из предложенных вариантов ответа на заданный вопрос выбрать правильные (один, несколько или ни одного), правильность каждого выбранного ответа обосновать ('''невыбранные ответы обосновывать не нужно''').
+
  
 
= Зачёт =
 
= Зачёт =
 
''Прошлогодняя информация, в скором времени обновится.''
 
  
 
После завершения лекций будет проведена вторая контрольная работа. Эта работа будет содержать
 
После завершения лекций будет проведена вторая контрольная работа. Эта работа будет содержать
* Две задачи, идентичные задачам 4, 5 экзамена, каждая из которых оценивается в 2 балла.
+
* Одну задачу: предложить доказательство общезначимости формулы логики предикатов в натуральном исчислении. Задача оценивается в 2 балла.
* Пять теоретических вопросов по лекциям, проведённым после контрольной работы, аналогичные теоретическим вопросам первой контрольной работы. Каждый теоретический вопрос оценивается в 1 балл.
+
* Пять теоретических вопросов того же устройства, что и на первой контрольной работе, но по темам лекций, не вошедшим в первую контрольную. Каждый теоретический вопрос оценивается в 1 балл.
  
Для получения зачёта необходимо набрать не менее '''16 баллов''' по итогам двух контрольных работ и сдачи других заданий.
+
Для получения зачёта необходимо набрать не менее '''14 баллов''' по итогам двух контрольных работ и сдачи других  
  
Не получившим зачёт по результатам второй контрольной работы будут предоставлены дополнительные попытки получения зачёта. На этих попытках:
+
На каждой попытке зачёта имеется возможность повысить набранные баллы:
* Сохраняются баллы за каждую задачу, суммарный балл за теоретические вопросы первой контрольной работы, суммарный балл за теоретические вопросы второй контрольной работы.
+
* Повторно решить любую задачу. Если удалось улучшить оценку задачи, то старая (низкая) оценка заменяется на новую (высокую).
* Предоставляется возможность поднять каждый из этих баллов, решив соответствующие части новых вариантов контрольных работ.
+
* Повторно ответить на теоретические вопросы по темам первой контрольной. Если суммарно за все ответы набрано больше баллов, чем было до этого, то старая (низкая) суммарная оценка заменяется на новую (высокую).
 +
* Повторно ответить на теоретические вопросы по темам второй контрольной. Если суммарно за все ответы набрано больше баллов, чем было до этого, то старая (низкая) суммарная оценка заменяется на новую (высокую).
  
 
= Дополнительные бонусы к экзамену и зачёту =
 
= Дополнительные бонусы к экзамену и зачёту =
Строка 157: Строка 153:
 
* Задача считается решённой, если не осталось неотвеченных вопросов по обоснованию всех шагов решения.
 
* Задача считается решённой, если не осталось неотвеченных вопросов по обоснованию всех шагов решения.
  
'''Бонусы за решение задач сформулированы для одной учебной группы''' и получаются внутри одной группы независимо от другой (например, "''первый''" трактуется как "''первый из группы 318, а также первый из группы 241, а также первый из группы 242''".
+
'''Бонусы за решение задач сформулированы для одной учебной группы''' и получаются внутри одной группы независимо от другой (например, "''первый''" трактуется как "''первый из группы 318, а также первый из группы 241, а также первый из группы 242''").
  
''Задачи будут появляться по мере проведения занятий''
+
{| class="wikitable"
 +
|colspan=2|Номер задачи
 +
|1
 +
|2
 +
|3
 +
|4
 +
|5
 +
|6
 +
|7
 +
|8
 +
|9
 +
|10
 +
|11
 +
|12
 +
|13
 +
|14
 +
|-
 +
|colspan=2|Сколько решений оценивается
 +
|3
 +
|2
 +
|2
 +
|3
 +
|3
 +
|2
 +
|4
 +
|3
 +
|3
 +
|3
 +
|4
 +
|3
 +
|4
 +
|
 +
|-
 +
|rowspan="3"|Сколько решений сдано в группе
 +
<!--
 +
|241
 +
|0
 +
|2
 +
|1
 +
|0
 +
|1
 +
|0
 +
|0
 +
|1
 +
|0
 +
|0
 +
|0
 +
|0
 +
|0
 +
|0
 +
|-
 +
|242
 +
|0
 +
|0
 +
|0
 +
|0
 +
|0
 +
|0
 +
|0
 +
|1
 +
|0
 +
|0
 +
|0
 +
|0
 +
|0
 +
|0
 +
|-
 +
-->
 +
|318
 +
|0
 +
|2
 +
|2
 +
|0
 +
|0
 +
|1
 +
|1<sup>*</sup>
 +
|1
 +
|2
 +
|0
 +
|0
 +
|0
 +
|0
 +
|0
 +
|}
  
== Полнота табличного вывода в логике предикатов ==
+
<sup>*</sup> Правило удаления всеобщности
  
=== Описание задачи ===
+
''Задачи будут появляться по мере проведения занятий''
 +
 
 +
== (1) Полнота табличного вывода в логике предикатов ==
  
 
Адаптировать доказательство теоремы о полноте табличного вывода в логике предикатов к более общему случаю:
 
Адаптировать доказательство теоремы о полноте табличного вывода в логике предикатов к более общему случаю:
Строка 177: Строка 258:
 
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
 
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
  
=== Количество предоставленных решений ===
+
== (2) Утверждения об отношении равносильности ==
  
'''Группа 241:''' 0
+
Обосновать три утверждения об отношении равносильности в лекции 6, помеченные словом "Самостоятельно" рядом со словом "Доказательство".
  
'''Группа 242:''' 0
+
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение задачи
  
'''Группа 318:''' 0
+
== (3) Фундированность троек чисел ==
  
== Утверждения об отношении равносильности ==
+
Доказать фундированность троек неотрицательных целых чисел относительно лексикографического порядка (лемма в лекции 8, сформулированная в рамках доказательства завершаемости алгоритма унификации, обоснование которой помечено словами "Попробуйте сами").
  
=== Описание задачи ===
+
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение задачи
  
Обосновать три утверждения об отношении равносильности в лекции 6, помеченные словом "Самостоятельно" рядом со словом "Доказательство".
+
== (4) Стратегия построения резолютивного вывода ==
  
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение задачи
+
Сформулировать (с обоснованием) список правил, которых достаточно придерживаться, чтобы в резолютивном выводе, строящемся произвольно в рамках этих правил для противоречивой системы дизъюнктов, рано или поздно появился пустой дизъюнкт.
  
=== Количество предоставленных решений ===
+
Бонусы за решение задачи:
 +
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
 +
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
  
'''Группа 241:''' 1
+
== (5) Вычислительные возможности метода резолюций ==
  
'''Группа 242:''' 0
+
Сформулировать и обосновать утверждение, дающее ответ на вопрос, поставленный в конце "заключительного примера для метода резолюций" лекции 10.
  
'''Группа 318:''' 1
+
Бонусы за решение задачи:
 +
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
 +
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
  
== Фундированность троек чисел ==
+
== (6) Исчисление семантических таблиц ==
  
=== Описание задачи ===
+
Определить аксиомы и правила вывода логического исчисления со следующими свойствами:
 
+
* формулы исчисления - семантические таблицы логики предикатов;
Доказать фундированность троек неотрицательных целых чисел относительно лексикографического порядка (лемма в лекции 8, сформулированная в рамках доказательства завершаемости алгоритма унификации, обоснование которой помечено словами "Попробуйте сами").
+
* таблица выводима в исчислении тогда и только тогда, когда для неё существует успешный табличный вывод,
 +
* из доказательства для таблицы T можно получить успешный табличный вывод для T, взяв некоторое неразмеченное дерево и доразметив вершины этого дерева таблицами из доказательства.
  
 
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение задачи
 
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение задачи
  
=== Количество предоставленных решений ===
+
== (7) Корректность натурального исчисления ==
  
'''Группа 241:''' 0
+
Выбрать одно из 4-х правил работы с кванторами в натуральном исчислении (введение/удаление существования/всеобщности) и обосновать корректность этого правила: если формулы над чертой общезначимы, то и формула под чертой общезначима (см. лекцию 12-13).
  
'''Группа 242:''' 0
+
Для каждого из правил принимается только одно решение, и от одного студента принимается решение только для одного правила.
 +
Бонус за решение: <span style="background:#DDFFDD">+1 балл</span>
  
'''Группа 318:''' 1
+
== (8) Теорема Гёделя о полноте ==
  
== Стратегия построения резолютивного вывода ==
+
Доказать теорему Гёделя о полноте (см. лекцию 12-13).
  
=== Описание задачи ===
+
Бонусы за решение задачи:
 +
* '''первый''' сдавший: <span style="background:#DDFFDD">+10 баллов</span>
 +
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+7 баллов</span>
  
Сформулировать (с обоснованием) список правил, которых достаточно придерживаться, чтобы в резолютивном выводе, строящемся произвольно в рамках этих правил для противоречивой системы дизъюнктов, рано или поздно появился пустой дизъюнкт.
+
== (9) Свойства шкал Крипке ==
 +
 
 +
Доказать утверждения о рефлексивности, транзитивности и симметричности шкал Крипке, сформулированные в разделе "Эпистемические логики" '''лекции 14'''
  
Бонусы за решение задачи:
+
Бонус за решение задачи:
 
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
 
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
 
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
 
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
  
=== Количество предоставленных решений ===
+
== (10) Задача о трёх мудрецах ==
  
'''Группа 241:''' 0
+
Записать и пояснить ход рассуждений мудрецов в ''задаче о трёх мудрецах'' ('''лекция 14''') в терминах эпистемической логики.
  
'''Группа 242:''' 0
+
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''трём''' предоставившим решение.
  
'''Группа 318:''' 0
+
== (11) Корректность логики Хоара ==
  
== Вычислительные возможности метода резолюций ==
+
Доказать корректность одного из правил логики Хоара ('''лекция 15, лемма о корректности правил'''), кроме правил для пустой команды и для присваивания.
  
=== Описание задачи ===
+
Для каждого из правил принимается только одно решение, и от одного студента принимается решение только для одного правила.
 +
Бонус за решение: <span style="background:#DDFFDD">+2 балла</span>
  
Сформулировать и обосновать утверждение, дающее ответ на вопрос, поставленный в конце "заключительного примера для метода резолюций" лекции 10.
+
== (12) Слабейшие предусловия ==
 +
 
 +
Доказать теорему о слабейшем предусловии ('''лекция 15''').
  
 
Бонусы за решение задачи:
 
Бонусы за решение задачи:
Строка 245: Строка 339:
 
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
 
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
  
=== Количество предоставленных решений ===
+
== (13) Законы темпоральных логик ==
  
'''Группа 241:''' 0
+
В '''лекции 16''' на слайде под заголовком "законы дистрибутивности" выбрать пару строк (1+2, 3+4, 5+6 или 7+8) и доказать либо опровергнуть равносильность в каждой из этих двух строк.
  
'''Группа 242:''' 0
+
Для каждой пары строк принимается только одно решение, и от одного студента принимается решение только для одной пары строк.
 +
Бонус за решение: <span style="background:#DDFFDD">+1 балл</span>
  
'''Группа 318:''' 0
+
== (14) Табличный алгоритм верификации для LTL ==
 +
 
 +
Ответить на существенную часть вопросов, сформулированных на последнем слайде последней лекции (17)
 +
 
 +
Бонус за решение задачи: '''обсуждается индивидуально'''.
  
 
<!--
 
<!--
Строка 315: Строка 414:
  
 
'''Группа 318:''' 3 (все баллы розданы)
 
'''Группа 318:''' 3 (все баллы розданы)
 
== Теорема Гёделя о полноте ==
 
 
=== Описание задачи ===
 
 
Доказать теорему Гёделя о полноте (см. '''лекцию 13''').
 
 
Бонусы за решение задачи:
 
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+9 баллов</span>
 
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+6 баллов</span>
 
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+6 баллов</span>
 
 
=== Количество предоставленных решений ===
 
 
'''Группа 318:''' 1
 
 
== Свойства шкал Крипке ==
 
 
=== Описание задачи ===
 
 
Доказать утверждения о рефлексивности, транзитивности и симметричности шкал Крипке, сформулированные в разделе "Эпистемические логики" '''лекции 14'''
 
 
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение.
 
 
=== Количество предоставленных решений ===
 
 
'''Группа 318:''' 1
 
 
== <s>Задача о трёх мудрецах</s> ==
 
 
=== Описание задачи ===
 
 
Записать и пояснить законы рассуждений и ход рассуждений мудрецов в ''задаче о трёх мудрецах'' ('''лекция 14''') в терминах эпистемической логики.
 
 
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение.
 
 
=== Количество предоставленных решений ===
 
 
'''Группа 318:''' 2 (все баллы розданы)
 
 
== Корректность правил логики Хоара ==
 
 
=== Описание задачи ===
 
 
Доказать корректность одного из правил логики Хоара ('''лекция 15, лемма о корректности правил'''), кроме правила R0 для пустой команды.
 
 
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> каждому решившему.
 
 
Ограничения на приём решений:
 
* От каждого принимается обоснование корректности не более чем одного правила.
 
* Обоснование корректности каждого правила принимается не более одного раза (в группе).
 
 
=== Принятые правила ===
 
 
'''Группа 318:''' -
 
 
== Слабейшие предусловия ==
 
 
Доказать теорему о слабейшем предусловии ('''лекция 15''').
 
 
Бонусы за решение задачи:
 
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+3 баллов</span>
 
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+2 балла</span>
 
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+1 балл</span>
 
 
=== Количество предоставленных решений ===
 
 
'''Группа 318:''' 0
 
 
== Законы темпоральных логик ==
 
 
=== Описание задачи ===
 
 
* Выбрать один темпоральный оператор логики линейного времени.
 
** Если выбран оператор U, то также выбрать ''право'' или ''лево''.
 
* Доказать или опровергнуть два закона дистрибутивности, сформулированные для выбранного оператора в '''лекции 16'''.
 
** Если выбран оператор U, то это два закона дистрибутивности для ''правого'' или ''левого'' аргумента, в зависимости от сделанного выбора.
 
 
Бонус за решение задачи: <span style="background:#DDFFDD">+1 балл</span> '''каждому''' предоставившему решение.
 
 
Ограничения на приём решений:
 
* От каждого принимается обоснование/опровержение не более чем одной пары законов.
 
* Обоснование/опровержение каждой пары законов принимается не более одного раза (в группе).
 
 
=== Операторы, для которых решения уже предоставлены ===
 
 
'''Группа 318:''' -
 
 
== Табличный алгоритм верификации для LTL ==
 
 
=== Описание задачи ===
 
 
Ответить на существенную часть вопросов, сформулированных на последнем слайде '''лекции 17''' 
 
 
Бонус за решение задачи: '''обсуждается индивидуально'''.
 
 
  
 
== Полнота семантической резолюции ==
 
== Полнота семантической резолюции ==
Строка 454: Строка 457:
  
 
= Программа курса =
 
= Программа курса =
 
''Программа будет уточняться по мере проведения занятий''
 
  
 
== Классические логики ==
 
== Классические логики ==
Строка 482: Строка 483:
 
</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>
 
 
-->
 
  
 
= Рекомендованная литература =
 
= Рекомендованная литература =

Текущая версия на 01:01, 3 июля 2020

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

Объявления

В этом разделе будут выкладываться объявления о текущих изменениях в курсе и на странице курса

  • 2020.07.03 01:00 Обновлена информация о принятых решениях бонусных задач
  • 2020.05.24 19:09 Появилась последняя бонусная задача (14)
  • 2020.05.24 19:04 Выложены слайды последней лекции (17)
  • 2020.05.08 11:46 Обновлены правила проведения экзамена и зачёта
  • 2020.05.03 22:05 Обновлены материалы семинара 5
  • 2020.04.17 15:50 Статистика предоставленных решений бонусных задач переехала из подразделов 6.1, 6.2, ... в единую таблицу в разделе 6
  • 2020.02.10 13:05 Страница подготовлена к началу весеннего семестра 2019/2020 учебного года

Содержание

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

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

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

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

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

Лекции 4 и 5 (рассказывал В. А. Захаров; желающие могут посмотреть то же самое другими словами от В. В. Подымова). Выполнимые и общезначимые формулы. Модели. Логическое следствие. Проблема общезначимости формул. Подстановки. Метод семантических таблиц в логике предикатов. Корректность табличного вывода.

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

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

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

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

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

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

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

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

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

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

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

Временный архив слайдов: 2018-2019 учебный год

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

Лекция 13. Исчисление предикатов гильбертовского типа. Теорема Гёделя о полноте (формулировка). Натуральное исчисление высказываний, его корректность и полнота. Натуральное исчисление предикатов, его корректность и полнота. Натуральный вывод формул.

Временный архив слайдов: 2017-2018 учебный год

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

Лекция 14-15. Модальные логики. Эпистемические логики. Темпоральные логики. Логика линейного времени (LTL). Логика деревьев вычислений (CTL). Верификация распределённых систем. Задача верификации для LTL. Табличный алгоритм верификации для LTL.

Временный архив слайдов: 2016-2017 учебный год

16-17.

Семинары

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

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

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

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

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

Формат проведения и длительность контрольной работы: письменно, 95 минут.

В рамках контрольной работы требуется решить

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

Контрольная работа оценивается по шкале от 0 до 15 баллов. Итоговые баллы за работу - это сумма баллов за задачи и теоретические вопросы.

Правильно решённая задача оценивается в 2 балла. Задача, решённая с ошибками, может быть оценена числом баллов от 0 до 2 в зависимости от качества и количества ошибок.

Правильно решённый теоретический вопрос оценивается в 1 балл. В каждом теоретическом вопросе предлагается несколько вариантов ответа. Среди этих ответов может быть один, ни одного или несколько правильных. Для правильного решения теоретического вопроса следует отметить все правильные ответы и только их. Обоснование того, почему выбраны или не выбраны те или иные ответы, не требуется.

Группы 241, 242: баллы, набранные за контрольную работу, суммируются с другими баллами, требуемыми для получения зачёта.

Группа 318: по результатам контрольной работы определяется бонус или штраф, суммирующийся с баллами за экзаменационную работу:

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

Экзамен

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

Экзаменационная работа оценивается по шкале от 0 до 27 баллов (промежуточные баллы). Итоговые баллы за экзаменационную работу - это сумма промежуточных баллов, бонусов и штрафов по итогам контрольной работы, а также других бонусов, если удалось их получить. В зависимости от полученных итоговых баллов за экзаменационную работу выставляется оценка за экзамен:

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

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

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

Зачёт

После завершения лекций будет проведена вторая контрольная работа. Эта работа будет содержать

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

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

На каждой попытке зачёта имеется возможность повысить набранные баллы:

  • Повторно решить любую задачу. Если удалось улучшить оценку задачи, то старая (низкая) оценка заменяется на новую (высокую).
  • Повторно ответить на теоретические вопросы по темам первой контрольной. Если суммарно за все ответы набрано больше баллов, чем было до этого, то старая (низкая) суммарная оценка заменяется на новую (высокую).
  • Повторно ответить на теоретические вопросы по темам второй контрольной. Если суммарно за все ответы набрано больше баллов, чем было до этого, то старая (низкая) суммарная оценка заменяется на новую (высокую).

Дополнительные бонусы к экзамену и зачёту

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

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

Бонусы за решение задач сформулированы для одной учебной группы и получаются внутри одной группы независимо от другой (например, "первый" трактуется как "первый из группы 318, а также первый из группы 241, а также первый из группы 242").

Номер задачи 1 2 3 4 5 6 7 8 9 10 11 12 13 14
Сколько решений оценивается 3 2 2 3 3 2 4 3 3 3 4 3 4
Сколько решений сдано в группе 318 0 2 2 0 0 1 1* 1 2 0 0 0 0 0

* Правило удаления всеобщности

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

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

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

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

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

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

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

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

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

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

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

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

(4) Стратегия построения резолютивного вывода

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

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

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

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

Сформулировать и обосновать утверждение, дающее ответ на вопрос, поставленный в конце "заключительного примера для метода резолюций" лекции 10.

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

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

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

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

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

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

(7) Корректность натурального исчисления

Выбрать одно из 4-х правил работы с кванторами в натуральном исчислении (введение/удаление существования/всеобщности) и обосновать корректность этого правила: если формулы над чертой общезначимы, то и формула под чертой общезначима (см. лекцию 12-13).

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

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

Доказать теорему Гёделя о полноте (см. лекцию 12-13).

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

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

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

Доказать утверждения о рефлексивности, транзитивности и симметричности шкал Крипке, сформулированные в разделе "Эпистемические логики" лекции 14

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

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

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

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

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

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

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

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

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

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

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

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

(13) Законы темпоральных логик

В лекции 16 на слайде под заголовком "законы дистрибутивности" выбрать пару строк (1+2, 3+4, 5+6 или 7+8) и доказать либо опровергнуть равносильность в каждой из этих двух строк.

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

(14) Табличный алгоритм верификации для LTL

Ответить на существенную часть вопросов, сформулированных на последнем слайде последней лекции (17)

Бонус за решение задачи: обсуждается индивидуально.


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

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

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