На первой лекции будут даны основные определения и рассмотрены примеры систем доказательств. Для понимания курса полезно (но не обязательно!)знание базовых определений теории вычислимости и сложности: машина Тьюринга, (не)вычислимость, класс NP, сводимости между вычислительными задачами: если Вы с ними когда-то познакомились, освежите свои знания перед первой лекцией.