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

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
 
(не показаны 242 промежуточных версий 1 участника)
Строка 1: Строка 1:
Обязательный курс для студентов 318 группы 6 семестра обучения. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].
+
Обязательный курс для студентов групп 318 и 319/2, ''а также 241 и 242 (Математическая логика и теория алгоритмов)''. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].
  
== Контрольная работа ==
+
Актуальность информации: весенний семестр 2020/2021 учебного года.
  
Письменная контрольная работа состоится '''9 апреля на 4 паре (14:35-16:10) в аудитории 613'''.
+
<!--
 +
'''Объявления'''
  
На контрольной будет проверяться знание материалов, рассказанных в лекциях 1-10 и обсуждённых на семинарах.
+
''В этом разделе будут выкладываться объявления об изменениях на странице курса''
  
== Лекции по курсу математической логики и логического программирования ==
+
* 2021.02.04 16:00 Страница курса подготовлена к весеннему семестру 2020/2021 учебного года
 +
-->
  
'''[[Media:Mathlog_318_lecture_1.pdf|Лекция 1.]]''' '''Что изучает логика? Логика в информатике. Структура курса. Исторические сведения. Логические парадоксы.'''
+
= Слайды лекций =
  
'''[[Media:Mathlog_318_lecture_2.pdf|Лекция 2.]]''' '''Классическая логика предикатов первого порядка. Синтаксис: термы и формулы. Семантика: интерпретации, Выполнимость.'''
+
''Слайды будут выкладываться по мере проведения занятий''
  
'''[[Media: LectLog_3.pdf|Лекция 3.]]''' '''Выполнимые и общезначимые формулы. Модели. Логическое следование. Проблема общезначимости. Семантические таблицы.''' (читал [[Захаров Владимир Анатольевич|В. А. Захаров]])
+
'''[[Media: Mathlog_318_b1.pdf|Блок 1]]''' (вводный). Что такое логика. Содержание лекций. Несколько логических парадоксов.
  
'''[[Media:Mathlog_318_lecture_4.pdf|Лекция 4.]]''' '''Подстановки. Табличный вывод. Корректность табличного вывода.'''
+
'''[[Media: Mathlog_318_b2.pdf|Блок 2]]'''. Логика высказываний: синтаксис, семантика, выполнимость, общезначимость.
  
'''[[Media:Mathlog_318_lecture_5.pdf|Лекция 5.]]''' '''Полнота табличного вывода. Теорема Левенгейма-Сколема. Теорема компактности Мальцева. Автоматическое доказательство теорем.'''
+
'''[[Media: Mathlog_318_b3.pdf|Блок 3]]'''. Логика предикатов: синтаксис, семантика.
  
'''[[Media:Mathlog_318_lecture_6.pdf|Лекция 6.]]''' '''Общая схема метода резолюций. Равносильные формулы. Теорема о равносильной замене. Предваренная нормальная форма. Сколемовская стандартная форма. Системы дизъюнктов.'''
+
'''[[Media: Mathlog_318_b4.pdf|Блок 4]]'''. Как формализовать предложение на языке логики предикатов (пример).
  
'''[[Media:Mathlog_318_lecture_7.pdf|Лекция 7.]]''' '''Эрбрановские интерпретации. Теорема Эрбрана. Задача унификации.'''
+
'''[[Media: Mathlog_318_b5.pdf|Блок 5]]'''. Логика предикатов: выполнимые и общезначимые формулы; модели формул; логическое следствие; проблема общезначимости формул (постановка).
  
'''[[Media:Mathlog_318_lecture_8.pdf|Лекция 8.]]''' '''Алгоритм унификации.'''
+
'''[[Media: Mathlog_318_b6.pdf|Блок 6]]'''. Логика предикатов: почему бы не проверять общезначимость формул "в лоб"?
  
'''[[Media:Mathlog_318_lecture_9.pdf|Лекция 9.]]''' '''Резолютивный вывод. Корректность резолютивного вывода. Применение метода резолюций.'''
+
'''[[Media: Mathlog_318_b7.pdf|Блок 7]]'''. Метод семантических таблиц в логике высказываний.
  
'''[[Media:Mathlog_318_lecture_10.pdf|Лекция 10.]]''' '''Полнота резолютивного вывода.'''
+
'''[[Media: Mathlog_318_b8.pdf|Блок 8]]'''. Метод семантических таблиц в логике предикатов: семантические таблицы.
  
Лекция 11. '''Стратегии резолютивного вывода. Вычислительные возможности метода резолюций.'''
+
'''[[Media: Mathlog_318_b9.pdf|Блок 9]]'''. Подстановки (основные определения).
  
