Приглашаю всех, интересующихся логическими аспектами CS, на свой спецкурс "Вычислительная логика и теория доказательств", который будет проходить по четвергам в ауд. 16-24 с 16 ч. 20 м.
первая лекция - 13 февраля
Сразу после спецкурса будет работать семинар "Математическая теория программирования" в ауд. 14-13
Конспекты лекций будут размещаться на моей страничке
http://u.pereslavl.ru/~mironov по мере их подготовки.
Аннотация:
В спецкурсе будут изложены основные вопросы, относящиеся к вопросам автоматизации логического вывода и общей теории доказательств. Также будут отражены приложения вычислительной логики к решению основных проблем математической теории программирования.
Программа курса:
Логика предикатов. Сколемовская нормальная форма.
Теорема Эрбрана.
Метод резолюций и его полнота.
Метод семантических таблиц.
Семантическая резлюция и ее полнота.
Лок-резолюция.
Линейная резолюция
Парамодуляция и гиперпарамодуляция
Процедура Правица
V-резолюция
Верификации программ методом резолюций
Алгоритмы синтеза программ
Обратный метод Маслова поиска вывода
Теорема Геделя о неполноте произвольных примитивно рекурсивных расширений формальной арифметики. Теорема Леба.
Логика Геделя-Леба и ее алгебраическая семантика. Логика Соловея.
Теорема Соловея о принципах доказуемости формальной арифметики.
Операторная логика доказательств С.Н.Артемова и ее арифметическая полнота.
Литература:
Ч. Чень, Р. Ли. Математическая логика и автоматическое доказательство теорем. Москва, "Наука", 1983
