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

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
(→‎Лекции по курсу математической логики и логического программирования)
 
(не показаны 88 промежуточные версии 2 участников)
Строка 1: Строка 1:
−
Обязательный курс для студентов III потока 7 семестра обучения.  
+
[[Категория:Лекционные курсы кафедры МК]]
 +
''Актуальность информации: осенний семестр 2024/2025 учебного года.''
  
−
Лекционная нагрузка — 48 ч., семинары — 16 ч.
+
Обязательный курс для студентов 3 потока 4 курса в 7 семестре.
 +
Лектор: [[Подымов Владислав Васильевич|Подымов В.В.]]
  
−
Курс читает профессор [[Захаров Владимир Анатольевич|В. А. Захаров]].
+
= Слайды лекций =
  
−
<!--
+
[[Media: MLLP_VP_01.pdf|Блок 1]] (вступительный). Что такое логика. Несколько логических парадоксов. Чего ожидать в лекциях.
−
== Материалы для подготовки к государственному экзамену по математике ==
+
  
−
'''[[Media: Bilet_1.pdf| Вопрос 3.]]''' '''Логика 1-го порядка.  Выполнимость и общезначимость. Общая схема метода резолюций.''' 
+
[[Media: MLLP_VP_02.pdf|Блок 2.]] Логика высказываний: синтаксис, семантика.
  
−
'''[[Media: Bilet_2.pdf| Вопрос 4.]]''' '''Логическое  программирование. Декларативная семантика и операционная семантика;  соотношение между ними.  Стандартная стратегия выполнения логических программ.'''
+
[[Media: MLLP_VP_03.pdf|Блок 3.]] Логика предикатов: синтаксис, семантика.
  
−
== '''ВНИМАНИЕ!'''==
+
[[Media: MLLP_VP_04.pdf|Блок 4.]] Как формализовать предложение на языке логики предикатов (пример).
  
−
'''[[Media: Exam-2019.pdf| Результаты экзамена 04 января 2019]]'''
+
[[Media: MLLP_VP_05.pdf|Блок 5.]] Логика высказываний: выполнимые и общезначимые формулы.
  
−
'''[[Media: Test.pdf| Тренировочный материал для подготовки к пересдаче экзамена 08 февраля 2019]]'''
+
[[Media: MLLP_VP_06.pdf|Блок 6.]] Логика предикатов: выполнимые и общезначимые формулы, модели формул, логическое следствие, проблема общезначимости формул (постановка).
  
−
+
[[Media: MLLP_VP_07.pdf|Блок 7.]] Логика предикатов: можно ли проверить общезначимость формулы "в лоб"?
  
−
'''КОНСУЛЬТАЦИЯ СОСТОИТСЯ 05 ЯНВАРЯ (ПЯТНИЦА), В АУД. П-13, в 16.00'''
+
[[Media: MLLP_VP_08.pdf|Блок 8.]] Метод семантических таблиц: семантические таблицы.
  
−
'''[[Media: Colloquium-2017.pdf| Результаты коллоквиума 2017]]'''
+
[[Media: MLLP_VP_09.pdf|Блок 9.]] Подстановки (основные определения).
  
−
== ЭКЗАМЕН ==
+
[[Media: MLLP_VP_10.pdf|Блок 10.]] Метод семантических таблиц: табличный вывод.
  
−
'''[[Media:ReExam-2018.pdf| РЕЗУЛЬТАТЫ ПЕРЕСДАЧИ ЭКЗАМЕНА (14.02.2018)]]'''
+
[[Media: MLLP_VP_11.pdf|Блок 11.]] Метод семантических таблиц: корректность табличного вывода.
  
−
'''[[Media:Exam-2016-1.pdf| РЕЗУЛЬТАТЫ ПЕРЕСДАЧИ (13.02.2017)]]'''
+
[[Media: MLLP_VP_12.pdf|Блок 12.]] Метод семантических таблиц: полнота табличного вывода.
  
−
Выставление оценок будет проводиться в 10.00, 09.01.2018 в ауд. 506
+
[[Media: MLLP_VP_13.pdf|Блок 13.]] Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Автоматизация доказательства теорем.
−
-->
+
  
 +
[[Media: MLLP_VP_14.pdf|Блок 14.]] Общая схема метода резолюций.
  
−
<!--
+
[[Media: MLLP_VP_15.pdf|Блок 15.]] Равносильность формул логики предикатов.
−
<ol>
+
−
<li> Экзамен по курсу "Математическая логика и логическое программирование" состоится 5 января в ауд. П-13; начало экзамена - 10.00; окончание экзамена - 12.30.
+
−
<li> Итоговая экзаменационная оценка складывается из оценки за экзаменационную контрольную работу и оценки за коллоквиум. [[Media:Colloquium-2016.pdf| Результаты коллоквиума (21.11.2016)]]
+
−
<li> Выставление экзаменационных оценок и ознакомление с работами будет проводиться 6 января в ауд. 506 в 15.00.
+
−
<li> Консультация к экзамену состоится 4 января в ауд. П-13 в 16.30.
+
−
<li> Типовые примеры экзаменационных контрольных работ представлены здесь: <br>
+
  
−
'''[[Media:Test-1.pdf| Пример 1]]''', <br>
+
[[Media: MLLP_VP_16.pdf|Блок 16.]] Предварённая нормальная форма (ПНФ).
  
−
'''[[Media:Test-2.pdf| Пример 2]]''', <br>
+
[[Media: MLLP_VP_17.pdf|Блок 17.]] Сколемовская стандартная форма (ССФ).
  
