Модели вычислений — различия между версиями
Материал из Кафедра математической кибернетики
Root (обсуждение | вклад) (Новая страница: «Лектор - профессор Захаров Владимир Анатольевич. Категория:Лекционные курсы кафедры…») |
|||
Строка 2: | Строка 2: | ||
[[Категория:Лекционные курсы кафедры МК]] | [[Категория:Лекционные курсы кафедры МК]] | ||
+ | |||
+ | == Программа курса == | ||
+ | |||
+ | === Логика предикатов первого порядка === | ||
+ | <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> Теорема о пересечении эрбрановских моделей логических программ. Теорема о наименьшей эрбрановской модели. Теорема об основных правильных ответах. | ||
+ | <li> SLD-резолюция. SLD-резолютивные вычисления (опровержения) логических программ. Процедурная интерпретация SLD-выводов. Примеры SLD-опровержений успешных, тупиковых и бесконечных. Вычислимый ответ. Операционная (процедурная) семантика логических программ. | ||
+ | <li> Теорема корректности SLD-резолютивных вычислений логических программ. | ||
+ | <li> Теорема полноты SLD-резолютивных вычислений логических программ. | ||
+ | <li> Правило вычислений и его роль. R-вычислимый ответ. Переключательная лемма. Теорема о независимости правила вычислений. Теорема сильной полноты SLD-резолюции. | ||
+ | <li> Дерево SLD-вычислений логических программ. Стратегии вычислений. Полные и неполные стратегии вычислений. Стандартная стратегия исполнения логических программ. Неполнота стандартной стратегии. | ||
+ | <li> Управление исполнением логических программ. Оператор отсечения. Операционная семантика оператора отсечения. | ||
+ | <li> Отрицание в Прологе. Допущение замкнутости мира. Отрицание как неудача. Эффект немонотонности вычислений логических программ с оператором отрицания. | ||
+ | <li> Встроенные предикаты и функции. Операционная семантика встроенных средств. | ||
+ | <li> Теорема о вычислительной универсальности чистого Пролога. Теорема Чёрча о неразрешимости логики предикатов первого порядка. | ||
+ | </ol> | ||
+ | |||
+ | === Неклассические прикладные логики === | ||
+ | <ol start="28"> | ||
+ | <li> Интуиционистская логика. Модели Крипке для интуиционистской логики. Примеры интуиционистски общезначимых и необщезначимых формул. Модальные логики. Модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики. | ||
+ | <li> Проблема верификации последовательных программ. Операционная семантика типовых программных конструкций. Предусловие и постусловие. Частичная корректность программ. Тройки Хоара и их содержательный смысл. Правила вывода в логике Хоара для доказательства частичной корректности последовательных программ. | ||
+ | <li> Моделирование программ системами переходов. Темпоральная логика высказываний линейного времени (LTL): синтаксис и семантика. Применение темпоральных логик для спецификации поведения реагирующих программных систем. | ||
+ | <li> Задача проверки выполнимости формул LTL на конечной модели. Равносильные преобразования формул LTL. Табличный алгоритм проверки выполнимости формул LTL на конечной модели: основные этапы. | ||
+ | </ol> | ||
+ | |||
+ | === Основания математики === | ||
+ | |||
+ | <ol start="32"> | ||
+ | <li> Как устроена математика. Исчисление предикатов первого порядка. Аксиоматические теории. Элементарная геометрия. Теория множеств Цермело-Френкеля. Арифметика Пеано. Теорема Геделя о неполноте формальной арифметики. | ||
+ | </ol> |
Версия 17:00, 28 декабря 2014
Лектор - профессор Захаров Владимир Анатольевич.
Содержание
Программа курса
Логика предикатов первого порядка
- Синтаксис и семантика логики предикатов. Термы, формулы, интерпретация. Отношение выполнимости формулы на интерпретации.
- Выполнимость, общезначимость, противоречивость формул логики предикатов. Примеры общезначимых и противоречивых формул логики предикатов. Модель. Логическое следствие. Теорема о логическом следствии.
- Проблемы выполнимости и общезначимости. Пример формулы, не имеющей конечных моделей.
- Семантические таблицы в логике предикатов. Табличный вывод. Теорема корректности табличного вывода.
- Теорема полноты табличного вывода.
- Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева.
- Равносильные формулы. Примеры равносильных формул. Теорема о равносильной замене.
Метод резолюций
- Предваренная нормальная форма. Теорема о приведении формулы к предваренной нормальной форме.
- Сколемовская стандартная форма. Теорема о приведении формулы к сколемовской стандартной форме.
- Эрбрановский универсум, эрбрановский базис, эрбрановские интерпретации. Теорема об эрбрановской модели для сколемовской стандартной формы. Сведение проблемы общезначимости формул к проблеме противоречивости систем дизъюнктов. Теорема Эрбрана.
- Подстановки. Применение подстановок к термам и формулам. Композиция подстановок. Унификатор. Наиболее общий унификатор.
- Сведение задачи унификации к задаче решения системы термальных уравнений. Лемма о связке. Алгоритм унификации. Теорема о корректности и завершаемости алгоритма унификации.
- Метод резолюций для логики предикатов: правила резолюции и склейки, резолютивный вывод. Теорема корректности резолютивного вывода.
- Лемма о подъеме. Теорема полноты резолютивного вывода для логики предикатов.
- Общая схема доказательства общезначимости формул логики предикатов методом резолюций. Стратегии резолютивного вывода.
Основы логического программирования
- Использование метода резолюций для нахождения ответов на запросы. Истолкование резолютивного вывода как вычисления. Примеры вычислительных возможностей резолютивного вывода.
- Хорновские дизъюнкты. Синтаксис языка логического программирования: логические программы и запросы. Декларативная семантика логических программ. Правильный ответ.
- Теорема о пересечении эрбрановских моделей логических программ. Теорема о наименьшей эрбрановской модели. Теорема об основных правильных ответах.
- SLD-резолюция. SLD-резолютивные вычисления (опровержения) логических программ. Процедурная интерпретация SLD-выводов. Примеры SLD-опровержений успешных, тупиковых и бесконечных. Вычислимый ответ. Операционная (процедурная) семантика логических программ.
- Теорема корректности SLD-резолютивных вычислений логических программ.
- Теорема полноты SLD-резолютивных вычислений логических программ.
- Правило вычислений и его роль. R-вычислимый ответ. Переключательная лемма. Теорема о независимости правила вычислений. Теорема сильной полноты SLD-резолюции.
- Дерево SLD-вычислений логических программ. Стратегии вычислений. Полные и неполные стратегии вычислений. Стандартная стратегия исполнения логических программ. Неполнота стандартной стратегии.
- Управление исполнением логических программ. Оператор отсечения. Операционная семантика оператора отсечения.
- Отрицание в Прологе. Допущение замкнутости мира. Отрицание как неудача. Эффект немонотонности вычислений логических программ с оператором отрицания.
- Встроенные предикаты и функции. Операционная семантика встроенных средств.
- Теорема о вычислительной универсальности чистого Пролога. Теорема Чёрча о неразрешимости логики предикатов первого порядка.
Неклассические прикладные логики
- Интуиционистская логика. Модели Крипке для интуиционистской логики. Примеры интуиционистски общезначимых и необщезначимых формул. Модальные логики. Модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики.
- Проблема верификации последовательных программ. Операционная семантика типовых программных конструкций. Предусловие и постусловие. Частичная корректность программ. Тройки Хоара и их содержательный смысл. Правила вывода в логике Хоара для доказательства частичной корректности последовательных программ.
- Моделирование программ системами переходов. Темпоральная логика высказываний линейного времени (LTL): синтаксис и семантика. Применение темпоральных логик для спецификации поведения реагирующих программных систем.
- Задача проверки выполнимости формул LTL на конечной модели. Равносильные преобразования формул LTL. Табличный алгоритм проверки выполнимости формул LTL на конечной модели: основные этапы.
Основания математики
- Как устроена математика. Исчисление предикатов первого порядка. Аксиоматические теории. Элементарная геометрия. Теория множеств Цермело-Френкеля. Арифметика Пеано. Теорема Геделя о неполноте формальной арифметики.