Кафедра математической логики и теории алгоритмов

Дневник лекций 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 трудность этой проблемы
для исчисления высказываний и большинства теорий первого порядка.
Примеры неразрешимых теорий. Теорема Фишера — Рабина (без доказательства).

Аксиоматизация и разрешимость элементарной теории поля комплексных чисел.