Программа курса и список литературы

Программа курсаЛогика предикатов первого порядка1. Синтаксис и семантика логики предикатов. Термы, формулы, интерпретация. Отношениевыполнимости формулы на интерпретации.2. Выполнимость, общезначимость, противоречивость формул логики предикатов. Примерыобщезначимых и противоречивых формул логики предикатов.

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

Равносильные формулы. Примеры равносильных формул. Теорема о равносильной замене.Метод резолюций8. Предваренная нормальная форма. Теорема о приведении формулы к предваренной нормальнойформе.9. Сколемовская стандартная форма. Теорема о приведении формулы к сколемовской стандартнойформе.10. Эрбрановский универсум, эрбрановский базис, эрбрановские интерпретации. Теорема обэрбрановской модели для сколемовской стандартной формы. Сведение проблемыобщезначимости формул к проблеме противоречивости систем дизъюнктов. Теорема Эрбрана.11. Подстановки. Применение подстановок к термам и формулам.

Композиция подстановок.Унификатор. Наиболее общий унификатор.12. Сведение задачи унификации к задаче решения системы термальных уравнений. Лемма о связке.Алгоритм унификации. Теорема о корректности и завершаемости алгоритма унификации.13. Метод резолюций для логики предикатов: правила резолюции и склейки, резолютивный вывод.Теорема корректности резолютивного вывода.14. Лемма о подъеме. Теорема полноты резолютивного вывода для логики предикатов.15.

Общая схема доказательства общезначимости формул логики предикатов методом резолюций.Стратегии резолютивного вывода.Основы логического программирования16. Использование метода резолюций для нахождения ответов на запросы. Истолкованиерезолютивного вывода как вычисления. Примеры вычислительных возможностей резолютивноговывода.17. Хорновские дизъюнкты. Синтаксис языка логического программирования: логическиепрограммы и запросы. Декларативная семантика логических программ. Правильный ответ.18.

Теорема о пересечении эрбрановских моделей логических программ. Теорема о наименьшейэрбрановской модели. Теорема об основных правильных ответах.19. SLD-резолюция. SLD-резолютивные вычисления (опровержения) логических программ.Процедурная интерпретация SLD-выводов. Примеры SLD-опровержений успешных, тупиковыхи бесконечных. Вычислимый ответ. Операционная (процедурная) семантика логическихпрограмм.20. Теорема корректности SLD-резолютивных вычислений логических программ.21. Множество успехов логической программы.

Лемма о подъеме для хорновских дизъюнктов.Теоремы полноты SLD-резолютивных вычислений логических программ.22. Правило вычислений и его роль. R-вычислимый ответ. Переключательная лемма. Теорема онезависимости правила вычислений. Теорема сильной полноты SLD-резолюции.23. Дерево SLD-вычислений логических программ. Стратегии вычислений. Полные и неполныестратегии вычислений. Стандартная стратегия исполнения логических программ. Неполнотастандартной стратегии.24. Управление исполнением логических программ.

Оператор отсечения. Операционная семантикаоператора отсечения.25. Отрицание в Прологе. Допущение замкнутости мира. Отрицание как неудача. Эффектнемонотонности вычислений логических программ с оператором отрицания.26. Встроенные предикаты и функции.

Операционная семантика встроенных средств.27. Теорема о вычислительной универсальности чистого Пролога. Теорема Чёрча о неразрешимостилогики предикатов первого порядка.Неклассические прикладные логики28. Интуиционистская логика. Модели Крипке для интуиционистской логики. Примерыинтуиционистски общезначимых и необщезначимых формул. Модальные логики. МоделиКрипке для модальных логик.

Эпистемические логики. Темпоральные логики.29. Проблема верификации последовательных программ. Операционная семантика типовыхпрограммных конструкций. Предусловие и постусловие. Частичная корректность программ.Тройки Хоара и их содержательный смысл. Правила вывода в логике Хоара для доказательствачастичной корректности последовательных программ.30. Моделирование программ системами переходов. Темпоральная логика высказываний линейноговремени (LTL): синтаксис и семантика. Применение темпоральных логик для спецификацииповедения реагирующих программных систем.31.

Задача проверки выполнимости формул 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 с..