Лекция 12. '''Хорновские логические программы: синтаксис. Декларативная семантика логических программ. Операционная семантика логических программ. SLD-резолютивные вычисления.'''
+
'''[[Media: Mathlog_318_b10.pdf|Блок 10]]'''. Метод семантических таблиц в логике предикатов: табличный вывод.
  
Лекция 13. '''Корректность операционной семантики. Полнота операционной семантики.'''
+
'''[[Media: Mathlog_318_b11.pdf|Блок 11]]'''. Метод семантических таблиц в логике предикатов: корректность табличного вывода.
  
Лекция 14. '''Правила выбора подцелей. Деревья вычислений логических программ. Стратегии вычисления логических программ.'''
+
'''[[Media: Mathlog_318_b12.pdf|Блок 12]]'''. Метод семантических таблиц в логике предикатов: полнота табличного вывода.
+
Лекция 15. '''Алгоритмическая полнота логических программ. Моделирование машин Тьюринга логическим программами. Теорема Черча.'''
+
  
Лекция 16. '''Управление вычислениями логических программ. Оператор отсечения.'''
+
'''[[Media: Mathlog_318_b13.pdf|Блок 13]]'''. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Автоматизация доказательства теорем.
  
Лекция 17. '''Отрицание в логическом программировании. Оператор not. Встроенные предикаты и функции. Оператор вычисления значений. Модификация баз данных.'''
+
== Слайды прошлых лет ==
  
Лекция 18. '''Интуиционистская логика.'''
+
'''[[Media: Mathlog_318_lecture_1.pdf|Лекция]]''' (вводная). Что такое логика? Содержание лекций. История логики. Логические парадоксы.
  
Лекция 19. '''Модальные логики.'''
+
'''[[Media: Mathlog_318_lecture_2.pdf|Лекция.]]''' Логика высказываний: синтаксис, семантика, выполнимость, общезначимость. Метод семантических таблиц в логике высказываний.
  
'''Лекция 20.''' Правильные программы. Императивные программы. Задача верификации программ. Логика Хоара.                          Автоматическая проверка правильности программ.
+
'''[[Media: Mathlog_318_lecture_3.pdf|Лекция.]]''' Логика предикатов: синтаксис (термы, формулы), семантика (интерпретации, отношение выполнимости).
  
'''Лекция 21.''' Верификация распределенных программ. Логика линейного времени PLTL.                                       Размеченные системы переходов. Задача верификации моделей программ.  
+
'''[[Media: Mathlog_318_lecture_4_5.pdf|Лекция.]]''' Выполнимые и общезначимые формулы. Модели. Логическое следствие. Проблема общезначимости формул. Подстановки. Метод семантических таблиц в логике предикатов. Корректность табличного вывода.
  
'''Лекция 22.''' Задача верификации моделей программ. Подформулы Фишера-Ладнера. Табличный метод верификации моделей программ. Системы Хинтикки. Алгоритм верификации моделей программ.
+
'''[[Media: Mathlog_318_lecture_6.pdf|Лекция.]]''' Полнота табличного вывода в логике предикатов. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Равносильные формулы. Теорема о равносильной замене.
  
== Программа курса == 
+
'''[[Media: Mathlog_318_lecture_7.pdf|Лекция.]]''' Общая схема метода резолюций. Предварённая нормальная форма. Сколемовская стандартная форма. Системы дизъюнктов. Задача унификации.
  
=== Логика предикатов первого порядка ===
+
'''[[Media: Mathlog_318_lecture_8.pdf|Лекция.]]''' Алгоритм унификации атомарных формул. Теорема об унификации.
 +
 
 +
'''[[Media: Mathlog_318_lecture_9.pdf|Лекция.]]''' Резолютивный вывод. Корректность резолютивного вывода. Применение метода резолюций. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях. Теорема Эрбрана.
 +
 
 +
'''[[Media: Mathlog_318_lecture_10.pdf|Лекция.]]''' Полнота резолютивного вывода. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.
 +
 
 +
'''[[Media: Mathlog_318_lecture_11.pdf|Лекция.]]''' Машины Тьюринга. Теорема Чёрча. Как устроены математические доказательства. Логические исчисления.
 +
 
 +
'''[[Media: Mathlog_318_lecture_12_13.pdf|Лекция.]]''' Натуральное исчисление высказываний. Натуральное исчисление предикатов. Исчисление предикатов гильбертовского типа.
 +
 
 +
'''[[Media: Mathlog_318_lecture_14.pdf|Лекция.]]''' Модальные логики. Эпистемические логики. Темпоральные логики.
 +
 
 +
'''[[Media: Mathlog_318_lecture_15.pdf|Лекция.]]''' Формальная верификация программ. Императивные программы. Корректность императивных программ. Логика Хоара. Автоматизация проверки правильности программ.
 +
 
 +
