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

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
м
Строка 56: Строка 56:
 
В каждом теоретическом вопросе предлагается несколько вариантов ответа.
 
В каждом теоретическом вопросе предлагается несколько вариантов ответа.
 
Среди этих ответов может быть один, ни одного или несколько правильных.
 
Среди этих ответов может быть один, ни одного или несколько правильных.
Чтобы вопрос был засчитан как правильно решённый, достаточно отметить ''все'' правильные ответы.
+
Для правильного решения теоретического вопроса следует отметить ''все'' правильные ответы и только их.
 
Обоснование того, почему выбраны или не выбраны те или иные ответы, ''не требуется''.
 
Обоснование того, почему выбраны или не выбраны те или иные ответы, ''не требуется''.
  

Версия 02:58, 27 марта 2016

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

Внимание! В весеннем семестре 2016 года планируется существенное изменение программы курса. Информация о лекциях 2015 года временно сохранена здесь.

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

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

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

Лекция 3. Логика предикатов. Синтаксис: термы и формулы. Семантика: интерпретации, отношение выполнимости. Выполнимые и общезначимые формулы. Модели. Логическое следствие. Проблема общезначимости формул.

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

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

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

Лекция 7. Задача унификации. Алгоритм унификации.

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

Лекция 9. Полнота резолютивного вывода. Стратегии резолютивного вывода. Резолютивный вывод в логическом программировании.

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

Семинары

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

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

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

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

Контрольная работа состоится 1 апреля 2016 г. по расписанию занятий: на первой паре (8:45-10:30) в аудитории 503.

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

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

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

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

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

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

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

  • набрано от 13 до 15 баллов: бонус +3 балла;
  • набрано от 10 до 12 баллов: бонус +1 балл;
  • набрано от 7 до 9 баллов: штраф -1 балл;
  • набрано 6 баллов или меньше: штраф -3 балла;
  • контрольная работа пропущена по неуважительной причине: штраф -3 балла;
  • контрольная работа пропущена по уважительной причине: бонус +0 баллов.

Бонусы и штрафы по итогам контрольной работы появятся здесь после проведения и проверки.

Экзамен

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

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

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

  • набрано 32 балла или больше: отлично;
  • набрано от 24 до 31 балла: хорошо;
  • набрано от 16 до 23 баллов: удовлетворительно;
  • набрано 15 баллов или меньше: неудовлетворительно.

Точное содержание экзаменационной работы и программа курса будут определены после окончания семестра.

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

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

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

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

Информация о лекциях 2015 года

Темы лекций 2015 года

Лекция 1. Что изучает логика? Логика в информатике. Структура курса. Исторические сведения. Логические парадоксы.

Лекция 2. Классическая логика предикатов первого порядка. Синтаксис: термы и формулы. Семантика: интерпретации, Выполнимость.

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

Лекция 4. Подстановки. Табличный вывод. Корректность табличного вывода.

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

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

Лекция 7. Эрбрановские интерпретации. Теорема Эрбрана. Задача унификации.

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

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

Лекция 10. Полнота резолютивного вывода.

Лекция 11. Стратегии резолютивного вывода. Вычислительные возможности метода резолюций.

Лекция 12. Хорновские логические программы: синтаксис, декларативная семантика, операционная семантика. SLD-резолютивные вычисления.

Лекция 13. Корректность и полнота операционной семантики хорновских логических программ.

Лекция 14. Правила выбора подцели. Деревья SLD-резолютивных вычислений. Правила поиска. Стратегии вычисления.

Лекция 15. Алгоритмическая полнота логических программ. Моделирование машин Тьюринга логическим программами. Теорема Чёрча-Тьюринга.

Лекция 16. Встроенные операторы. Управление вычислениями. Оператор отсечения. Отрицание в логическом программировании. Оператор отрицания.

Лекция 17. Интуиционистская логика.

Лекция 17. Модальные логики. Правильные программы. Императивные программы. Задача верификации программ. Логика Хоара. Автоматическая проверка правильности программ.

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

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

Программа 2015 года

Логика предикатов первого порядка

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

Метод резолюций

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

Основы логического программирования

  1. Использование метода резолюций для нахождения ответов на запросы. Истолкование резолютивного вывода как вычисления. Примеры вычислительных возможностей резолютивного вывода.
  2. Хорновские дизъюнкты. Синтаксис языка логического программирования: логические программы и запросы. Декларативная семантика логических программ. Правильный ответ.
  3. Теорема о пересечении эрбрановских моделей логических программ. Теорема о наименьшей эрбрановской модели. Теорема об основных правильных ответах.
  4. SLD-резолюция. SLD-резолютивные вычисления (опровержения) логических программ. Процедурная интерпретация SLD-выводов. Примеры SLD-опровержений успешных, тупиковых и бесконечных. Вычислимый ответ. Операционная (процедурная) семантика логических программ.
  5. Теорема корректности SLD-резолютивных вычислений логических программ.
  6. Множество успехов логической программы. Лемма о подъеме для хорновских дизъюнктов. Теоремы полноты SLD-резолютивных вычислений логических программ.
  7. Правило вычислений и его роль. R-вычислимый ответ. Переключательная лемма. Теорема о независимости правила вычислений. Теорема сильной полноты SLD-резолюции.
  8. Дерево SLD-вычислений логических программ. Стратегии вычислений. Полные и неполные стратегии вычислений. Стандартная стратегия исполнения логических программ. Неполнота стандартной стратегии.
  9. Управление исполнением логических программ. Оператор отсечения. Операционная семантика оператора отсечения.
  10. Отрицание в Прологе. Допущение замкнутости мира. Отрицание как неудача. Эффект немонотонности вычислений логических программ с оператором отрицания.
  11. Встроенные предикаты и функции. Операционная семантика встроенных средств.
  12. Теорема о вычислительной универсальности чистого Пролога. Теорема Чёрча о неразрешимости логики предикатов первого порядка.

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

  1. Интуиционистская логика. Модели Крипке для интуиционистской логики. Примеры интуиционистски общезначимых и необщезначимых формул. Модальные логики. Модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики.
  2. Проблема верификации последовательных программ. Операционная семантика типовых программных конструкций. Предусловие и постусловие. Частичная корректность программ. Тройки Хоара и их содержательный смысл. Правила вывода в логике Хоара для доказательства частичной корректности последовательных программ.
  3. Моделирование программ системами переходов. Темпоральная логика высказываний линейного времени (LTL): синтаксис и семантика. Применение темпоральных логик для спецификации поведения реагирующих программных систем.
  4. Задача проверки выполнимости формул LTL на конечной модели. Равносильные преобразования формул LTL. Табличный алгоритм проверки выполнимости формул LTL на конечной модели: основные этапы.