−
'''[[Media:Test-3.pdf| Пример 3]]''', <br>
+
[[Media: MLLP_VP_18.pdf|Блок 18.]] Системы дизъюнктов.
  
−
'''[[Media:Test-4.pdf| Пример 4]]'''.
+
[[Media: MLLP_VP_19.pdf|Блок 19.]] Композиция подстановок. Постановка задачи унификации.
−
</ol> -->
+
  
−
== Задачи по курсу математической логики и логического программирования ==
+
[[Media: MLLP_VP_20.pdf|Блок 20.]] Алгоритм унификации атомарных формул.
  
−
[[Media:MatLog_tasks.pdf| Сборник обязательных задач для семинарских занятий]]
+
[[Media: MLLP_VP_21.pdf|Блок 21.]] Монотонность и транзитивность логического следования.
  
−
[[Медиа:MatLog_exer.pdf| Расширенный сборник задач для самостоятельного решения]]
+
[[Media: MLLP_VP_22.pdf|Блок 22.]] Резолютивный вывод. Корректность резолютивного вывода.
  
−
== Лекции по курсу математической логики и логического программирования ==
+
[[Media: MLLP_VP_23.pdf|Блок 23.]] Обоснование общезначимости формулы методом резолюций (пример).
  
−
'''[[Media: People_who_made_logic.pdf| Биографии некоторых математиков, создавших математическую логику.]]'''
+
[[Media: MLLP_VP_24.pdf|Блок 24.]] Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях.
  
−
'''[[Media: LectLog_1.pdf| Лекция 1.]]''' Что изучает логика? Логика в информатике. Структура курса. Исторические сведения. Логические парадоксы. 
+
[[Media: MLLP_VP_25.pdf|Блок 25.]] Теорема Эрбрана. Полнота резолютивного вывода.
  
−
'''[[Media: LectLog2.pdf| Лекция 2.]]''' Классическая логика предикатов первого порядка. Синтаксис. Термы и формулы.Семантика. Интерпретация. Выполнимость формул.   
+
[[Media: MLLP_VP_26.pdf|Блок 26.]] Иллюстрация полноты резолютивного вывода.
  
−
'''[[Media: LectLog_3.pdf| Лекция 3.]]''' Выполнимые и общезначимые формулы. Модели. Логическое следование. Проблема общезначимости. Семантические таблицы.     
+
[[Media: MLLP_VP_27.pdf|Блок 27.]] Стратегии резолютивного вывода.
  
−
'''[[Media: LectLog4.pdf| Лекция 4.]]''' Подстановки. Табличный вывод. Корректность табличного вывода.     
+
[[Media: MLLP_VP_28.pdf|Блок 28.]] Даша, Саша, Паша, пиво и метод семантических таблиц с методом резолюций.
  
−
'''[[Media: LectLog5.pdf| Лекция 5.]]''' Полнота табличного вывода. Теорема Левенгейма-Сколема. Теорема компактности Мальцева. Автоматическое доказательство теорем.   
+
[[Media: MLLP_VP_29.pdf|Блок 29.]] Хорновские дизъюнкты.
  
−
'''[[Media: LectLog_6.pdf| Лекция 6.]]''' Общая схема метода резолюций. Равносильные формулы. Теорема о равносильной замене. Предваренная нормальная форма. Сколемовская стандартная форма. Системы дизъюнктов.   
+
[[Media: MLLP_VP_30.pdf|Блок 30.]] Вычислительные возможности метода резолюций.
  
−
'''Лекция 7.''' <!--'''[[Media: LectLog7.pdf| Лекция 7.]]'''--> Эрбрановские интерпретации. Теорема Эрбрана. Задача унификации.  
+
[[Media: MLLP_VP_31.pdf|Блок 31.]] Хорновские логические программы: синтаксис, декларативная семантика, правильные ответы.
  
−
'''Лекция 8.''' <!--'''[[Media: LectLog8.pdf| Лекция 8.]]'''--> Алгоритм унификации.  
+
[[Media: MLLP_VP_32.pdf|Блок 32.]] Хорновские логические программы: списки.
  
−
'''Лекция 9.''' <!--'''[[Media: LectLog9.pdf| Лекция 9.]]'''--> Резолютивный вывод. Корректность резолютивного вывода. Применение метода резолюций.    
+
[[Media: MLLP_VP_33.pdf|Блок 33.]] Хорновские логические программы: операционная семантика, SLD-резолютивные вычисления, SLD-вычислимые ответы.
  
−
'''Лекция 10.''' <!--'''[[Media: LectLog_10.pdf| Лекция 10.]]'''--> Полнота резолютивного вывода.    
+
[[Media: MLLP_VP_34.pdf|Блок 34.]] Хорновские логические программы: корректность операционной семантики.
  
−
'''Лекция 11.''' <!--'''[[Media: LectLog11.pdf| Лекция 11.]]'''--> Стратегии резолютивного вывода. Вычислительные возможности метода резолюций   
+
[[Media: MLLP_VP_35.pdf|Блок 35.]] Хорновские логические программы: полнота операционной семантики.
  
−
'''Лекция 12.''' <!--'''[[Media: LectLog12.pdf| Лекция 12.]]'''--> Хорновские логические программы: синтаксис. Декларативная семантика логических программ. Операционная семантика логических программ. SLD-резолютивные вычисления.    
+
[[Media: MLLP_VP_36.pdf|Блок 36.]] Хорновские логические программы: содержательное сравнение семантик.
  
