Математическая логика и интеллектуальные системы

В курсе рассматривается пропозициональная логика, логика первого порядка и темпоральная логика. Семантические и дедуктивные свойства каждой логики описываются в свете их применения при создании интеллектуальных системах для решения практических задач. В первую очередь – это проблема выполнимости булевых формул, проблема общезначимости формул первого порядка, логическое программирование, верификация последовательных и параллельных программ. Будут рассмотрен метод резолюций, двоичные разрешающие диаграммы, DPLL алгоритм, SLD-резолюция, метод верификации на основе проверки модели и др.