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

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
 
(не показаны 292 промежуточных версий 2 участников)
Строка 1: Строка 1:
Обязательный курс для студентов 318 группы 6 семестра обучения. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].
+
[[Категория:Лекционные курсы кафедры МК]]
  
'''Внимание!''' ''В весеннем семестре 2016 года планируется существенное изменение программы курса. Информацию о лекциях 2015 года сейчас можно найти [[Математическая логика и логическое программирование (группа 318)#Информация о лекциях 2015 года|здесь]].''
+
Актуальность информации: весенний семестр 2023/2024 учебного года.
  
== Слайды лекций ==
+
Обязательный курс для студентов групп 318 и 319/2, ''а также 241 и 242 (Математическая логика и теория алгоритмов)''. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].
  
''В этом разделе будут выкладываться слайды лекций по мере их появления.''
+
= Слайды лекций =
  
'''[[Media: Mathlog_318_lecture_1.pdf|Лекция 1.]]''' Что такое логика? Содержание лекций. История логики. Логические парадоксы.
+
[[Media: Mathlog_318_b1.pdf|Блок 1]] (вводный). Что такое логика. Несколько логических парадоксов. Чего ожидать в курсе.
  
'''[[Media: Mathlog_318_lecture_2.pdf|Лекция 2.]]''' Логика высказываний: синтаксис, семантика, общезначимость, выполнимость, метод семантических таблиц. SAT.
+
[[Media: Mathlog_318_b2.pdf|Блок 2]]. Логика высказываний: синтаксис, семантика.
  
'''[[Media: Mathlog_318_lecture_3.pdf|Лекция 3.]]''' Логика предикатов. Синтаксис: термы и формулы. Семантика: интерпретации, отношение выполнимости. Выполнимые и общезначимые формулы. Модели. Логическое следствие. Проблема общезначимости формул.
+
[[Media: Mathlog_318_b3.pdf|Блок 3]]. Логика предикатов: синтаксис, семантика.
  
== Информация о лекциях 2015 года ==
+
[[Media: Mathlog_318_b4.pdf|Блок 4]]. Как формализовать предложение на языке логики предикатов (пример).
  
<!--
+
[[Media: Mathlog_318_b5.pdf|Блок 5]]. Логика высказываний: выполнимые и общезначимые формулы.
  
=== Контрольная работа ===
+
[[Media: Mathlog_318_b6.pdf|Блок 6]]. Логика предикатов: выполнимые и общезначимые формулы; модели формул; логическое следствие; проблема общезначимости формул (постановка).
  
Письменная контрольная работа состоялась '''09.04.2015 на 4 паре (14:35-16:10) в аудитории 613'''.
+
[[Media: Mathlog_318_b7.pdf|Блок 7]]. Логика предикатов: можно ли проверить общезначимость формулы "в лоб"?
  
'''[[Media:Mllp_318_test_2015_results.docx|Результаты контрольной работы здесь.]]'''
+
[[Media: Mathlog_318_b8.pdf|Блок 8]]. Метод семантических таблиц: семантические таблицы.
  
-->
+
[[Media: Mathlog_318_b9.pdf|Блок 9]]. Подстановки (основные определения).
  
=== Темы лекций 2015 года ===
+
[[Media: Mathlog_318_b10.pdf|Блок 10]]. Метод семантических таблиц: табличный вывод.
  
'''Лекция 1.''' Что изучает логика? Логика в информатике. Структура курса. Исторические сведения. Логические парадоксы.
+
[[Media: Mathlog_318_b11.pdf|Блок 11]]. Метод семантических таблиц: корректность табличного вывода.
  
'''Лекция 2.''' Классическая логика предикатов первого порядка. Синтаксис: термы и формулы. Семантика: интерпретации, Выполнимость.
+
[[Media: Mathlog_318_b12.pdf|Блок 12]]. Метод семантических таблиц: полнота табличного вывода.
  
'''Лекция 3.''' Выполнимые и общезначимые формулы. Модели. Логическое следование. Проблема общезначимости. Семантические таблицы.
+
[[Media: Mathlog_318_b13.pdf|Блок 13]]. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Автоматизация доказательства теорем.
  
'''Лекция 4.''' Подстановки. Табличный вывод. Корректность табличного вывода.
+
[[Media: Mathlog_318_b14.pdf|Блок 14]]. Общая схема метода резолюций.
  
'''Лекция 5.''' Полнота табличного вывода. Теорема Левенгейма-Сколема. Теорема компактности Мальцева. Автоматическое доказательство теорем.
+
[[Media: Mathlog_318_b15.pdf|Блок 15]]. Равносильность формул.
  
'''Лекция 6.''' Общая схема метода резолюций. Равносильные формулы. Теорема о равносильной замене. Предваренная нормальная форма. Сколемовская стандартная форма. Системы дизъюнктов.
+
[[Media: Mathlog_318_b16.pdf|Блок 16]]. Предварённая нормальная форма (ПНФ).
  
'''Лекция 7.''' Эрбрановские интерпретации. Теорема Эрбрана. Задача унификации.
+
[[Media: Mathlog_318_b17.pdf|Блок 17]]. Сколемовская стандартная форма (ССФ).
  
'''Лекция 8.''' Алгоритм унификации.
+
[[Media: Mathlog_318_b18.pdf|Блок 18]]. Системы дизъюнктов.
  
'''Лекция 9.''' Резолютивный вывод. Корректность резолютивного вывода. Применение метода резолюций.
+
[[Media: Mathlog_318_b19.pdf|Блок 19]]. Композиция подстановок. Постановка задачи унификации.
  
'''Лекция 10.''' Полнота резолютивного вывода.
+
[[Media: Mathlog_318_b20.pdf|Блок 20]]. Алгоритм унификации атомарных формул.
  
'''Лекция 11.''' Стратегии резолютивного вывода. Вычислительные возможности метода резолюций.
+
[[Media: Mathlog_318_b21.pdf|Блок 21]]. Монотонность и транзитивность отношения логического следования.
  
'''Лекция 12.''' Хорновские логические программы: синтаксис, декларативная семантика, операционная семантика. SLD-резолютивные вычисления.
+
[[Media: Mathlog_318_b22.pdf|Блок 22]]. Резолютивный вывод. Корректность резолютивного вывода.
  
'''Лекция 13.''' Корректность и полнота операционной семантики хорновских логических программ.
+
[[Media: Mathlog_318_b23.pdf|Блок 23]]. Обоснование общезначимости формулы методом резолюций (пример).
  
'''Лекция 14.''' Правила выбора подцели. Деревья SLD-резолютивных вычислений. Правила поиска. Стратегии вычисления.
+
[[Media: Mathlog_318_b24.pdf|Блок 24]]. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях.
+
'''Лекция 15.''' Алгоритмическая полнота логических программ. Моделирование машин Тьюринга логическим программами. Теорема Чёрча-Тьюринга.
+
  
'''Лекция 16.''' Встроенные операторы. Управление вычислениями. Оператор отсечения. Отрицание в логическом программировании. Оператор отрицания.
+
[[Media: Mathlog_318_b25.pdf|Блок 25]]. Теорема Эрбрана. Полнота резолютивного вывода.
  
<strike>Лекция 17. Интуиционистская логика.</strike>
+
[[Media: Mathlog_318_b26.pdf|Блок 26]]. Даша, Саша, Паша, пиво и метод семантических таблиц с методом резолюций.
  
'''Лекция 17.''' Модальные логики. Правильные программы. Императивные программы. Задача верификации программ. Логика Хоара. Автоматическая проверка правильности программ.
+
[[Media: Mathlog_318_b27.pdf|Блок 27]]. Как устроены математические доказательства. Логические исчисления.
  
'''Лекция 18.''' Верификация распределенных систем. Логика линейного времени LTL. Размеченные системы переходов. Задача model checking.
+
[[Media: Mathlog_318_b28.pdf|Блок 28]]. Натуральное исчисление высказываний: основные определения.
  
'''Лекция 19.''' Задача model checking для LTL. Подформулы Фишера-Ладнера. Табличный метод model checking. Система Хинтикки. Алгоритм model checking.
+
[[Media: Mathlog_318_b29.pdf|Блок 29]]. Натуральное исчисление высказываний: правило монотонности, закон исключённого третьего, корректность.
  
=== Программа 2015 года ===
+
[[Media: Mathlog_318_b30.pdf|Блок 30]]. Натуральное исчисление высказываний: правило сечения, правило полного перебора, правило приведения к абсурду, полнота.
  
==== Логика предикатов первого порядка ====
+
[[Media: Mathlog_318_b31.pdf|Блок 31]]. Натуральное исчисление предикатов: основные определения, корректность.
 +
 
 +
[[Media: Mathlog_318_b32.pdf|Блок 32]]. Гильбертовское исчисление предикатов. Теорема Гёделя о полноте (формулировка).
 +
 
 +
''Слайды будут появляться по мере чтения лекций.''
 +
 
 +
== Прошлогодние слайды ==
 +
 
 +
[[Media: Mathlog_318_b33.pdf|Блок 33]]. Натуральное исчисление предикатов: полнота.
 +
 
 +
[[Media: Mathlog_318_b34.pdf|Блок 34]]. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.
 +
 
 +
[[Media: Mathlog_318_b35.pdf|Блок 35]]. Машины Тьюринга (МТ).
 +
 
 +
[[Media: Mathlog_318_b36.pdf|Блок 36]]. Теорема Чёрча.
 +
 
 +
[[Media: Mathlog_318_b37.pdf|Блок 37]]. Аксиоматические теории первого порядка. Проблема общезначимости формул в теории.
 +
 
 +
[[Media: Mathlog_318_b38.pdf|Блок 38]]. Основные свойства аксиоматических теорий.
 +
 
 +
[[Media: Mathlog_318_b39.pdf|Блок 39]]. Арифметические интерпретации и теории.
 +
 
 +
[[Media: Mathlog_318_b40.pdf|Блок 40]]. Определения и выразимость.
 +
 
 +
[[Media: Mathlog_318_b41.pdf|Блок 41]]. Формальная арифметика. Теорема Гёделя о неполноте.
 +
 
 +
[[Media: Mathlog_318_b42.pdf|Блок 42]]. Арифметика Пресбургера.
 +
 
 +
[[Media: Mathlog_318_b43.pdf|Блок 43]]. Модальные логики.
 +
 
 +
[[Media: Mathlog_318_b44.pdf|Блок 44]]. Эпистемические логики.
 +
 
 +
[[Media: Mathlog_318_b45.pdf|Блок 45]]. Темпоральные логики.
 +
 
 +
[[Media: Mathlog_318_b46.pdf|Блок 46]]. Интуиционистская логика.
 +
 
 +
[[Media: Mathlog_318_b47.pdf|Блок 47]]. Формальная верификация.
 +
 
 +
[[Media: Mathlog_318_b48.pdf|Блок 48]]. Модельные императивные программы. Постановка задачи верификации программ.
 +
 
 +
[[Media: Mathlog_318_b49.pdf|Блок 49]]. Логика Хоара. Автоматизация проверки правильности программ.
 +
 
 +
[[Media: Mathlog_318_b50.pdf|Блок 50]]. Проверка правильности распределённых систем. Пара слов о методе model checking.
 +
 
 +
[[Media: Mathlog_318_b51.pdf|Блок 51]]. Размеченные системы переходов.
 +
 
 +
[[Media: Mathlog_318_b52.pdf|Блок 52]]. Спецификация систем при помощи темпоральных логик.
 +
 
 +
[[Media: Mathlog_318_b53.pdf|Блок 53]]. Алгоритм model checking для CTL.
 +
 
 +
= Семинары =
 +
 
 +
''Материалы семинаров будут обновляться по мере проведения занятий''
 +
 
 +
Семинары 1-4 проводятся по [[Media:MatLog_tasks.pdf| этому сборнику задач.]]
 +
 
 +
Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]]
 +
 
 +