−
'''Лекция 13.''' <!--'''[[Media: LectLog13.pdf| Лекция 13.]]'''--> Корректность операционной семантики. Полнота операционной семантики.  
+
[[Media: MLLP_VP_37.pdf|Блок 37.]] Хорновские логические программы: переключательная лемма, сильная полнота операционной семантики, стандартное правило выбора подцели.
  
−
'''Лекция 14.''' <!--'''[[Media: LectLog14.pdf| Лекция 14.]]'''--> Правила выбора подцелей. Деревья вычислений логических программ. Стратегии вычисления логических программ.   
+
[[Media: MLLP_VP_38.pdf|Блок 38.]] Хорновские логические программы: деревья SLD-резолютивных вычислений, стратегии вычисления и их полнота, стандартная стратегия вычисления.
−
+
−
'''Лекция 15.''' <!--'''[[Media: LectLog15.pdf| Лекция 15.]]'''--> Алгоритмическая полнота логических программ. Моделирование машин Тьюринга логическим программами. Теорема Черча.      
+
  
−
'''Лекция 16.''' <!--'''[[Media: LectLog16.pdf| Лекция 16.]]'''--> Управление вычислениями логических программ. Оператор отсечения.      
+
[[Media: MLLP_VP_39.pdf|Блок 39.]] Машины Тьюринга.
  
−
'''Лекция 17.''' <!--'''[[Media: LectLog17.pdf| Лекция 17.]]'''--> Отрицание в логическом программировании. Оператор not. Встроенные предикаты и функции. Оператор вычисления значений. Модификация баз данных.    
+
[[Media: MLLP_VP_40.pdf|Блок 40.]] Моделирование машин Тьюринга хорновскими логическими программами.
  
−
'''Лекция 18.''' <!--'''[[Media: LectLog18.pdf| Лекция 18.]]'''--> Интуиционистская логика.  
+
[[Media: MLLP_VP_41.pdf|Блок 41.]] Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.
  
−
'''Лекция 19.''' <!--'''[[Media: LectLog18.pdf| Лекция 19.]]'''--> Модальные логики.        
+
[[Media: MLLP_VP_42.pdf|Блок 42.]] Теорема Чёрча.
  
−
'''Лекция 20.''' <!--'''[[Media: LectLog20.pdf| Лекция 20.]]'''--> Правильные программы. Императивные программы. Задача верификации программ. Логика Хоара. Автоматическая проверка правильности программ.   
+
[[Media: MLLP_VP_43.pdf|Блок 43.]] Логические программы: встроенные предикаты и функции.
  
−
'''Лекция 21.''' <!--'''[[Media: LectLog21.pdf| Лекция 21.]]'''--> Верификация распределенных программ. Логика линейного времени PLTL.        Размеченные системы переходов. Задача верификации моделей программ.  
+
[[Media: MLLP_VP_44.pdf|Блок 44.]] Логические программы: стековые вычисления.
  
−
'''Лекция 22.''' <!--'''[[Media: LectLog22-2.pdf| Лекция 22.]]'''--> Задача верификации моделей программ. Подформулы Фишера-Ладнера. Табличный метод верификации моделей программ. Системы Хинтикки. Алгоритм верификации моделей программ.
+
[[Media: MLLP_VP_45.pdf|Блок 45.]] Логические программы: управление вычислениями, оператор отсечения.
  
−
'''Лекция 23-24.''' <!--'''[[Media: LectLog25.pdf| Лекции 23-24.]]'''--> Как устроена математика. Исчисление предикатов первого порядка. Аксиоматические теории. Элементарная геометрия. Теория множеств Цермело-Френкеля. Арифметика Пеано. Теорема Геделя о неполноте формальной арифметики.
+
[[Media: MLLP_VP_46.pdf|Блок 46.]] Отрицание в логическом программировании. Допущение замкнутости мира.
  
−
== Программа курса == 
+
[[Media: MLLP_VP_47.pdf|Блок 47.]] Логические программы: оператор отрицания, SLDNF-резолюция.
  
