Курс состоит из трех частей. Первая часть посвящена базе математической логики – теории двоичных функций. Вторая часть излагает базовые разделы математической логики, наиболее часто применяемые в практике информационных технологий: методы формализации умозаключений, алгоритмы формального логического вывода, аксиоматические теории. Заключительная часть посвящена методам верификации распределенных алгоритмов и систем.

В результате изучения дисциплины студент должен:

- знать понятия, определения, термины, методы, алгоритмы, способы решения задач логики высказываний; логики предикатов и соответствующих исчислений.
- уметь оценить сложность алгоритмов, выделить легко и трудноразрешимые задачи, оценить классы задач P и NP.
- овладеть базовыми методами и алгоритмами проверки логического следования, проверки корректности программ, способами определения сложности вычислений и организации эффективных алгоритмов.