'''[[Media: Mathlog_318_lecture_16.pdf|Лекция.]]''' Верификация распределённых систем. Логика линейного времени (LTL). Размеченные системы переходов. Задача верификации (model checking) для LTL.
 +
 
 +
'''[[Media: Mathlog_318_lecture_17.pdf|Лекция.]]''' Табличный алгоритм верификации для LTL. Замыкание Фишера-Ладнера. Системы Хинтикки.
 +
 
 +
'''[[Media: Mathlog_318_lecture_11_12.pdf|Лекция.]]''' Аксиоматические теории. Основные свойства теорий. Формальная арифметика. Арифметика Пеано. Теорема Гёделя о неполноте. Определимость. Арифметика Пресбургера.
 +
 
 +
'''[[Media: Mathlog_318_lecture_16_17.pdf|Лекция.]]'''.
 +
 
 +
= Семинары =
 +
 
 +
''Материалы семинаров будут обновляться по мере проведения занятий''
 +
 
 +
Семинары 1-4 проводятся по [[Media:MatLog_tasks.pdf| этому сборнику задач.]]
 +
 
 +
Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]]
 +
 
 +
[[Media:Mathlog_318_seminar_natural_inference.pdf| Материалы семинара 5 (натуральное исчисление).]]
 +
 
 +
= Экзамен =
 +
 
 +
Формат проведения и длительность экзамена: письменно, 120 минут.
 +
 
 +
Экзаменационная работа оценивается по шкале от 0 до 33 технических баллов.
 +
К оценке за эту работу прибавляются технические баллы, полученные за работу в семестре (выполнение премиальных задач).
 +
Согласно набранной сумме технических баллов выставляется оценка:
 +
* хотя бы 27: '''отлично''';
 +
* хотя бы 21, но менее 27: '''хорошо''';
 +
* хотя бы 15, но менее 21: '''удовлетворительно''';
 +
* менее 15: '''неудовлетворительно'''.
 +
 
 +
Баллы за экзаменационную работу складываются из баллов за каждую задачу, предложенную в работе:
 +
* Каждая из задач 1-5 оценивается в 3 балла. Темы задач:
 +
*# Формализовать в логике предикатов предложение, записанное на естественном языке.
 +
*# Проверить общезначимость формулы логики предикатов методом семантических таблиц.
 +
*# Проверить общезначимость формулы логики предикатов методом резолюций.
 +
*# ''По теме логических исчислений, точная формулировка определится позже''.
 +
*# ''По теме аксиоматических теорий, точная формулировка определится позже''.
 +
* Каждая из задач 6-8 оценивается в 2 балла и состоит из двух частей:
 +
*# Сформулировать утверждение, определение и т.п.
 +
*# Ответить на вопрос "на понимание", так или иначе связанный с формулировкой.
 +
* Каждая из задач 9-12 оценивается в 3 балла и устроена так:
 +
** Из нескольких предложенных вариантов ответа выбрать правильные (один, несколько или ни одного) и '''обосновать''' выбранные ответы.
 +
** Невыбранные ответы обосновывать не нужно.
 +
 
 +
= Зачёт =
 +
 
 +
На зачёте оцениваются результаты, относящиеся к решению типовых задач, знанию теории и работе в семестре.
 +
 
 +
В курсе встретится 5 типовых задач:
 +
# Формализовать в логике предикатов предложение, записанное на естественном языке.
 +
# Проверить общезначимость формулы логики предикатов методом семантических таблиц.
 +
# Проверить общезначимость формулы логики предикатов методом резолюций.
 +
# ''По теме логических исчислений, точная формулировка определится позже''.
 +
# ''По теме аксиоматических теорий, точная формулировка определится позже''.
 +
 
 +
При проставлении зачёта учитывается 7 технических оценок:
 +
* Пять оценок за типовые задачи, по одной за каждую задачу. Максимальная оценка за каждую задачу - 3 балла.
 +
* Оценка за знание теории. Максимум - 15 баллов.
 +
* Оценка за решение премиальных задач.
 +
 
 +
Для получения зачёта требуется достичь следующих результатов:
 +
# '''Решить хотя бы 4 типовые задачи на 2 балла''' (т.е. правильно или с незначительными недочётами).
 +
# '''Набрать хотя бы 20 баллов''' суммарно за всё (типовые задачи, теория, премиальные задачи).
 +
 
 +
В курсе планируются две контрольные работы: первая - в середине семестра, вторая - после завершения лекций.
 +
Контрольные работы и попытки зачёта проводятся письменно, длительность каждого мероприятия - 90 минут (одна пара).
 +
 
 +
== Сдача типовых задач ==
 +
 
 +