[[Media:Mathlog_318_seminar_natural_inference.pdf| Материалы семинара 5-6 (натуральное исчисление).]]
 +
 
 +
= Контрольные работы =
 +
 
 +
Контрольные работы проводятся письменно, длительность каждой - 90 минут.
 +
 
 +
В контрольных работах встретятся 4 типовые задачи со следующими темами:
 +
# Формализовать в логике предикатов предложение, записанное на естественном языке.
 +
# Обосновать общезначимость формулы логики предикатов методом семантических таблиц.
 +
# Обосновать общезначимость формулы логики предикатов методом резолюций.
 +
# Доказать формулу в натуральном исчислении предикатов.
 +
 
 +
Оценка решений типовых задач:
 +
* Максимальная оценка - 4 балла.
 +
* Если решение в целом верно, но содержит редкие ошибки серьёзнее опечаток, то оно оценивается в 3 балла.
 +
* Если решение содержит серьёзные ошибки, но имеет структуру, в целом разумно соотносящуюся с правильной, то задача оценивается в 2 балла.
 +
* Если в решении обнаружены правильные элементы, в заметном, но всё же малом количестве, то задача оценивается в 1 балл.
 +
 
 +
Теоретические вопросы даются в форме теста с множественным выбором: из предложенных вариантов ответа требуется выбрать правильные (один, несколько или ни одного), обоснование не требуется.
 +
