Лектор Герасимов Александр Сергеевич
Язык логики высказываний и его семантика
Слова, вхождения, формальные языки: определения и примеры.
Язык логики высказываний.
Интерпретация языка логики высказываний, истинностное значение формулы.
Пропозициональные тавтологии, примеры.
Логика высказываний: логическое следствие, теорема о логическом следствии, логически эквивалентные формулы.
Теорема о подстановке пропозициональных формул в пропозициональную тавтологию.
Теорема об эквивалентной замене (семантический вариант) для логики высказываний.
Теорема о выражении булевой функции формулами, находящимися в конъюнктивной и дизъюнктивной нормальных формах.
Теорема о выражении булевой функции пропозициональной формулой, в которую из логических связок входит только одна.
Выражение булевой функции полиномом Жегалкина.
Общее понятие исчисления
Исчисление и вывод: определения и примеры.
Вывод из гипотез: определения и примеры.
Исчисление высказываний гильбертовского типа
Формулировка исчисления высказываний гильбертовского типа. Пример вывода.
Теоремы о корректности и непротиворечивости исчисления высказываний гильбертовского типа.
Теорема о дедукции для исчисления высказываний гильбертовского типа.
Техника естественного вывода для исчисления высказываний гильбертовского типа.
Определения совместного, непротиворечивого и полного множеств пропозициональных формул. Теорема о непротиворечивости совместного множества пропозициональных формул.
Теорема о совместности непротиворечивого множества пропозициональных формул (с леммами).
Теоремы о компактности для логики высказываний и о полноте исчисления высказываний гильбертовского типа.
Поиск вывода в исчислении высказываний гильбертовского типа. Алгоритм Британского музея.
Секвенциальное исчисление высказываний генценовского типа
Систематический поиск контрпримера для пропозициональной формулы.
Формулировка секвенциального исчисления высказываний генценовского типа.
Пример вывода в секвенциальном исчислении высказываний. Дерево поиска вывода и дерево вывода.
Теоремы о корректности и полноте секвенциального исчисления высказываний.
Некоторые правила, допустимые в секвенциальном исчислении высказываний.
Язык логики предикатов и его семантика
Определение языка первого порядка.
Основные определения, касающиеся вхождений предметных переменных в предикатные формулы.
Интерпретация языка первого порядка, истинностное значение формулы.
Примеры языков первого порядка и их интерпретаций.
Выражение предиката формулой, примеры.
Свободные подстановки.
Конгруэнтные формулы. Лемма о чистоте переменных.
Переименование связанных переменных, правильные подстановки.
Общезначимые предикатные формулы, логическое следствие, теорема о логическом следствии, логически эквивалентные формулы.
Утверждения о логической эквивалентности некоторых предикатных формул, в том числе теорема об эквивалентной замене (семантический вариант). Доказательства нескольких утверждений.
Теорема о предварённой нормальной форме.
Исчисление предикатов гильбертовского типа
Формулировка исчисления предикатов гильбертовского типа. Пример вывода.
Теоремы о корректности и непротиворечивости исчисления предикатов гильбертовского типа.
Теорема о дедукции для исчисления предикатов гильбертовского типа.
Теорема о выводимости (в исчислении предикатов гильбертовского типа) частного случая пропозициональной тавтологии. Некоторые правила, допустимые в исчислении предикатов гильбертовского типа.
Определения совместного, непротиворечивого и полного множеств предикатных формул. Теорема о непротиворечивости совместного множества предикатных формул.
Теорема о существовании модели (без доказательства). Теорема Лёвенгейма-Скулема, теоремы о компактности для логики предикатов и о полноте исчисления предикатов гильбертовского типа.
Синтаксическая эквивалентность формул. Теорема об эквивалентной замене (синтаксический вариант).
Секвенциальное исчисление предикатов генценовского типа
Систематический поиск контрпримера для формулы с кванторами.
Формулировка секвенциального исчисления предикатов генценовского типа. Пример вывода в этом исчислении.
Теоремы о корректности и непротиворечивости секвенциального исчисления предикатов.
Теорема о полноте секвенциального исчисления предикатов (без доказательства), соотношение секвенциального исчисления предикатов и исчисления предикатов гильбертовского типа, допустимость правила сечения.
Формальные аксиоматические теории
Формальные аксиоматические теории: основные определения.
Теории с равенством: определения и примеры.
Теорема о существовании нормальной модели.
Аксиомы элементарной арифметики.
Нестандартная модель арифметики.
Доказательство коммутативности сложения в элементарной арифметике.
Наивная теория множеств. Парадокс Рассела.
Аксиомы теории множеств Цермело-Френкеля.
Теория множеств Цермело-Френкеля: упорядоченная пара и теорема о её основном свойстве.
Отношения и функции в теории множеств Цермело-Френкеля. Аксиома выбора.
Натуральные и целые числа в теории множеств Цермело-Френкеля.
Метод резолюций и основы логического программирования
Метод резолюций для логики высказываний, теорема о его корректности.
Скулемовская стандартная форма: определение, примеры, представление в виде множества дизъюнктов.
Теорема о выполнимости формулы и её скулемовской стандартной формы.
Эрбрановская интерпретация множества дизъюнктов: определения и примеры.
Теорема о ложности множества дизъюнктов в эрбрановских интерпретациях.
Семантические деревья для множества дизъюнктов: определения и примеры.
Теорема Эрбрана в терминах семантических деревьев.
Теорема Эрбрана в терминах основных примеров дизъюнктов.
Алгоритм проверки невыполнимости множества дизъюнктов, основанный на теореме Эрбрана.
Унификаторы: определения и примеры.
Алгоритм унификации.
Метод резолюций для логики предикатов, его корректность, примеры.
Лемма подъёма.
Теорема о полноте метода резолюций для логики предикатов.
Алгоритм доказательства методом резолюций.
Логическая программа и её декларативная семантика.
SLD-резолюция. Пример представления знаний в виде логической программы и поиска ответа на запрос к логической программе.
Операционная семантика логической программы. Теорема о корректности вычисленной подстановки.
Теория вычислимости
Машины Тьюринга.
Вычислимые по Тьюрингу функции. Тезис Чёрча.
Нормальные алгорифмы Маркова.
Разрешимые и перечислимые множества натуральных чисел. Теорема Поста.
Теорема о равносильности четырёх определений перечислимого множества натуральных чисел.
Разрешимые и перечислимые отношения на натуральных числах.
Теоремы о проекции.
Разрешимые и перечислимые языки и словарные отношения.
Нумерация вычислимых функций.
Теорема о параметризации.
Универсальные функции. Теорема о непродолжимости универсальной функции.
Понятие массовой проблемы разрешения. Теоремы о неразрешимости проблем самоприменимости и остановки. Пример неперечислимого множества.
Теорема о рекурсии.
Теорема Райса.
Постановка проблемы эквивалентности для ассоциативных исчислений и проблемы равенства для полугрупп.
Теорема о существовании ассоциативного исчисления с неразрешимой проблемой эквивалентности.
Теоремы о неразрешимости проблемы общезначимости и проблемы выводимости для исчисления предикатов.
Перечислимость множества теорем рекурсивно аксиоматизируемой теории.
Эффективно неотделимые множества.
Теорема Гёделя о неполноте арифметики в форме Россера.
Теорема о неразрешимости арифметики.
Вторая теорема Гёделя.
Элементы теории сложности вычислений
Задачи распознавания, кодирование и языки. Временная и ёмкостная сложность детерминированной машины Тьюринга. Класс P.
Недетерминированная машина Тьюринга, её временная и ёмкостная сложность. Класс NP.
Теорема о совпадении класса NP с классом полиномиально верифицируемых языков.
Теорема о временной сложности детерминированной машины Тьюринга, распознающей язык из класса NP.
Полиномиальная сводимость, NP-полные языки: определения и простейшие теоремы.
Примеры NP-полных языков.
Исчисление Хоара для доказательства корректности программ
Определение программы и её операционной семантики.
Аксиоматическая семантика программы: формулировка исчисления Хоара. Пример вывода в этом исчислении.
Теорема о корректности исчисления Хоара относительно операционной семантики.