Для решения каждой типовой задачи будет предложено несколько попыток.
 +
При проставлении зачёта учитывается '''максимальная''' оценка за задачу среди всех попыток её решить.
 +
 
 +
На первой контрольной работе будут предложены типовые задачи 1-3.
 +
На второй контрольной работе и на каждой попытке зачёта будут предложены все типовые задачи.
 +
 
 +
== Сдача теории ==
 +
 
 +
Теоретические вопросы даются в форме теста с множественным выбором: из предложенных вариантов ответа требуется выбрать правильные (один, несколько или ни одного), обоснование не требуется.
 +
Правильно решённый теоретический вопрос оценивается в 1 балл.
 +
 
 +
На первой контрольной работе будет предложено 9 теоретических вопросов.
 +
На второй контрольной работе будет предложено 6 теоретических вопросов.
 +
Оценка за знание теории складывается из оценок за эти 15 теоретических вопросов.
 +
 
 +
На каждой попытке зачёта также будет предложено 15 теоретических вопросов.
 +
При проставлении зачёта учитывается '''максимальная''' оценка среди полученных за контрольные работы и за каждую из попыток зачёта.
 +
 
 +
= Премиальные задачи =
 +
 
 +
''По ходу проведения курса в подразделах этого раздела будут появляться премиальные задачи''
 +
 
 +
Общие условия сдачи решений премиальных задач:
 +
* Можно как прислать письменное решение, так и обсудить решение устно. Если прислано письменное решение и к нему есть вопросы, то для их решения может потребоваться дополнительное устное обсуждение.
 +
* При подготовке решения и во время его сдачи можно пользоваться любыми материалами.
 +
* При сдаче может быть проверено понимание '''каждой''' детали предложенного решения - следует быть к этому готовым.
 +
* Решение принимается, когда по нему не остаётся неотвеченных вопросов.
 +
 
 +
'''Бонусы за решение задач сформулированы для одной учебной группы''' и получаются внутри одной группы независимо от другой.
 +
Например, "''первый''" трактуется как "''первый из группы 318, а также первый из группы 319/2, а также ...''".
 +
 
 +
== (1) Свойства семантических таблиц в логике высказываний ==
 +
 
 +
Доказать три утверждения в блоке 7, доказательство которых помечено словами "А попробуйте сами", '''или''' два утверждения в блоке 8, помеченные теми же словами.
 +
 
 +
Бонус за решение задачи: <span style="background:#DDFFDD">+1 балл</span> первым '''двум''' предоставившим решение задачи
 +
 
 +
== (2) Полнота табличного вывода в логике предикатов ==
 +
 
 +
Адаптировать доказательство теоремы о полноте табличного вывода в логике предикатов к более общему случаю:
 +
* сигнатура алфавита состоит из
 +
** не более чем счётного числа констант,
 +
** не более чем счётного числа функциональных символов произвольных местностей,
 +
** не более чем счётного числа предикатных символов произвольных местностей;
 +
* формулы исходной таблицы могут содержать свободные переменные;
 +
* исходная таблица содержит не более чем счётное число формул.
 +
 
 +
Бонусы за решение задачи:
 +
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
 +
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
 +
 
 +
<!--
 +
 
 +
== (2) Утверждения об отношении равносильности ==
 +
 
 +
Обосновать три утверждения об отношении равносильности в лекции 6, помеченные словом "Самостоятельно" рядом со словом "Доказательство".
 +
 
 +
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение задачи
 +
 
 +
== (3) Фундированность троек чисел ==
 +
 
 +
Доказать фундированность троек неотрицательных целых чисел относительно лексикографического порядка (лемма в лекции 8, сформулированная в рамках доказательства завершаемости алгоритма унификации, обоснование которой помечено словами "Попробуйте сами").
 +
 
 +
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение задачи
 +
 
 +
== (4) Стратегия построения резолютивного вывода ==
 +
 
 +
Сформулировать (с обоснованием) список правил, которых достаточно придерживаться, чтобы в резолютивном выводе, строящемся произвольно в рамках этих правил для противоречивой системы дизъюнктов, рано или поздно появился пустой дизъюнкт.
 +
 
 +
Бонусы за решение задачи:
 +
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
 +
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
 +
 
 +
== (5) Вычислительные возможности метода резолюций ==
 +
 
 +
Сформулировать и обосновать утверждение, дающее ответ на вопрос, поставленный в конце "заключительного примера для метода резолюций" лекции 10.
 +
 
 +
Бонусы за решение задачи:
 +
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
 +
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
 +
 
 +
== (6) Исчисление семантических таблиц ==
 +
 
 +
Определить аксиомы и правила вывода логического исчисления со следующими свойствами:
 +
