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

Последнее изменение: 05/02/2025 08:44:23

Основной курс для алгоритмического бакалавриата ИРИТ-РТФ. В весеннем семестре 2024/2015 учебного года читается по четвергам с 16:10, ауд. 628.

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

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

Литература

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

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