(C) 2001

 



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

( Оценки за экзаменационную работу 09.01.2010 )

Выставление оценок состоится 11 января в 10.00 в ауд. 790а

Лекции по курсу математической логики и логического программирования

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Лекция 17. Отрицание в логическом программировании. Оператор not. Встроенные предикаты и функции. Оператор вычисления значений. Модификация баз данных.

Лекция 18. Формальные аксиоматические теории. Исчисление предикатов с равенством. Элементарная геометрия. Теория множеств Цермело-Френкеля. Арифметика Пеано. Теорема Геделя о неполноте формальной арифметики.

Лекция 19-20. Интуиционистская логика. Модальные логики.

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

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

Лекция 23. Задача верификации моделей программ. Подформулы Фишера-Ладнера. Табличный метод верификации моделей программ. Системы Хинтикки. Алгоритм верификации моделей программ. ( Лекция 23.)

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

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

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

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

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

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

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

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

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

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

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

 

О ПОРЯДКЕ ПРОВЕДЕНИЯ ЭКЗАМЕНА ПО КУРСУ «МАТЕМАТИЧЕСКАЯ ЛОГИКА И ЛОГИЧЕСКОЕ ПРОГРАММИРОВАНИЕ»

1.     Экзамен проводится в форме письменной контрольной работы.

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

Типовой пример задачи: Слово – это конечный непустой список букв русского алфавита. Текст – это конечный непустой список слов. Два разных слова W¢ и W² называется однокоренными, если W¢=U1WV1, W¢=U2WV2, где U1, V1, U2, V2 - непустые префиксы и суффиксы слов W¢, W², а W – слово, состоящее не менее чем из трех букв. Построить логическую программу, которая для заданного текста L вычисляет все пары X,Y однокоренных слов. Запрос к программе должен иметь вид  ? G(L,X,Y).

3.     Вторая часть работы – решение задач и ответы на теоретические вопросы:

·        4 типовые задачи – построение формулы логики предикатов, соответствующей естественно-языковому утверждению, построение табличного вывода для доказательства общезначимости формулы логики предикатов, применение метода резолюций для доказательства общезначимости формулы логики предикатов и построение дерева SLD-резолютивных вычислений заданного запроса к заданной логической программе.

·        5 вопросов, требующих знания формулировки определений, алгоритмов и утверждений, рассмотренных лекционном курсе. Вопросы предусматривают проведение простейшего анализа основных понятий математической логики.

·        4 теоретические задачи, требующие умения обоснованно выбрать истинные утверждения из предложенного списка.

На выполнение контрольной работы отводится 150 мин.

Типовые задачи:

1. Используя только предикаты, перечисленные в Приложении, построить замкнутую формулу логики предикатов, адекватно выражающую следующее суждение:

«Каков бы ни был черный куб, лежащий под всеми черными шарами, слева от него не находится ни одного белого шара».

Приложение.

 

B(x) – «предмет x имеет черный цвет»;

W(x) – «предмет x имеет белый цвет»;

C(x) – «предмет x –  куб»;

S(x) – «предмет x –  шар»;

D(x,y) – «предмет x расположен под предметом y»;

U(x,y) – «предмет x расположен над предметом y»;

L(x,y) – «предмет x расположен слева от предмета y»;

R(x,y) – «предмет x расположен справа от предмета y».

 

2. Используя правила табличного вывода, доказать общезначимость следующей формулы логики предикатов:      (Ø$y P(y) Ú "x R(x)) ® "x (P(x) ® R(x))

 

3. Для заданной формулы j выяснить, применяя метод резолюций, является ли эта формула общезначимой.

($y ØP(y) ® $x R(x)) ® "x $y (P(x) Ú R(y))

 

4.  Для заданного запроса  G=? P(x), R(x)   к заданной логической программе P построить на основе стандартной стратегии вычислений (с использованием оператора отсечения) дерево SLD-резолютивных вычислений и определить множество вычислимых ответов.

 

P: P(b) ¬ ;

   P(f(b)) ¬ R(b), !;

   P(c) ¬ ;

   R(f(x)) ¬ P(x), !;

   R(x) ¬ P(x);

 

4.     Результаты экзамена будут объявлены на этой странице спустя два дня после экзамена.

 

5.     Критерии оценки контрольной работы:

Задача 0 оценивается 6 очками:

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

Каждая из типовых задач оценивается 3 очками, каждый из вопросов по определениям и утверждениям оценивается 2 очками, каждая из теоретических задач оценивается 3 очками.

Для получения оценки

«отлично» требуется набрать не менее 33 очков

«хорошо» требуется набрать не менее 26 очков

«удовлетворительно» требуется набрать не менее 18 очков.