Математическая логика

Последнее изменение: 22/05/2014 19:00:00

Основной курс для потока КН-КБ второго курса. В весеннем семестре 2013/2014 учебного года читается по понедельникам с 16:10, ауд. 632.

Содержание курса

  • Логика высказываний (ЛВ). Законы ЛВ. Теорема о конъюнктивной нормальной форме. Логическое следствие. Метод резолюций для ЛВ. Полнота метода резолюций для ЛВ.
  • Логика предикатов (ЛП). Законы ЛП. Предваренная нормальная форма. Скулемизация. Алгоритм унификации. Метод резолюций для ЛП. Теорема Эрбрана. Полнота метода резолюций для ЛП.
  • Различные приложения метода резолюций (базы данных, планирование операций, логическое программирование). Реализации метода резолюций. Обзор современных систем автоматического доказательства.
  • Монадическая логика второго порядка и регулярные языки. Теорема Бюхи-Элгота-Трахтенброта. Языки бесконечных слов.

Литература

Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.: Наука, 1983.

Задачи по разделу "Монадическая логика второго порядка и регулярные языки"

Курсовые работы, связанные с курсом "Математическая логика": сориты Льюиса Кэррола

Соритами в классической логике называют цепочки силлогизмов. Льюис Кэррол (автор "Алисы в стране чудес") придумал много забавных соритов для иллюстрации своего символического логического исчисления. Они собраны в его книге "Символическая логика", перевод которой вошел в сборник "История с узелками" (М.: Мир, 1985). Идея предлагаемого исследования состоит в том, чтобы прорешать сориты из сборника с помощью метода резолюций, найти ошибочные сориты (т.е. те, в которых заключение на самом деле не следует из посылок), сравнить их с оригиналом и исправить.

Смотрите также: