|
|
| Строка 5: |
Строка 5: |
| | == Программа курса == | | == Программа курса == |
| | | | |
| − | === Логика предикатов первого порядка === | + | === Конечные автоматы и регулярные выражения === |
| | <ol> | | <ol> |
| − | <li> Синтаксис и семантика логики предикатов. Термы, формулы, интерпретация. Отношение выполнимости формулы на интерпретации. | + | <li> Конечные автоматы: определения основных понятий. Языки, распознаваемые конечными автоматами. Замкнутость класса автоматных языков относительно операций объединения, пересечения и дополнения. |
| − | <li> Выполнимость, общезначимость, противоречивость формул логики предикатов. Примеры общезначимых и противоречивых формул логики предикатов. Модель. Логическое следствие. Теорема о логическом следствии. | + | <li> Детерминированные конечные автоматы. Метод детерминизации конечных автоматов. |
| − | <li> Проблемы выполнимости и общезначимости. Пример формулы, не имеющей конечных моделей. | + | <li> Алгоритм проверки эквивалентности детерминированных конечных автоматов. |
| − | <li> Семантические таблицы в логике предикатов. Табличный вывод. Теорема корректности табличного вывода. | + | <li> Минимальные детерминированные конечные автоматы. Алгоритм минимизации детерминированных конечных автоматов. |
| − | <li> Теорема полноты табличного вывода. | + | <li> Алгебра регулярных выражений. Примеры тождеств в алгебре регулярных выражений. Регулярные языки. |
| − | <li> Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. | + | <li> Алгоритм построения регулярного выражения, определяющего язык, распознаваемый заданным конечным автоматом. |
| − | <li> Равносильные формулы. Примеры равносильных формул. Теорема о равносильной замене. | + | <li> Алгоритм построения конечного автомата, распознающего язык, определяемый заданным регулярным выражением. Теорема Клини о совпадении класса автоматных языков и класса регулярных языков. |
| | </ol> | | </ol> |
| − | === Метод резолюций === | + | === Вычислимые функции и рекурсивные множества === |
| | <ol start="8"> | | <ol start="8"> |
| − | <li> Предваренная нормальная форма. Теорема о приведении формулы к предваренной нормальной форме. | + | <li> |
| − | <li> Сколемовская стандартная форма. Теорема о приведении формулы к сколемовской стандартной форме. | + | <li> |
| − | <li> Эрбрановский универсум, эрбрановский базис, эрбрановские интерпретации. Теорема об эрбрановской модели для сколемовской стандартной формы. Сведение проблемы общезначимости формул к проблеме противоречивости систем дизъюнктов. Теорема Эрбрана. | + | <li> |
| − | <li> Подстановки. Применение подстановок к термам и формулам. Композиция подстановок. Унификатор. Наиболее общий унификатор. | + | <li> |
| − | <li> Сведение задачи унификации к задаче решения системы термальных уравнений. Лемма о связке. Алгоритм унификации. Теорема о корректности и завершаемости алгоритма унификации. | + | <li> |
| − | <li> Метод резолюций для логики предикатов: правила резолюции и склейки, резолютивный вывод. Теорема корректности резолютивного вывода. | + | <li> |
| − | <li> Лемма о подъеме. Теорема полноты резолютивного вывода для логики предикатов. | + | <li> |
| − | <li> Общая схема доказательства общезначимости формул логики предикатов методом резолюций. Стратегии резолютивного вывода. | + | <li> |
| | </ol> | | </ol> |
| − | === Основы логического программирования === | + | === Формальные грамматики и языки === |
| | <ol start="16"> | | <ol start="16"> |
| − | <li> Использование метода резолюций для нахождения ответов на запросы. Истолкование резолютивного вывода как вычисления. Примеры вычислительных возможностей резолютивного вывода. | + | <li> |
| − | <li> Хорновские дизъюнкты. Синтаксис языка логического программирования: логические программы и запросы. Декларативная семантика логических программ. Правильный ответ. | + | <li> |
| − | <li> Теорема о пересечении эрбрановских моделей логических программ. Теорема о наименьшей эрбрановской модели. Теорема об основных правильных ответах. | + | <li> |
| − | <li> SLD-резолюция. SLD-резолютивные вычисления (опровержения) логических программ. Процедурная интерпретация SLD-выводов. Примеры SLD-опровержений успешных, тупиковых и бесконечных. Вычислимый ответ. Операционная (процедурная) семантика логических программ. | + | <li> |
| − | <li> Теорема корректности SLD-резолютивных вычислений логических программ. | + | <li> |
| − | <li> Теорема полноты SLD-резолютивных вычислений логических программ. | + | <li> |
| − | <li> Правило вычислений и его роль. R-вычислимый ответ. Переключательная лемма. Теорема о независимости правила вычислений. Теорема сильной полноты SLD-резолюции. | + | <li> |
| − | <li> Дерево SLD-вычислений логических программ. Стратегии вычислений. Полные и неполные стратегии вычислений. Стандартная стратегия исполнения логических программ. Неполнота стандартной стратегии. | + | <li> |
| − | <li> Управление исполнением логических программ. Оператор отсечения. Операционная семантика оператора отсечения. | + | <li> |
| − | <li> Отрицание в Прологе. Допущение замкнутости мира. Отрицание как неудача. Эффект немонотонности вычислений логических программ с оператором отрицания. | + | <li> |
| − | <li> Встроенные предикаты и функции. Операционная семантика встроенных средств. | + | <li> |
| − | <li> Теорема о вычислительной универсальности чистого Пролога. Теорема Чёрча о неразрешимости логики предикатов первого порядка. | + | <li> |
| | </ol> | | </ol> |
| | | | |
| − | === Неклассические прикладные логики === | + | === Алгоритмически неразрешимые математические задачи === |
| | <ol start="28"> | | <ol start="28"> |
| − | <li> Интуиционистская логика. Модели Крипке для интуиционистской логики. Примеры интуиционистски общезначимых и необщезначимых формул. Модальные логики. Модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики. | + | <li> |
| − | <li> Проблема верификации последовательных программ. Операционная семантика типовых программных конструкций. Предусловие и постусловие. Частичная корректность программ. Тройки Хоара и их содержательный смысл. Правила вывода в логике Хоара для доказательства частичной корректности последовательных программ. | + | <li> |
| − | <li> Моделирование программ системами переходов. Темпоральная логика высказываний линейного времени (LTL): синтаксис и семантика. Применение темпоральных логик для спецификации поведения реагирующих программных систем. | + | <li> |
| − | <li> Задача проверки выполнимости формул LTL на конечной модели. Равносильные преобразования формул LTL. Табличный алгоритм проверки выполнимости формул LTL на конечной модели: основные этапы. | + | <li> |
| − | </ol>
| + | |
| − | | + | |
| − | === Основания математики ===
| + | |
| − | | + | |
| − | <ol start="32">
| + | |
| − | <li> Как устроена математика. Исчисление предикатов первого порядка. Аксиоматические теории. Элементарная геометрия. Теория множеств Цермело-Френкеля. Арифметика Пеано. Теорема Геделя о неполноте формальной арифметики.
| + | |
| | </ol> | | </ol> |