−
=== Логика предикатов первого порядка ===
+
[[Media: MLLP_VP_48.pdf|Блок 48.]] Модальные логики.
−
<ol>
+
−
<li> Синтаксис и семантика логики предикатов. Термы, формулы, интерпретация. Отношение        выполнимости формулы на интерпретации.
+
−
<li> Выполнимость,        общезначимость, противоречивость формул логики предикатов. Примеры        общезначимых и противоречивых формул логики предикатов. Модель. Логическое следствие. Теорема о логическом следствии.
+
−
<li> Проблемы        выполнимости и общезначимости. Пример формулы, не имеющей конечных        моделей.
+
−
<li> Семантические        таблицы в логике предикатов. Табличный вывод. Теорема корректности        табличного вывода.
+
−
<li> Теорема полноты        табличного вывода.
+
−
<li> Теорема        Лёвенгейма-Сколема. Теорема компактности Мальцева.
+
−
<li> Равносильные        формулы. Примеры равносильных формул. Теорема о равносильной замене.
+
−
</ol>
+
−
=== Метод резолюций ===
+
−
<ol start="8">
+
−
<li> Предваренная        нормальная форма. Теорема о приведении формулы к предваренной нормальной        форме.
+
−
<li> Сколемовская        стандартная форма. Теорема о приведении формулы к сколемовской        стандартной форме.
+
−
<li> Эрбрановский        универсум, эрбрановский базис, эрбрановские интерпретации. Теорема об        эрбрановской модели для сколемовской стандартной формы. Сведение        проблемы общезначимости формул к проблеме противоречивости систем        дизъюнктов. Теорема Эрбрана.
+
−
<li> Подстановки.        Применение подстановок к термам и формулам. Композиция подстановок.        Унификатор. Наиболее общий унификатор.
+
−
<li> Сведение задачи        унификации к задаче решения системы термальных уравнений. Лемма о        связке. Алгоритм унификации. Теорема о корректности и завершаемости        алгоритма унификации.
+
−
<li> Метод резолюций для        логики предикатов: правила резолюции и склейки, резолютивный вывод.        Теорема корректности резолютивного вывода.
+
−
<li> Лемма о подъеме.        Теорема полноты резолютивного вывода для логики предикатов.
+
−
<li> Общая схема        доказательства общезначимости формул логики предикатов методом        резолюций. Стратегии резолютивного вывода.
+
−
</ol>
+
−
=== Основы логического программирования ===
+
−
<ol start="16">
+
−
<li> Использование        метода резолюций для нахождения ответов на запросы. Истолкование        резолютивного вывода как вычисления. Примеры вычислительных возможностей        резолютивного вывода.
+
−
<li> Хорновские        дизъюнкты. Синтаксис языка логического программирования: логические        программы и запросы. Декларативная семантика логических программ.        Правильный ответ.
+
−
<li> SLD-резолюция.        SLD-резолютивные вычисления (опровержения) логических программ.        Процедурная интерпретация SLD-выводов. Примеры SLD-опровержений        успешных, тупиковых и бесконечных. Вычислимый ответ. Операционная        (процедурная) семантика логических программ.
+
−
<li>  Теорема корректности SLD-резолютивных вычислений        логических программ.
+
−
<li>  Теорема полноты SLD-резолютивных        вычислений логических программ.
+
−
<li> Правило вычислений        и его роль. R-вычислимый ответ. Переключательная лемма. Теорема о        независимости правила вычислений. Теорема сильной полноты SLD-резолюции.
+
−
<li> Дерево        SLD-вычислений логических программ. Стратегии вычислений. Полные и неполные стратегии вычислений. Стандартная        стратегия исполнения логических программ. Неполнота стандартной        стратегии.
+
−
<li> Управление        исполнением логических программ. Оператор отсечения. Операционная        семантика оператора отсечения.
+
−
<li> Отрицание в        Прологе. Допущение замкнутости мира. Отрицание как неудача. Эффект        немонотонности вычислений логических программ с оператором отрицания.
+
−
<li> Встроенные        предикаты и функции. Операционная семантика встроенных средств.
+
−
<li> Теорема о        вычислительной универсальности чистого Пролога. Теорема Чёрча о        неразрешимости логики предикатов первого порядка.
+
−
</ol>
+
  
−
=== Неклассические прикладные логики ===
+
[[Media: MLLP_VP_49.pdf|Блок 49.]] Эпистемические логики.
−
<ol start="28">
+
−
<li> Интуиционистская логика. Модели Крипке для интуиционистской логики.       Примеры интуиционистски общезначимых и необщезначимых формул. Модальные логики. Модели Крипке для модальных логик.        Эпистемические логики. Темпоральные логики.
+
−
<li> Проблема верификации последовательных программ.        Операционная семантика типовых программных конструкций. Предусловие и постусловие. Частичная корректность программ.        Тройки Хоара и их содержательный смысл. Правила вывода в логике Хоара для доказательства частичной корректности        последовательных программ.
+
−
<li> Моделирование программ системами переходов. Темпоральная логика        высказываний линейного времени (PLTL): синтаксис и семантика. Применение темпоральных логик для спецификации поведения        реагирующих программных систем.
+
−
<li> Задача проверки выполнимости формул PLTL на конечной модели. Равносильные преобразования формул PLTL. Табличный алгоритм проверки выполнимости формул PLTL на конечной модели: основные этапы.
+
−
</ol>
+
  
−
=== Основания математики ===
+
[[Media: MLLP_VP_50.pdf|Блок 50.]] Темпоральные логики.
  
−
<ol start="32">
+
[[Media: MLLP_VP_51.pdf|Блок 51.]] Интуиционистская логика.
−
<li> Как устроена математика. Исчисление предикатов первого порядка. Аксиоматические теории. Элементарная геометрия. Теория множеств Цермело-Френкеля. Арифметика Пеано. Теорема Геделя о неполноте формальной арифметики.
+
−
</ol>
+
  
−
== Основная литература ==
+
[[Media: MLLP_VP_52.pdf|Блок 52.]] Формальная верификация.
−
# Клини С. Математическая логика. М.:Мир, 1973, 480 с.
+
−
# Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.:Мир, 1983. 360 с.
+
−
# Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логике и теории алгоритмов. Москва, "Физико-математическая литература", 1995 г., 250 с.
+
−
# Метакидес Г., Нероуд А., Принципы логики и логического программирования. Москва, "Факториал", 1998, 288 с.
+
−
# Братко И. Программирование на Прологе для искусственного интеллекта. М.:Мир, 1990, 560 с.
+
−
# Набебин А.А. Логика и Пролог в дискретной математике. М., Изд-во МЭИ, 1997.
+
−
# Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: model checking. Изд-во МЦНМО, Москва, 2002, 405 с.
+
  
−
== Дополнительная литература ==
+
[[Media: MLLP_VP_53.pdf|Блок 53.]] Модельные императивные программы. Постановка задачи верификации программ.
  