* формулы исчисления - семантические таблицы логики предикатов;
 +
* таблица выводима в исчислении тогда и только тогда, когда для неё существует успешный табличный вывод,
 +
* из доказательства для таблицы T можно получить успешный табличный вывод для T, взяв некоторое неразмеченное дерево и доразметив вершины этого дерева таблицами из доказательства.
 +
 
 +
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение задачи
 +
 
 +
== (7) Корректность натурального исчисления ==
 +
 
 +
Выбрать одно из 4-х правил работы с кванторами в натуральном исчислении (введение/удаление существования/всеобщности) и обосновать корректность этого правила: если формулы над чертой общезначимы, то и формула под чертой общезначима (см. лекцию 12-13).
 +
 
 +
Для каждого из правил принимается только одно решение, и от одного студента принимается решение только для одного правила.
 +
Бонус за решение: <span style="background:#DDFFDD">+1 балл</span>
 +
 
 +
== (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">+2 балла</span>
 +
 
 +
== (10) Задача о трёх мудрецах ==
 +
 
 +
Записать и пояснить ход рассуждений мудрецов в ''задаче о трёх мудрецах'' ('''лекция 14''') в терминах эпистемической логики.
 +
 
 +
Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''трём''' предоставившим решение.
 +
 
 +
== (11) Корректность логики Хоара ==
 +
 
 +
Доказать корректность одного из правил логики Хоара ('''лекция 15, лемма о корректности правил'''), кроме правил для пустой команды и для присваивания.
 +
 
 +
Для каждого из правил принимается только одно решение, и от одного студента принимается решение только для одного правила.
 +
Бонус за решение: <span style="background:#DDFFDD">+2 балла</span>
 +
 
 +
== (12) Слабейшие предусловия ==
 +
 
 +
Доказать теорему о слабейшем предусловии ('''лекция 15''').
 +
 
 +
Бонусы за решение задачи:
 +
* '''первый''' сдавший: <span style="background:#DDFFDD">+3 балла</span>
 +
* '''второй''' и '''третий''' сдавшие: <span style="background:#DDFFDD">+2 балла</span>
 +
 
 +
== (13) Законы темпоральных логик ==
 +
 
 +
В '''лекции 16''' на слайде под заголовком "законы дистрибутивности" выбрать пару строк (1+2, 3+4, 5+6 или 7+8) и доказать либо опровергнуть равносильность в каждой из этих двух строк.
 +
 
 +
Для каждой пары строк принимается только одно решение, и от одного студента принимается решение только для одной пары строк.
 +
Бонус за решение: <span style="background:#DDFFDD">+1 балл</span>
 +
 
 +
== (14) Табличный алгоритм верификации для LTL ==
 +
 
 +
Ответить на существенную часть вопросов, сформулированных на последнем слайде последней лекции (17)
 +
 
 +
Бонус за решение задачи: '''обсуждается индивидуально'''.
 +
-->
 +
 
 +
<!--
 +
 
 +
== Изоморфизм и элементарная эквивалентность интерпретаций ==
 +
 
 +
=== Описание задачи ===
 +
 
 +
Доказать утверждение на слайде 24 лекции 10 о соотношении понятий изоморфизма и элементарной эквивалентности интерпретаций.
 +
 
 +
Бонусы за решение задачи:
 +
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+2 балла</span>
 +
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+1 балл</span>
 +
 
 +
=== Количество предоставленных решений ===
 +
 
 +
'''Группа 318:''' 1
 +
 
 +
== <s>Теорема Гёделя о неполноте</s> ==
 +
 
 +
=== Описание задачи ===
 +
 
 +
Доказать теорему Гёделя о неполноте ('''лекция 10'''): либо адаптировать доказательство в лекции к общему случаю и доказать лемму о диагонали и утверждение об арифметизуемости графика, либо предоставить независимое доказательство.
 +
 
 +
Бонусы за решение задачи:
 +
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+14 баллов</span>
 +
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+11 баллов</span>
 +
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+8 баллов</span>
 +
 
 +
=== Количество предоставленных решений ===
 +
 
 +
'''Группа 318:''' 3 (все баллы розданы)
 +
 
 +
== Арифметика Пресбургера и математическая индукция ==
 +
 
 +
=== Описание задачи ===
 +
 
 +
Указать все места в доказательстве разрешимости арифметики Пресбургера ('''лекция 11'''), в которых существенно используется наличие схемы аксиом индукции в этой арифметике, и объяснить способ использования.
 +
 
 +
Бонусы за решение задачи:
 +
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+3 балла</span>
 +
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+2 балла</span>
 +
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+1 балл</span>
 +
 
 +
=== Количество предоставленных решений ===
 +
 
 +
'''Группа 318:''' 0
 +
 
 +
== <s>Определение экспоненты</s> ==
 +
 
 +
=== Описание задачи ===
 +
 
 +
Предложить (с обоснованием) определение одноместной функции 2^x (два в степени икс) в арифметической интерпретации на целых неотрицательных числах с сигнатурой <{0}, {+, x, s}, {=}> (семинар 5, задача 1, пункт 19).
 +
 
 +
''Если в обосновании будут содержаться китайская теорема об остатках, малая теорема Ферма или что-либо другое нетривиальное, то обоснование этого - часть решения''
 +
 
 +
Бонусы за решение задачи:
 +
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+5 баллов</span>
 +
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+4 балла</span>
 +
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+3 балла</span>
 +
 
 +
=== Количество предоставленных решений ===
 +
 
 +
'''Группа 318:''' 3 (все баллы розданы)
 +
 
 +
== Полнота семантической резолюции ==
 +
 
 +
=== Описание задачи ===
 +
 
 +
Доказать теорему полноты семантической резолюции (лекция 9).
 +
 
 +
Бонусы за решение задачи:
 +
* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+3 балла</span>
 +
* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+2 балла</span>
 +
* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+1 балла</span>
 +
 
 +
=== Количество предоставленных решений ===
 +
 
 +
'''Группа 318:''' 0
 +
 
 +
'''Группа 241:''' 0
 +
 
 +
== Законы темпоральной логики ==
 +
 
 +
Все пункты задачи относятся к ''законам темпоральной логики'' ('''лекция 17''').
 +
 
 +
* Выбрать одну пару двойственных левых частей для предполагаемых законов дистрибутивности (1+2, 3+4, 5+6, 7+8), сформулировать правые части, описывающие дистрибутивность операций в естественном понимании, и доказать и/или опровергнуть полученные законы.
 +
* Доказать закон неподвижной точки для одного из операторов U, R.
 +
* Сформулировать закон, ''не более тривиальный'', чем законы дистрибутивности для темпоральных операторов, и доказать его.
 +
 
 +
Один сдающий может выбрать только '''один''' закон (или пару законов дистрибутивности), '''не выбранный ранее''' другими сдавшими. <span style="background:#DDFFDD">+1 балл</span> каждому решившему.
 +
 
 +
''Статистика:''
 +
 
 +
* решены законы дистрибутивности 1+2, 3+4
 +
* один решивший: законы из разных пар, поэтому пары остаются незанятыми
 +
 
 +
== Model checking для LTL ==
 +
 
 +
Доказать (додоказать) утверждение, представленное в слайдах '''лекции 18'''.
 +
 
 +
* Утверждение на слайде 18 (106): однозначное задание согласованных предположений атомарными высказываниями и Next-time-формулами. <span style="background:#DDFFDD">+2 балла</span> каждому решившему.
 +
* Обоснование табличного метода model checking, достаточность, индуктивный переход, Until-формула: предложить обоснование для этого случая. <span style="background:#DDFFDD">+3 балла</span> каждому решившему.
 +
 
 +
-->
 +
 
 +
= Программа курса =
 +
 
 +
''Программа будет обновляться по ходу чтения курса''
 +
 
 +
== Классические логики ==
 
<ol>
 
<ol>
<li> Синтаксис и семантика логики предикатов. Термы, формулы, интерпретация. Отношение        выполнимости формулы на интерпретации.
+
<li> Логика высказываний: синтаксис, семантика; выполнимость, невыполнимость, общезначимость формул. Проблема общезначимости формул логики высказываний.
<li> Выполнимость,       общезначимость, противоречивость формул логики предикатов. Примеры        общезначимых и противоречивых формул логики предикатов. Модель. Логическое следствие. Теорема о логическом следствии.
+
<li> Метод семантических таблиц в логике высказываний: семантическая таблица, табличный вывод, теорема о табличном выводе.
<li> Проблемы        выполнимости и общезначимости. Пример формулы, не имеющей конечных       моделей.
+
<li> Логика предикатов: синтаксис (термы, формулы, свободные и связанные переменные), семантика (интерпретации, отношение выполнимости).
<li> Семантические        таблицы в логике предикатов. Табличный вывод. Теорема корректности       табличного вывода.
+
<li> Выполнимость, общезначимость и противоречивость формул логики предикатов. Модели. Логическое следование. Теорема о логическом следствии. Проблема общезначимости формул логики предикатов.
<li> Теорема полноты        табличного вывода.
+
<li> Пример выполнимой формулы логики предикатов, не имеющей конечных моделей.
<li> Теорема        Лёвенгейма-Сколема. Теорема компактности Мальцева.
+
<li> Метод семантических таблиц в логике предикатов: семантическая таблица, табличный вывод, теорема о табличной проверке общезначимости, теоремы о корректности и полноте табличного вывода.
<li> Равносильные       формулы. Примеры равносильных формул. Теорема о равносильной замене.
+
<li> Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Теорема Чёрча.
 +
<li> Равносильные формулы. Теорема о равносильной замене.
 
</ol>
 
</ol>
=== Метод резолюций ===
+
 
<ol start="8">
+
== Метод резолюций в логике предикатов ==
<li> Предваренная        нормальная форма. Теорема о приведении формулы к предваренной нормальной       форме.
+
<ol start="9">
<li> Сколемовская       стандартная форма. Теорема о приведении формулы к сколемовской        стандартной форме.
+
<li> Предварённая нормальная форма. Теорема о предварённой нормальной форме.
<li> Эрбрановский        универсум, эрбрановский базис, эрбрановские интерпретации. Теорема об        эрбрановской модели для сколемовской стандартной формы. Сведение       проблемы общезначимости формул к проблеме противоречивости систем       дизъюнктов. Теорема Эрбрана.
+
<li> Сколемовская стандартная форма. Алгоритм сколемизации предварённой нормальной формы. Теорема о сколемизации.
<li> Подстановки.        Применение подстановок к термам и формулам. Композиция подстановок.       Унификатор. Наиболее общий унификатор.
+
<li> Дизъюнкты. Сведение проблемы общезначимости формул к проблеме противоречивости систем дизъюнктов.
<li> Сведение задачи        унификации к задаче решения системы термальных уравнений. Лемма о       связке. Алгоритм унификации. Теорема о корректности и завершаемости        алгоритма унификации.
+
<li> Подстановки. Композиция подстановок. Унификатор. Наиболее общий унификатор. Задача унификации выражений логики предикатов.
<li> Метод резолюций для        логики предикатов: правила резолюции и склейки, резолютивный вывод.       Теорема корректности резолютивного вывода.
+
<li> Лемма о связке. Алгоритм унификации. Теорема об унификации.
<li> Лемма о подъеме.       Теорема полноты резолютивного вывода для логики предикатов.
+
<li> Правило резолюции. Правило склейки. Резолютивный вывод. Теорема о корректности резолютивного вывода.
<li> Общая схема       доказательства общезначимости формул логики предикатов методом        резолюций. Стратегии резолютивного вывода.
+
<li> Эрбрановский универсум. Эрбрановский базис. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях. Теорема Эрбрана.
 +
<li> Лемма об основных дизъюнктах. Лемма о подъёме. Теорема о полноте резолютивного вывода.
 +
<li> Метод резолюций: общая схема, применение.
 
</ol>
 
</ol>
=== Основы логического программирования ===
+
 
<ol start="16">
+
== Логические исчисления ==
<li> Использование        метода резолюций для нахождения ответов на запросы. Истолкование        резолютивного вывода как вычисления. Примеры вычислительных возможностей        резолютивного вывода.
+
<ol start="18">
<li> Хорновские        дизъюнкты. Синтаксис языка логического программирования: логические        программы и запросы. Декларативная семантика логических программ.        Правильный ответ.
+
<li> Логические исчисления. Исчисления высказываний и исчисления предикатов. Доказуемость (выводимость) формул.
<li> Теорема о        пересечении эрбрановских моделей логических программ. Теорема о        наименьшей эрбрановской модели. Теорема об основных правильных ответах.
+
<li> Натуральное исчисление высказываний. Корректность и полнота исчисления.
<li> SLD-резолюция.       SLD-резолютивные вычисления (опровержения) логических программ.        Процедурная интерпретация SLD-выводов. Примеры SLD-опровержений        успешных, тупиковых и бесконечных. Вычислимый ответ. Операционная        (процедурная) семантика логических программ.
+
<li> Натуральное исчисление предикатов. Корректность и полнота исчисления.
<li> Теорема корректности SLD-резолютивных вычислений        логических программ.
+
<li> Исчисление предикатов гильбертовского типа. Теорема Гёделя о полноте.
<li> Множество успехов логической программы. Лемма о подъеме для        хорновских дизъюнктов. Теоремы полноты SLD-резолютивных        вычислений логических программ.
+
<li> Правило вычислений        и его роль. R-вычислимый ответ. Переключательная лемма. Теорема о        независимости правила вычислений. Теорема сильной полноты SLD-резолюции.
+
<li> Дерево        SLD-вычислений логических программ. Стратегии вычислений. Полные и неполные стратегии вычислений. Стандартная        стратегия исполнения логических программ. Неполнота стандартной        стратегии.
+
<li> Управление        исполнением логических программ. Оператор отсечения. Операционная        семантика оператора отсечения.
+
<li> Отрицание в        Прологе. Допущение замкнутости мира. Отрицание как неудача. Эффект        немонотонности вычислений логических программ с оператором отрицания.
+
<li> Встроенные        предикаты и функции. Операционная семантика встроенных средств.
+
<li> Теорема о       вычислительной универсальности чистого Пролога. Теорема Чёрча о        неразрешимости логики предикатов первого порядка.
+
 
</ol>
 
</ol>
=== Неклассические прикладные логики ===
+
 
<ol start="28">
+
== Неклассические прикладные логики ==
<li> Интуиционистская логика. Модели Крипке для интуиционистской логики.        Примеры интуиционистски общезначимых и необщезначимых формул. Модальные логики. Модели Крипке для модальных логик.         Эпистемические логики. Темпоральные логики.
+
<ol start="22">
<li> Проблема верификации последовательных программ.         Операционная семантика типовых программных конструкций. Предусловие и постусловие. Частичная корректность программ.       Тройки Хоара и их содержательный смысл. Правила вывода в логике Хоара для доказательства частичной корректности        последовательных программ.
+
<li> Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики. Логика линейного времени. Логика деревьев вычислений.
<li> Моделирование программ системами переходов. Темпоральная логика        высказываний линейного времени (LTL): синтаксис и семантика. Применение темпоральных логик для спецификации поведения         реагирующих программных систем.
+
<li> Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Корректность и частичная корректность программ. Тройки Хоара. Логика Хоара. Корректность вывода в логике Хоара. Слабейшее предусловие. Инвариант цикла.
<li> Задача проверки выполнимости формул LTL на конечной модели. Равносильные преобразования формул LTL. Табличный алгоритм проверки выполнимости формул LTL на конечной модели: основные этапы.
+
<li> Верификация распределённых систем. Логика линейного времени: синтаксис, семантика. Основные равносильности в логике линейного времени. Применение темпоральных логик для спецификации поведения распределённых систем.
 +
<li> Размеченные системы переходов. Моделирование программ системами переходов. Семантика чередующихся вычислений. Задача верификации (проверки моделей; model checking) для логики линейного времени.
 +
<li> Табличный алгоритм верификации для логики линейного времени. Упрощение формул. Замыкание Фишера-Ладнера. Согласованные предположения. Система Хинтикки. Сведение задачи верификации к графовым задачам.
 
</ol>
 
</ol>
 +
 +
= Рекомендованная литература =
  
 
== Основная литература ==
 
== Основная литература ==
Строка 123: Строка 462:
 
# Ковальский Р. Логика в решении проблем. М.: Наука, 1990. 277 с.
 
# Ковальский Р. Логика в решении проблем. М.: Наука, 1990. 277 с.
 
# Логический подход к искусственному интеллекту (от модальной логики к логике баз данных). М.:Мир, 1998. 495 с.
 
# Логический подход к искусственному интеллекту (от модальной логики к логике баз данных). М.:Мир, 1998. 495 с.
 
== См. также ==
 
 
[[Media:MatLog_tasks.pdf| Задачи для семинарских занятий по курсу математической логики и логического программирования]]
 
 
[[Категория:Лекционные курсы кафедры МК]]
 

Текущая версия на 19:24, 21 февраля 2021

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

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


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

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

Блок 1 (вводный). Что такое логика. Содержание лекций. Несколько логических парадоксов.

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

Блок 3. Логика предикатов: синтаксис, семантика.

Блок 4. Как формализовать предложение на языке логики предикатов (пример).

Блок 5. Логика предикатов: выполнимые и общезначимые формулы; модели формул; логическое следствие; проблема общезначимости формул (постановка).

Блок 6. Логика предикатов: почему бы не проверять общезначимость формул "в лоб"?

Блок 7. Метод семантических таблиц в логике высказываний.

Блок 8. Метод семантических таблиц в логике предикатов: семантические таблицы.

Блок 9. Подстановки (основные определения).

Блок 10. Метод семантических таблиц в логике предикатов: табличный вывод.

Блок 11. Метод семантических таблиц в логике предикатов: корректность табличного вывода.

Блок 12. Метод семантических таблиц в логике предикатов: полнота табличного вывода.

Блок 13. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Автоматизация доказательства теорем.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Лекция..

Семинары

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

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

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

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

Экзамен

Формат проведения и длительность экзамена: письменно, 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. Решить хотя бы 4 типовые задачи на 2 балла (т.е. правильно или с незначительными недочётами).
  2. Набрать хотя бы 20 баллов суммарно за всё (типовые задачи, теория, премиальные задачи).

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

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

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

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

Сдача теории

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  • первый сдавший: +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 с.