Правильно решённый теоретический вопрос оценивается в 1 балл.
 +
 
 +
'''Первая контрольная работа''' будет содержать
 +
* 3 типовые задачи по темам 1-3 и
 +
* 9 теоретических вопросов по прочитанным лекциям.
 +
 
 +
'''Вторая контрольная работа''' будет содержать
 +
* 4 типовые задачи по всем темам и
 +
* 5 теоретических вопросов по лекциям, не попавшим в первую контрольную работу.
 +
 
 +
'''Остальные контрольные работы''' будут содержать
 +
* 4 типовые задачи по всем темам и
 +
* 14 теоретических вопросов по всем лекциям.
 +
 
 +
= Зачёт =
 +
 
 +
На зачёте оцениваются результаты, относящиеся к решению типовых задач, знанию теории и работе в семестре.
 +
При проставлении зачёта учитывается 6 технических оценок:
 +
* Четыре оценки за типовые задачи, по одной за каждую задачу.
 +
* Оценка за знание теории. Максимум - 14 баллов.
 +
* Оценка за решение премиальных задач.
 +
 
 +
Для получения зачёта требуется получить два результата:
 +
# Набрать хотя бы 11 баллов за типовые задачи.
 +
# Набрать хотя бы 20 баллов суммарно за всё (типовые задачи, теория, премиальные задачи).
 +
 
 +