−
# Мендельсон Э. Введение в математическую логику. М.:Наука, 1984. 319 с.
+
[[Media: MLLP_VP_54.pdf|Блок 54.]] Логика Хоара. Автоматизация проверки правильности программ.
−
# Верещагин Н.К., Шень А. Языки и исчисления. 2004.
+
−
# Успенский В.А., Верещагин Н.К., Плиско В.Е. Вводный курс математической логики. 2004. 128 с.
+
−
# Лавров И.А. Математическая логика. Учебное пособие для вузов. М.: Академия, 2006.
+
−
# Колмогоров А.Н., Драгалин А.Г. Математическая логика. Серия "Классический университетский учебник". Изд.3, 2006, 240 с.
+
−
# Ершов Ю.Л., Палютин Е.А. Математическая логика - М.: 1979.
+
−
# Непейвода Н. Н. Прикладная логика. Новосибирск. 2000 г.
+
−
# Хоггер К., Введение в логическое программирование. М.:Мир, 1988. 348 с.
+
−
# Клоксин У., Меллиш К. Программирование на языке Пролог. М.:Мир, 1987. 336 с.
+
−
# Кларк К.Л., Маккейб Ф.Г. Микро-Пролог: введение в логическое программирование. Москва, "Радио и связь". 1987, 311 с.
+
−
# Стерлинг Л., Шапиро Э., Искусство программирования на языке ПРОЛОГ. Москва, "Мир", 1990, 235 с.
+
−
# Ковальский Р. Логика в решении проблем. М.: Наука, 1990. 277 с.
+
−
# Логический подход к искусственному интеллекту (от модальной логики к логике баз данных). М.:Мир, 1998. 495 с.
+
  
−
== Коллоквиум ==
+
[[Media: MLLP_VP_55.pdf|Блок 55.]] Проверка правильности распределённых систем. Пара слов о методе проверки моделей.
  
−
Коллоквиум по курсу математической логики и логического программирования проводится по материалам лекций и семинарских занятий, охватывающих вопросы 1-15.
+
''Материалы будут обновляться по мере чтения лекций.''
  
−
Коллоквиум проводится в письменной форме. На выполнение всех заданий коллквиума отводится 90 мин.
+
== Прошлогодние ==
  
−
Задание коллоквиума состоит из 3 практических задач
+
[[Media: MLLP_VP_56.pdf|Блок 56.]] Размеченные системы переходов.
  
−
- построение формулы логики предикатов, адекватно выражающей утверждение естественного языка;
+
[[Media: MLLP_VP_57.pdf|Блок 57.]] Спецификация систем при помощи темпоральных логик.
  
−
- проверка общезначимости формулы логики предикатов при помощи табличного вывода;
+
[[Media: MLLP_VP_58.pdf|Блок 58.]] Алгоритм model checking для CTL.
  
−
- проверка общезначимости формулы логики предикатов при помощи метода резолюций;
+
[[Media: MLLP_VP_all.pdf|Все слайды лекций в одном файле.]]
  
−
и 9 теоретических вопросов.
+
= Сборники задач для семинаров =
  
−
В каждом теоретическом вопросе предлагается несколько вариантов ответа. Для решения задачи достаточно отметить (обвести кружком номер выбранного варианта) ВСЕ правильные варианты ответа. Возможно, что для некоторых вопросов не будет предложено ни одного правильного варианта ответа. В этом случае, естественно, ни один вариант ответа не должен быть отмечен.  
+
[[Media: MatLog_tasks.pdf| Сборник обязательных задач для семинарских занятий.]]
  
−
Максимальная оценка за решение практической задачи - 2 очка. Максимальная оценка за решение теоретической задачи - 1 очко.
+
[[Медиа: MatLog_exer.pdf| Расширенный сборник задач для самостоятельного решения.]]
  
−
Оценка "отлично" получают работы с количеством очков 13-15. Авторы этих работ получают бонус 3 балла, который добавляется к числу баллов, полученных за экзаменационную работу.
+
= Коллоквиум =
  
