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

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
м
м
Строка 439: Строка 439:
  
 
== Метод резолюций в логике предикатов ==
 
== Метод резолюций в логике предикатов ==
<ol start="10">
+
<ol start="9">
 
<li> Предварённая нормальная форма. Теорема о предварённой нормальной форме.
 
<li> Предварённая нормальная форма. Теорема о предварённой нормальной форме.
 
<li> Сколемовская стандартная форма. Алгоритм сколемизации предварённой нормальной формы. Теорема о сколемизации.
 
<li> Сколемовская стандартная форма. Алгоритм сколемизации предварённой нормальной формы. Теорема о сколемизации.
Строка 451: Строка 451:
 
</ol>
 
</ol>
  
== Аксиоматические теории первого порядка ==
+
== Аксиоматические теории и исчисления ==
<ol start="21">
+
<ol start="18">
 
<li> Аксиомы, теоремы и теории. Выполнимость, противоречивость и общезначимость формул в теории. Проблема общезначимости формул логики предикатов в теории.
 
<li> Аксиомы, теоремы и теории. Выполнимость, противоречивость и общезначимость формул в теории. Проблема общезначимости формул логики предикатов в теории.
 
<li> Основные свойства интерпретаций: непротиворечивость, полнота, разрешимость, адекватность интерпретациям.
 
<li> Основные свойства интерпретаций: непротиворечивость, полнота, разрешимость, адекватность интерпретациям.

Версия 09:18, 26 апреля 2019

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

Объявления

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

  • 2019.04.22 16:10 Обновлена статистика предоставленных решений бонусных задач
  • 2019.04.21 20:30 Появилось условие бонусной задачи 8
  • 2019.04.21 20:22 Появились слайды лекций 12, 13
  • 2019.02.05 14:05 Страница подготовлена к началу весеннего семестра 2018/2019 учебного года

Содержание

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

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

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

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

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

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

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

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

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

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

Лекция 9. (Захаров В.А.) Полнота резолютивного вывода.

Лекция 10. Аксиоматические теории. Основные свойства теорий (адекватность интерпретациям, непротиворечивость, разрешимость, полнота). Формальная арифметика. Арифметика Пеано. Теорема Гёделя о неполноте.

Лекция 11. Выразимость в теориях и интерпретациях. Арифметика Пресбургера (определение, разрешимость, полнота, выразительные возможности).

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

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


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

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

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

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

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

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

14, 16-17.

Семинары

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Экзамен

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

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

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

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

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

Зачёт

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

  • Две задачи, идентичные задачам 4, 5 экзамена, каждая из которых оценивается в 2 балла.
  • Пять теоретических вопросов по лекциям, проведённым после контрольной работы, аналогичные теоретическим вопросам первой контрольной работы. Каждый теоретический вопрос оценивается в 1 балл.

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

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

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

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

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

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

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

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

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

Описание задачи

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

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

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

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

Количество предоставленных решений

Группа 318: 0

Группа 241: 0

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

Описание задачи

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

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

Количество предоставленных решений

Группа 318: 1

Группа 241: 1

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

Описание задачи

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

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

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

Количество предоставленных решений

Группа 318: 1

Группа 241: 2 (все баллы розданы)

Изоморфизм и элементарная эквивалентность интерпретаций

Описание задачи

Доказать утверждение на слайде 24 лекции 10 о соотношении понятий изоморфизма и элементарной эквивалентности интерпретаций.

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

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

Количество предоставленных решений

Группа 318: 0

Группа 241: 0

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

Описание задачи

Доказать теорему Гёделя о неполноте (лекция 10): либо адаптировать доказательство в лекции к общему случаю и доказать лемму о диагонали и утверждение об арифметизуемости графика, либо предоставить независимое доказательство.

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

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

Количество предоставленных решений

Группа 318: 0

Группа 241: 1

Арифметика Пресбургера и математическая индукция

Описание задачи

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

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

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

Количество предоставленных решений

Группа 318: 0

Группа 241: 0

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

Описание задачи

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

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

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

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

Количество предоставленных решений

Группа 318: 0

Группа 241: 0

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

Описание задачи

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

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

  • первый предоставивший решение: +9 баллов
  • второй предоставивший решение: +6 баллов
  • третий предоставивший решение: +6 баллов

Количество предоставленных решений

Группа 318: 0

Группа 241: 0


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

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

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

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

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

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

Аксиоматические теории и исчисления

  1. Аксиомы, теоремы и теории. Выполнимость, противоречивость и общезначимость формул в теории. Проблема общезначимости формул логики предикатов в теории.
  2. Основные свойства интерпретаций: непротиворечивость, полнота, разрешимость, адекватность интерпретациям.
  3. Формальная арифметика. Арифметика Пеано. Теорема Гёделя о неполноте.
  4. Выразимость символов сигнатуры в интерпретациях. Теорема о расширении теории. Теорема о подстановке определения.
  5. Арифметика Пресбургера.
  6. Логические исчисления. Исчисления предикатов. Доказуемость (выводимость) формул.
  7. Исчисление высказываний гильбертовского типа. Корректность и полнота исчисления.
  8. Исчисление предикатов гильбертовского типа. Теорема Гёделя о полноте.
  9. Натуральное исчисление высказываний. Корректность и полнота исчисления.
  10. Натуральное исчисление предикатов. Корректность и полнота исчисления. Натуральный вывод формул.

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

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