Баллы за типовые задачи и за теорию набираются на [[#Контрольные работы|контрольных работах]].
 +
 
 +
Для решения каждой типовой задачи будет предложено несколько попыток.
 +
При проставлении зачёта учитывается '''максимальная''' оценка за задачу среди всех попыток её решить.
 +
 
 +
При проставлении зачёта учитывается '''максимальная''' оценка за теорию среди полученных
 +
* суммарно за первые две контрольные работы и
 +
* за каждую из следующих контрольных работ.
 +
 
 +
= Экзамен =
 +
 
 +
Формат проведения и длительность экзамена: письменно, 120 минут.
 +
 
 +
Экзаменационная работа содержит 10 задач и оценивается по шкале от 0 до 37 технических баллов.
 +
К этим техническим баллам прибавляются баллы за выполнение премиальных задач и поощрение/штраф за [[#Контрольная работа|контрольную работу]].
 +
Согласно набранной сумме технических баллов выставляется оценка:
 +
* хотя бы 30: '''отлично''';
 +
* хотя бы 23, но менее 30: '''хорошо''';
 +
* хотя бы 16, но менее 23: '''удовлетворительно''';
 +
* менее 16: '''неудовлетворительно'''.
 +
 
 +
Баллы за экзаменационную работу складываются из баллов за каждую задачу, предложенную в работе:
 +
* Каждая из задач 1-4 оценивается в 4 балла. Темы задач:
 +
*# Формализовать в логике предикатов предложение, записанное на естественном языке.
 +
*# Обосновать общезначимость формулы логики предикатов методом семантических таблиц.
 +
*# Обосновать общезначимость формулы логики предикатов методом резолюций.
 +
*# Доказать формулу в натуральном исчислении предикатов.
 +
* Каждая из задач 5-7 оценивается в 3 балла и состоит из трёх частей:
 +
*# Сформулировать утверждение, определение и т.п.
 +
*# Ответить на вопрос "на понимание", так или иначе связанный с формулировкой.
 +
*# Аргументировать (обосновать) ответ на вопрос.
 +
* Каждая из задач 8-10 оценивается в 4 балла и устроена так:
 +
** Из нескольких предложенных вариантов ответа выбрать правильные (один, несколько или ни одного) и '''обосновать''' выбранные ответы.
 +
** Невыбранные ответы обосновывать не нужно.
 +
 
 +
== Контрольная работа ==
 +
 
 +
На оценку за экзамен влияет первая [[#Контрольные работы|контрольная работа]].
 +
Максимальная техническая оценка за эту работу - 21 балл.
 +
В зависимости от технических баллов, набранных за первую контрольную работу, определяется поощрение или штраф к техническим баллам за экзамен:
 +
* Набрано хотя бы 19 баллов: бонус <span style="background:#DDFFDD">+3 балла</span>;
 +
* Набрано хотя бы 16, но менее 19 баллов: бонус <span style="background:#DDFFDD">+2 балла</span>;
 +
* Набрано хотя бы 13, но менее 16 баллов: бонус <span style="background:#DDFFDD">+1 балл</span>;
 +
* Набрано хотя бы 10, но менее 13 баллов: <span style="background:#CCCCCC">0 баллов</span>;
 +
* Набрано хотя бы 7, но менее 10 баллов: штраф <span style="background:#FFDDDD">-1 балл</span>;
 +
* Набрано хотя бы 4, но менее 7 баллов: штраф <span style="background:#FFDDDD">-2 балла</span>;
 +
* Набрано менее 4 баллов: штраф <span style="background:#FFDDDD">-3 балла</span>;
 +
* Неявка без уважительной причины: штраф <span style="background:#FFDDDD">-3 балла</span>;
 +
* Неявка по уважительной причине: <span style="background:#CCCCCC">0 баллов</span>.
 +
 
 +
= Премиальные задачи =
 +
 
 +
Общие условия сдачи решений премиальных задач:
 +
* Можно как прислать письменное решение, так и обсудить решение устно. Если прислано письменное решение и к нему есть вопросы, то для ответов на эти вопросы может потребоваться дополнительное устное обсуждение.
 +
* При подготовке решения и во время его сдачи можно пользоваться любыми материалами.
 +
* При сдаче может быть проверено понимание '''каждой''' детали предложенного решения - следует быть к этому готовым.
 +
* Решение принимается, когда по нему не остаётся неотвеченных вопросов.
 +
 
 +
'''Бонусы за решение задач формулируются для одной учебной группы''' и распределяются внутри одной группы независимо от другой.
 +
Например, "''первый''" трактуется как "''первый в группе 318, а также первый в группе 319/2, а также ...''".
 +
 
 +
Условия задач и статистика принятых решений будут обновляться и доводиться до слушателей по мере чтения курса.
 +
 
 +
= Программа курса =
 +
 
 +
''Программа будет обновляться согласно фактически прочитанному материалу''
 +
 
 +
== Классические логики ==
 
<ol>
 
<ol>
<li> Синтаксис и семантика логики предикатов. Термы, формулы, интерпретация. Отношение        выполнимости формулы на интерпретации.
+
<li> Логика высказываний: синтаксис, семантика; выполнимость и общезначимость формул. Проблема общезначимости формул логики высказываний.
<li> Выполнимость,        общезначимость, противоречивость формул логики предикатов. Примеры        общезначимых и противоречивых формул логики предикатов. Модель. Логическое следствие. Теорема о логическом следствии.
+
<li> Метод семантических таблиц в логике высказываний: семантическая таблица, табличный вывод, теорема о табличном выводе.
<li> Проблемы        выполнимости и общезначимости. Пример формулы, не имеющей конечных       моделей.
+
<li> Логика предикатов: синтаксис (термы, формулы, свободные и связанные переменные), семантика (интерпретации, отношение выполнимости).
<li> Семантические        таблицы в логике предикатов. Табличный вывод. Теорема корректности       табличного вывода.
+
<li> Выполнимость и общезначимость формул логики предикатов. Модели. Логическое следование. Теорема о логическом следствии. Проблема общезначимости формул логики предикатов.
<li> Теорема полноты        табличного вывода.
+
<li> Пример выполнимой формулы логики предикатов, не имеющей конечных моделей.
<li> Теорема        Лёвенгейма-Сколема. Теорема компактности Мальцева.
+
<li> Метод семантических таблиц в логике предикатов: семантическая таблица, табличный вывод, теорема о табличной проверке общезначимости, теоремы о корректности и полноте табличного вывода.
<li> Равносильные       формулы. Примеры равносильных формул. Теорема о равносильной замене.
+
<li> Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева.
 +
<li> Машины Тьюринга. Теорема Чёрча.
 +
<li> Равносильные формулы. Теорема о равносильной замене.
 
</ol>
 
</ol>
==== Метод резолюций ====
+
 
<ol start="8">
+
== Метод резолюций в логике предикатов ==
<li> Предваренная        нормальная форма. Теорема о приведении формулы к предваренной нормальной       форме.
+
<ol start="10">
<li> Сколемовская       стандартная форма. Теорема о приведении формулы к сколемовской        стандартной форме.
+
<li> Предварённая нормальная форма. Теорема о предварённой нормальной форме.
<li> Эрбрановский        универсум, эрбрановский базис, эрбрановские интерпретации. Теорема об        эрбрановской модели для сколемовской стандартной формы. Сведение       проблемы общезначимости формул к проблеме противоречивости систем       дизъюнктов. Теорема Эрбрана.
+
<li> Сколемовская стандартная форма. Алгоритм сколемизации предварённой нормальной формы. Теорема о сколемизации.
<li> Подстановки.        Применение подстановок к термам и формулам. Композиция подстановок.       Унификатор. Наиболее общий унификатор.
+
<li> Дизъюнкты. Сведение проблемы общезначимости формул к проблеме невыполнимости систем дизъюнктов.
<li> Сведение задачи        унификации к задаче решения системы термальных уравнений. Лемма о       связке. Алгоритм унификации. Теорема о корректности и завершаемости        алгоритма унификации.
+
<li> Подстановки. Композиция подстановок. Унификатор. Наиболее общий унификатор. Задача унификации выражений логики предикатов.
<li> Метод резолюций для        логики предикатов: правила резолюции и склейки, резолютивный вывод.       Теорема корректности резолютивного вывода.
+
<li> Лемма о связке. Алгоритм унификации. Теорема об унификации.
<li> Лемма о подъеме.       Теорема полноты резолютивного вывода для логики предикатов.
+
<li> Правило резолюции. Правило склейки. Резолютивный вывод. Теорема о корректности резолютивного вывода.
<li> Общая схема       доказательства общезначимости формул логики предикатов методом        резолюций. Стратегии резолютивного вывода.
+
<li> Эрбрановский универсум. Эрбрановский базис. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях. Теорема Эрбрана.
 +
<li> Лемма об основных дизъюнктах. Лемма о подъёме. Теорема о полноте резолютивного вывода.
 +
<li> Метод резолюций: общая схема, применение.
 
</ol>
 
</ol>
==== Основы логического программирования ====
+
 
<ol start="16">
+
== Логические исчисления ==
<li> Использование        метода резолюций для нахождения ответов на запросы. Истолкование        резолютивного вывода как вычисления. Примеры вычислительных возможностей        резолютивного вывода.
+
<ol start="19">
<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="23">
 +
<li> Аксиоматические теории первого порядка: основные определения, проблема общезначимости формул в теории.
 +
<li> Основные свойства аксиоматических теорий: непротиворечивость, элементарность, полнота, разрешимость.
 +
<li> Определения и выразимость в интерпретациях. Теорема о подстановке определения.
 +
<li> Формальная арифметика. Теорема Гёделя о неполноте (формулировка и схема доказательства).
 +
<li> Арифметика Пресбургера, её разрешимость и выразительность.
 +
</ol>
 +
 
 +
== Неклассические прикладные логики ==
 
<ol start="28">
 
<ol start="28">
<li> Интуиционистская логика. Модели Крипке для интуиционистской логики.       Примеры интуиционистски общезначимых и необщезначимых формул. Модальные логики. Модели Крипке для модальных логик.         Эпистемические логики. Темпоральные логики.
+
<li> Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики. Логика линейного времени. Логика деревьев вычислений.
<li> Проблема верификации последовательных программ.         Операционная семантика типовых программных конструкций. Предусловие и постусловие. Частичная корректность программ.       Тройки Хоара и их содержательный смысл. Правила вывода в логике Хоара для доказательства частичной корректности        последовательных программ.
+
<li> Интуиционистская логика.
<li> Моделирование программ системами переходов. Темпоральная логика        высказываний линейного времени (LTL): синтаксис и семантика. Применение темпоральных логик для спецификации поведения         реагирующих программных систем.
+
<li> Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Полная и частичная корректность программ. Тройки Хоара. Логика Хоара. Корректность вывода в логике Хоара. Слабейшее предусловие. Инвариант цикла.
<li> Задача проверки выполнимости формул LTL на конечной модели. Равносильные преобразования формул LTL. Табличный алгоритм проверки выполнимости формул LTL на конечной модели: основные этапы.
+
<li> Размеченные системы переходов. Моделирование программ системами переходов. Логика деревьев вычислений (CTL): синтаксис, семантика, основные равносильности, применение для спецификации поведения распределённых систем. Задача проверки моделей (model checking) относительно CTL: формулировка, решающий алгоритм.
 
</ol>
 
</ol>
  
=== Основная литература ===
+
= Рекомендованная литература =
 +
 
 +
== Основная литература ==
 
# Клини С. Математическая логика. М.:Мир, 1973, 480 с.
 
# Клини С. Математическая логика. М.:Мир, 1973, 480 с.
 
# Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.:Мир, 1983. 360 с.
 
# Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.:Мир, 1983. 360 с.
Строка 122: Строка 299:
 
# Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: model checking. Изд-во МЦНМО, Москва, 2002, 405 с.
 
# Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: model checking. Изд-во МЦНМО, Москва, 2002, 405 с.
  
=== Дополнительная литература ===
+
== Дополнительная литература ==
  
 
# Мендельсон Э. Введение в математическую логику. М.:Наука, 1984. 319 с.
 
# Мендельсон Э. Введение в математическую логику. М.:Наука, 1984. 319 с.
Строка 137: Строка 314:
 
# Ковальский Р. Логика в решении проблем. М.: Наука, 1990. 277 с.
 
# Ковальский Р. Логика в решении проблем. М.: Наука, 1990. 277 с.
 
# Логический подход к искусственному интеллекту (от модальной логики к логике баз данных). М.:Мир, 1998. 495 с.
 
# Логический подход к искусственному интеллекту (от модальной логики к логике баз данных). М.:Мир, 1998. 495 с.
 
=== См. также ===
 
 
[[Media:MatLog_tasks.pdf| Задачи для семинарских занятий по курсу математической логики и логического программирования]]
 
 
[[Категория:Лекционные курсы кафедры МК]]
 

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Блок 14. Общая схема метода резолюций.

Блок 15. Равносильность формул.

Блок 16. Предварённая нормальная форма (ПНФ).

Блок 17. Сколемовская стандартная форма (ССФ).

Блок 18. Системы дизъюнктов.

Блок 19. Композиция подстановок. Постановка задачи унификации.

Блок 20. Алгоритм унификации атомарных формул.

Блок 21. Монотонность и транзитивность отношения логического следования.

Блок 22. Резолютивный вывод. Корректность резолютивного вывода.

Блок 23. Обоснование общезначимости формулы методом резолюций (пример).

Блок 24. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях.

Блок 25. Теорема Эрбрана. Полнота резолютивного вывода.

Блок 26. Даша, Саша, Паша, пиво и метод семантических таблиц с методом резолюций.

Блок 27. Как устроены математические доказательства. Логические исчисления.

Блок 28. Натуральное исчисление высказываний: основные определения.

Блок 29. Натуральное исчисление высказываний: правило монотонности, закон исключённого третьего, корректность.

Блок 30. Натуральное исчисление высказываний: правило сечения, правило полного перебора, правило приведения к абсурду, полнота.

Блок 31. Натуральное исчисление предикатов: основные определения, корректность.

Блок 32. Гильбертовское исчисление предикатов. Теорема Гёделя о полноте (формулировка).

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

Прошлогодние слайды

Блок 33. Натуральное исчисление предикатов: полнота.

Блок 34. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.

Блок 35. Машины Тьюринга (МТ).

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

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

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

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

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

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

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

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

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

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

Блок 46. Интуиционистская логика.

Блок 47. Формальная верификация.

Блок 48. Модельные императивные программы. Постановка задачи верификации программ.

Блок 49. Логика Хоара. Автоматизация проверки правильности программ.

Блок 50. Проверка правильности распределённых систем. Пара слов о методе model checking.

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

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

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

Семинары

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Зачёт

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

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

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

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

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

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

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

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

Экзамен

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  1. Логика высказываний: синтаксис, семантика; выполнимость и общезначимость формул. Проблема общезначимости формул логики высказываний.
  2. Метод семантических таблиц в логике высказываний: семантическая таблица, табличный вывод, теорема о табличном выводе.
  3. Логика предикатов: синтаксис (термы, формулы, свободные и связанные переменные), семантика (интерпретации, отношение выполнимости).
  4. Выполнимость и общезначимость формул логики предикатов. Модели. Логическое следование. Теорема о логическом следствии. Проблема общезначимости формул логики предикатов.
  5. Пример выполнимой формулы логики предикатов, не имеющей конечных моделей.
  6. Метод семантических таблиц в логике предикатов: семантическая таблица, табличный вывод, теорема о табличной проверке общезначимости, теоремы о корректности и полноте табличного вывода.
  7. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева.
  8. Машины Тьюринга. Теорема Чёрча.
  9. Равносильные формулы. Теорема о равносильной замене.

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

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

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

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

Аксиоматические теории

  1. Аксиоматические теории первого порядка: основные определения, проблема общезначимости формул в теории.
  2. Основные свойства аксиоматических теорий: непротиворечивость, элементарность, полнота, разрешимость.
  3. Определения и выразимость в интерпретациях. Теорема о подстановке определения.
  4. Формальная арифметика. Теорема Гёделя о неполноте (формулировка и схема доказательства).
  5. Арифметика Пресбургера, её разрешимость и выразительность.

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

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

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

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

  1. Клини С. Математическая логика. М.:Мир, 1973, 480 с.
  2. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.:Мир, 1983. 360 с.
  3. Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логике и теории алгоритмов. Москва, "Физико-математическая литература", 1995 г., 250 с.
  4. Метакидес Г., Нероуд А., Принципы логики и логического программирования. Москва, "Факториал", 1998, 288 с.
  5. Братко И. Программирование на Прологе для искусственного интеллекта. М.:Мир, 1990, 560 с.
  6. Набебин А.А. Логика и Пролог в дискретной математике. М., Изд-во МЭИ, 1997.
  7. Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: model checking. Изд-во МЦНМО, Москва, 2002, 405 с.

Дополнительная литература

  1. Мендельсон Э. Введение в математическую логику. М.:Наука, 1984. 319 с.
  2. Верещагин Н.К., Шень А. Языки и исчисления. 2004.
  3. Успенский В.А., Верещагин Н.К., Плиско В.Е. Вводный курс математической логики. 2004. 128 с.
  4. Лавров И.А. Математическая логика. Учебное пособие для вузов. М.: Академия, 2006.
  5. Колмогоров А.Н., Драгалин А.Г. Математическая логика. Серия "Классический университетский учебник". Изд.3, 2006, 240 с.
  6. Ершов Ю.Л., Палютин Е.А. Математическая логика - М.: 1979.
  7. Непейвода Н. Н. Прикладная логика. Новосибирск. 2000 г.
  8. Хоггер К., Введение в логическое программирование. М.:Мир, 1988. 348 с.
  9. Клоксин У., Меллиш К. Программирование на языке Пролог. М.:Мир, 1987. 336 с.
  10. Кларк К.Л., Маккейб Ф.Г. Микро-Пролог: введение в логическое программирование. Москва, "Радио и связь". 1987, 311 с.
  11. Стерлинг Л., Шапиро Э., Искусство программирования на языке ПРОЛОГ. Москва, "Мир", 1990, 235 с.
  12. Ковальский Р. Логика в решении проблем. М.: Наука, 1990. 277 с.
  13. Логический подход к искусственному интеллекту (от модальной логики к логике баз данных). М.:Мир, 1998. 495 с.