−
Оценка "хорошо" получают работы с количеством очков 10-12. Авторы этих работ получают бонус 1 балл, который добавляется к числу баллов, полученных за экзаменационную работу.
+
Коллоквиум проводится по материалам лекций и семинарских занятий, охватывающих вопросы 1-21 [[#Программа| программы курса]], письменно на одном из лекционных занятий, длительность - одна пара (90 минут).
  
−
Оценка "удовлетворительно" получают работы с количеством очков 7-9. Авторы этих работ получают штраф 1 балл, который вычитается из числа баллов, полученных за экзаменационную работу.
+
Вариант коллоквиума содержит 12 задач:
 +
* 3 типовые задачи:
 +
*# Формализовать в логике предикатов с заданной сигнатурой заданное предложение, записанное на естественном языке.
 +
*# Обосновать общезначимость заданной формулы логики предикатов методом семантических таблиц.
 +
*# Обосновать общезначимость заданной формулы логики предикатов методом резолюций.
 +
* 9 теоретических задач в форме теста с множественным выбором. Среди предложенных вариантов ответа требуется выбрать и отметить правильные - один, ни одного или несколько, в том числе, быть может, все. Обосновывать выбор не требуется.
  
−
Оценка "неудовлетворительно" получают работы с количеством очков менее 7, а также все те слушатели курса, которые не приняли участие в коллоквиуме без уважительных причин. Неудовлетворительная оценка дает штраф 3 балла, которые вычитаются из числа баллов, полученных за экзаменационную работу.
+
Оценка решений типовых задач:
 +
* Правильное решение - 4 балла.
 +
* Решение в целом верно, но содержит редкие ошибки серьёзнее опечаток - 3 балла.
 +
* Решение содержит серьёзные ошибки, но имеет структуру, в целом разумно соотносящуюся с правильной - 2 балла.
 +
* В решении обнаружены правильные элементы в заметном, но всё же малом количестве - 1 балл.
 +
* Даже этого в решении нет - 0 баллов.
  
−
== Экзамен ==
+
Теоретический вопрос в зависимости от количества и качества правильно обведённых и правильно необведённых ответов оценивается в 0, 1 или 2 балла.
  
−
Экзамен проводится в форме письменной контрольной работы, состоящей из 14 заданий. На выполнение работы отводится 150 минут.
+
Наибольший возможный балл за решение варианта коллоквиума - 30.
  
−
Задание 0. Разработать логическую программу решения некоторой комбинаторной задачи.
+
Техническими баллами, набранными за коллоквиум, определяется добавка (бонус или штраф) к техническим баллам за экзаменационную работу:
−
Максимальная оценка за решение задачи - 6 баллов.
+
  
−
Задания 1-4. Решить стандартные задачи курса: построить логическую формулу логики предикатов, адекватно выражающей заданное утверждение естественного языка, проверить общезначимость заданных формул логики предикатов при помощи табличного вывода и при помощи метода резолюций, построить дерево SLD-резолютивного вывода для заданной логической программы. Максимальная оценка за решение каждой задачи этого типа - 3 балла.
+
{| class="wikitable" style="margin:auto"
 +
|-
 +
! Баллов за коллоквиум
 +
! Бонус/штраф на экзамене
 +
|-
 +
| 28-30
 +
| <span style="background:#DDFFDD">+4 балла</span>
 +
|-
 +
| 25-27
 +
| <span style="background:#DDFFDD">+3 балла</span>
 +
|-
 +
| 22-24
 +
| <span style="background:#DDFFDD">+2 балла</span>
 +
|-
 +
| 19-21
 +
| <span style="background:#DDFFDD">+1 балл</span>
 +
|-
 +
| 16-18
 +
| <span style="background:#DDDDDD">+0 баллов</span>
 +
|-
 +
| 13-15
 +
| <span style="background:#FFDDDD">-1 балл</span>;
 +
|-
 +
| 10-12
 +
| <span style="background:#FFDDDD">-2 балла</span>;
 +
|-
 +
| 7-9
 +
| <span style="background:#FFDDDD">-3 балла</span>;
 +
|-
 +
| 0-6
 +
| <span style="background:#FFDDDD">-4 балла</span>;
 +
|-
 +
| Неявка без уважительной причины
 +
| <span style="background:#FFDDDD">-4 балла</span>
 +
|-
 +
| Неявка по уважительной причине
 +
| <span style="background:#DDDDDD">+0 баллов</span>
 +
|}
  
−
Задания 5-9. Привести формулировку одной из теорем или определение одного из понятий, изученных в лекционном курсе, а также дать краткий ответ (вида "да"-"нет") на дополнительный вопрос, относящийся к этой формулировке. Максимальная оценка за решение каждой задачи этого типа - 2 балла.
+
= Экзамен =
  
−
Задания 10-13. Представить набросок (эскиз) доказательства одной из теорем курса или выбрать  правильные варианты ответа на заданный вопрос и обосновать выбор. Максимальная оценка за решение каждой задачи этого типа - 3 балла.
+
Экзамен проводится письменно, длительность - 150 минут.
 +
Вариант экзамена содержит 12 задач:
 +
* Задача 1 (''8 баллов'') - написать логическую программу с заданным поведением.
 +
* Задачи 2-5 (''4 балла''):
 +
*# Формализовать в логике предикатов предложение, записанное на естественном языке.
 +
*# Обосновать общезначимость формулы логики предикатов методом семантических таблиц.
 +
*# Обосновать общезначимость формулы логики предикатов методом резолюций.
 +
*# Построить дерево SLD-резолютивных вычислений заданной логической программы.
 +
* Каждая из задач 6-8 (''3 балла'') состоит из трёх частей:
 +
*# Сформулировать утверждение, определение и т.п.
 +
*# Ответить на вопрос "на понимание", так или иначе связанный с формулировкой.
 +
*# Аргументировать (обосновать) ответ на вопрос.
 +
* Каждая из задач 9-12 (''4 балла'') устроена так:
 +
** Из нескольких предложенных вариантов ответа выбрать правильные (один, несколько или ни одного) и обосновать выбранные ответы.
 +
** Невыбранные ответы обосновывать не нужно.
  
−
Экзаменационная оценка выставляется на основе суммарного количества баллов, полученных за решение задач экзаменационной контрольной работы, и количества бонусных (штрафных) баллов, полученных за решение задач коллоквиума.
+
Наибольший возможный балл за решение варианта экзамена - 49.
 +
Баллы, полученные за решение варианта экзамена, складываются с бонусом/штрафом за коллоквиум и бонусами за другие достижения, если вдруг они есть.
 +
По полученной сумме определяется оценка:
  
−
Оценка '''отлично''': не менее 32 баллов.
+
{| class="wikitable" style="margin:auto"
 +
|-
 +
! Сумма
 +
! Оценка
 +
|-
 +
| Хотя бы 40
 +
| Отлично
 +
|-
 +
| 30-39
 +
| Хорошо
 +
|-
 +
| 20-29
 +
| Удовлетворительно
 +
|-
 +
| Менее 20
 +
| Неудовлетворительно
 +
|}
  
−
Оценка '''хорошо''': не менее 24 и не более 31 баллов.
+
= Программа =
  
−
Оценка '''удовлетворительно''': не менее 16 и не более 23 баллов.
+
''Программа может уточняться по мере проведения занятий.''
  
−
Оценка '''неудовлетворительно''': не более 15 баллов.
+
== Классические логики ==
 +
<ol>
 +
<li> Логика высказываний: синтаксис, семантика; выполнимость и общезначимость формул. Проблема общезначимости формул логики высказываний.
 +
<li> Метод семантических таблиц в логике высказываний: семантическая таблица, табличный вывод, теорема о табличном выводе.
 +
<li> Логика предикатов: синтаксис (термы, формулы, свободные и связанные переменные), семантика (интерпретации, отношение выполнимости).
 +
<li> Выполнимость и общезначимость формул логики предикатов. Модели. Логическое следование. Теорема о логическом следствии. Проблема общезначимости формул логики предикатов.
 +
<li> Пример выполнимой формулы логики предикатов, не имеющей конечных моделей.
 +
<li> Подстановки и их применение к термам и формулам логики предикатов.
 +
<li> Метод семантических таблиц в логике предикатов: семантическая таблица, табличный вывод, теорема о табличной проверке общезначимости, теоремы о корректности и полноте табличного вывода.
 +
<li> Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева.
 +
<li> Равносильные формулы. Теорема о равносильной замене.
 +
</ol>
  
 +
== Метод резолюций в логике предикатов ==
 +
<ol start="10">
 +
<li> Предварённая нормальная форма. Теорема о предварённой нормальной форме.
 +
<li> Сколемовская стандартная форма. Алгоритм сколемизации предварённой нормальной формы. Теорема о сколемизации.
 +
<li> Дизъюнкты. Сведение проблемы общезначимости формул к проблеме невыполнимости систем дизъюнктов.
 +
<li> Композиция подстановок. Унификатор. Наиболее общий унификатор. Задача унификации выражений логики предикатов.
 +
<li> Лемма о связке. Алгоритм унификации. Теорема об унификации.
 +
<li> Правило резолюции. Правило склейки. Резолютивный вывод. Теорема о корректности резолютивного вывода.
 +
<li> Эрбрановский универсум. Эрбрановский базис. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях. Теорема Эрбрана.
 +
<li> Лемма об основных дизъюнктах. Лемма о подъёме. Теорема о полноте резолютивного вывода.
 +
<li> Метод резолюций: общая схема, применение.
 +
<li> Стратегии резолютивного вывода. Семантическая резолюция. Входной вывод.
 +
<li> Хорновские дизъюнкты.
 +
<li> Резолютивный вывод как средство вычисления ответов на запросы.
 +
</ol>
  
 +
== Основы логического программирования ==
 +
<ol start="22">
 +
<li> Синтаксис хорновских логических программ: факты, правила, утверждения, программы, подцели, запросы.
 +
<li> Декларативная семантика хорновских логических программ, правильный ответ на запрос.
 +
<li> SLD-резолюция. SLD-резолютивное вычисление хорновской логической программы. Успешные, тупиковые и бесконечные вычисления программ. Операционная семантика программ, вычислимый ответ на запрос.
 +
<li> Корректность и полнота операционной семантики хорновских логических программ относительно декларативной.
 +
<li> Правило выбора подцели. Переключательная лемма, теорема о сильной полноте SLD-резолюции.
 +
<li> Дерево SLD-резолютивных вычислений. Стратегия вычисления хорновских логических программ, примеры полных и неполных стратегий. Стандартная стратегия вычисления.
 +
<li> Встроенные функции и предикаты в логических программах, их операционная семантика.
 +
<li> Управление вычислениями логических программ. Оператор отсечения, его операционная семантика.
 +
<li> Отрицание в логических программах. Гипотеза замкнутости мира. Оператор отрицания, его операционная семантика.
 +
<li> Машины Тьюринга, моделирование их логическими программами. Теорема Чёрча.
 +
</ol>
  
−
[[Категория:Лекционные курсы кафедры МК]]
+
== Неклассические прикладные логики ==
 +
<ol start="32">
 +
<li> Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики. Логика линейного времени. Логика деревьев вычислений.
 +
<li> Интуиционистская логика. Модели Крипке для интуиционистской логики.
 +
<li> Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Полная и частичная корректность программ. Тройки Хоара. Логика Хоара. Корректность вывода в логике Хоара. Слабейшее предусловие. Инвариант цикла.
 +
<li> Размеченные системы переходов. Моделирование программ системами переходов. Логика деревьев вычислений (CTL): синтаксис, семантика, основные равносильности, применение для спецификации поведения распределённых систем. Задача проверки моделей (model checking) относительно CTL: формулировка, решающий алгоритм.
 +
</ol>
 +
 
 +
= Литература =
 +
 
 +
== Основная ==
 +
# Клини С. Математическая логика. М.:Мир, 1973, 480 с.
 +
# Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.:Мир, 1983. 360 с.
 +
# Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логике и теории алгоритмов. Москва, "Физико-математическая литература", 1995 г., 250 с.
 +
# Метакидес Г., Нероуд А., Принципы логики и логического программирования. Москва, "Факториал", 1998, 288 с.
 +
# Братко И. Программирование на Прологе для искусственного интеллекта. М.:Мир, 1990, 560 с.
 +
# Набебин А.А. Логика и Пролог в дискретной математике. М., Изд-во МЭИ, 1997.
 +
# Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: model checking. Изд-во МЦНМО, Москва, 2002, 405 с.
 +
 
 +
== Дополнительная ==
 +
# Мендельсон Э. Введение в математическую логику. М.:Наука, 1984. 319 с.
 +
# Верещагин Н.К., Шень А. Языки и исчисления. 2004.
 +
# Успенский В.А., Верещагин Н.К., Плиско В.Е. Вводный курс математической логики. 2004. 128 с.
 +
# Лавров И.А. Математическая логика. Учебное пособие для вузов. М.: Академия, 2006.
 +
# Колмогоров А.Н., Драгалин А.Г. Математическая логика. Серия "Классический университетский учебник". Изд.3, 2006, 240 с.
 +
# Ершов Ю.Л., Палютин Е.А. Математическая логика - М.: 1979.
 +
# Непейвода Н. Н. Прикладная логика. Новосибирск. 2000 г.
 +
# Хоггер К., Введение в логическое программирование. М.:Мир, 1988. 348 с.
 +
# Клоксин У., Меллиш К. Программирование на языке Пролог. М.:Мир, 1987. 336 с.
 +
# Кларк К.Л., Маккейб Ф.Г. Микро-Пролог: введение в логическое программирование. Москва, "Радио и связь". 1987, 311 с.
 +
# Стерлинг Л., Шапиро Э., Искусство программирования на языке ПРОЛОГ. Москва, "Мир", 1990, 235 с.
 +
# Ковальский Р. Логика в решении проблем. М.: Наука, 1990. 277 с.
 +
# Логический подход к искусственному интеллекту (от модальной логики к логике баз данных). М.:Мир, 1998. 495 с.
 +
 
 +
= Материалы для подготовки к государственному экзамену =
 +
 
 +
''Материалы составлены для выпуска 2024.''
 +
 
 +
[[Media: MLLP_VP_gos3.pdf|Вопрос 3.]] Логика 1-го порядка. Выполнимость и общезначимость. Общая схема метода резолюций.
 +
 
 +
[[Media: MLLP_VP_gos4.pdf|Вопрос 4.]] Логическое программирование. Декаларативная семантика и операционная семантика, соотношение между ними. Стандартная стратегия выполнения логических программ.

Текущая версия на 20:25, 24 ноября 2024

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

Обязательный курс для студентов 3 потока 4 курса в 7 семестре. Лектор: Подымов В.В.

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

Блок 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. Хорновские логические программы: операционная семантика, SLD-резолютивные вычисления, SLD-вычислимые ответы.

Блок 34. Хорновские логические программы: корректность операционной семантики.

Блок 35. Хорновские логические программы: полнота операционной семантики.

Блок 36. Хорновские логические программы: содержательное сравнение семантик.

Блок 37. Хорновские логические программы: переключательная лемма, сильная полнота операционной семантики, стандартное правило выбора подцели.

Блок 38. Хорновские логические программы: деревья SLD-резолютивных вычислений, стратегии вычисления и их полнота, стандартная стратегия вычисления.

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

Блок 40. Моделирование машин Тьюринга хорновскими логическими программами.

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

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

Блок 43. Логические программы: встроенные предикаты и функции.

Блок 44. Логические программы: стековые вычисления.

Блок 45. Логические программы: управление вычислениями, оператор отсечения.

Блок 46. Отрицание в логическом программировании. Допущение замкнутости мира.

Блок 47. Логические программы: оператор отрицания, SLDNF-резолюция.

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

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

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

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

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

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

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

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

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

Прошлогодние

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

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

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

Все слайды лекций в одном файле.

Сборники задач для семинаров

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

Расширенный сборник задач для самостоятельного решения.

Коллоквиум

Коллоквиум проводится по материалам лекций и семинарских занятий, охватывающих вопросы 1-21 программы курса, письменно на одном из лекционных занятий, длительность - одна пара (90 минут).

Вариант коллоквиума содержит 12 задач:

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

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

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

Теоретический вопрос в зависимости от количества и качества правильно обведённых и правильно необведённых ответов оценивается в 0, 1 или 2 балла.

Наибольший возможный балл за решение варианта коллоквиума - 30.

Техническими баллами, набранными за коллоквиум, определяется добавка (бонус или штраф) к техническим баллам за экзаменационную работу:

Баллов за коллоквиум Бонус/штраф на экзамене
28-30 +4 балла
25-27 +3 балла
22-24 +2 балла
19-21 +1 балл
16-18 +0 баллов
13-15 -1 балл;
10-12 -2 балла;
7-9 -3 балла;
0-6 -4 балла;
Неявка без уважительной причины -4 балла
Неявка по уважительной причине +0 баллов

Экзамен

Экзамен проводится письменно, длительность - 150 минут. Вариант экзамена содержит 12 задач:

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

Наибольший возможный балл за решение варианта экзамена - 49. Баллы, полученные за решение варианта экзамена, складываются с бонусом/штрафом за коллоквиум и бонусами за другие достижения, если вдруг они есть. По полученной сумме определяется оценка:

Сумма Оценка
Хотя бы 40 Отлично
30-39 Хорошо
20-29 Удовлетворительно
Менее 20 Неудовлетворительно

Программа

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

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

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

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

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

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

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

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

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

Материалы для подготовки к государственному экзамену

Материалы составлены для выпуска 2024.

Вопрос 3. Логика 1-го порядка. Выполнимость и общезначимость. Общая схема метода резолюций.

Вопрос 4. Логическое программирование. Декаларативная семантика и операционная семантика, соотношение между ними. Стандартная стратегия выполнения логических программ.

Источник — «https://mk.cs.msu.ru/index.php?title=Математическая_логика_и_логическое_программирование_(3-й_поток)&oldid=11590»