Дневник лекций 2015 года
Дневник лекций 2015 года
19 сентября 2015
Формулы, таблицы истинности, тавтологии, выполнимые формулы.
Основные логические законы в форме тавтологий.
Полиномиальный алгоритм проверки выполнимости 2-КНФ.
Полиномиальный алгоритм поиска присваивания, которое делает
истинным 7/8 конъюнкций данной 3-КНФ.
26 сентября 2015
Исчисление секвенций. Теорема корректности. Теорема о полноте.
Выводы в исчислении секвенций.
Исчисление резолюций. Теорема корректности.
Доказательства невыолнимости КНФ в исчислении резолюций.
Доказательства тавтологий общего вида в исчислении резолюций.
3 октября 2015
Правило ослабления. Теорема полноты для исчисления резолюций.
Исчисление высказываний. Теорема корректности.
10 октября 2015
Лемма о дедукции. Правило сведения к противоречию. Правило разбора случаев.
Доказательство теоремы полноты исчисления высказываний.
17 октября 2015
Язык логики предикатов. Сигнатуры, модели. Термы, формулы.
Определение истинности по Тарскому.
24 октября 2015
Общезначимые и выполнимые формулы. Равносильные формулы, примеры равносильных формул.
Приведение формул к предварённой нормальной форме.
Изофорфизм и элементарная эквивалентость моделей. Теорема о сохранении
истинности при изоморфизме. Автоморфизмы.
31 октября 2015 лекции не было (сессия)
7 ноября 2015
Теории, семантическое следование, совместные и полные теории.
Доказательство элементарной эквивалентности с помощью построения
гомоморфизма на.
Доказательство невыразимости с помощью автоморфизмов.
14 ноября 2015
Элиминация кванторов в целых числах с функцией следования. Элиминация
кванторов в рациональных числах со сложением и порядком и константами 0,1.
Алгоритм разрешения элементарных теорий и полная система аксиом для этих моделей.
Семинары: аксиоматизация натуральных чисел с функцией следования. Аксиомиатизация
рациональных чисел со сложением и порядком, но без констант 0,1. Аксиоматизация
целых чисел с порядком и сложением.
21 ноября 2015
Аксиомы и правила вывода исчисления предикатов.
Корректность исчисления предикатов.
Правило обобщения.
Семинары: выводы в исчислении предикатов.
28 ноября 2015
Лемма о дедукции для ИП. Непротиворечивые и полные теории.
Теорема Геделя о полноте (первая форма): всякая непротиворечивая
теория имеет модель. Теорема Геделя о полноте (вторая форма): семантическое следование
влечет дедуктивное следование.
Аксиомы равенства. Теорема Гёделя о полноте для теорий
с равенством.
Теорема компактности Мальцева.
Семинары: задачи о спектре формул.
5 декабря 2015
Способы задания теорий первого порядка: аксиоматический и семантический.
Проблема разрешения теории первого порядка. NP трудность этой проблемы
для исчисления высказываний и большинства теорий первого порядка.
Примеры неразрешимых теорий. Теорема Фишера — Рабина (без доказательства).
Аксиоматизация и разрешимость элементарной теории поля комплексных чисел.