City: Saint Petersburg Novosibirsk Kazan Language: Русский English

A survey of automated theorem proving
Saint Petersburg / autumn 2013, посмотреть все семестры

Enroll in the course to get notifications and to be able to submit home assignments.
Register to enroll now Login

In these lectures I will give a general overview of automated theorem proving in the broad sense, including fully automated methods, interactive methods and their applications in both mathematics and computing. The content of the course will be quite strongly influenced by my book and its associated code, but will be more high-level and include more discussion of applications.

Date and time Class|Name Venue|short Materials
28 September
Background, history and propositional logic, Lecture ПОМИ РАН slides,  video
28 September
First-order logic with and without equality, Lecture ПОМИ РАН video
29 September
Decidable problems in logic and algebra, Lecture ПОМИ РАН video
29 September
Interactive theorem proving and proof-checking, Lecture ПОМИ РАН video
29 September
Applications to mathematics and computer verification, Lecture ПОМИ РАН No