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 http://www.cambridge.org/9780521899574 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
17:20–18:55
Background, history and propositional logic, Lecture ПОМИ РАН slides,  video
28 September
19:05–20:40
First-order logic with and without equality, Lecture ПОМИ РАН video
29 September
11:15–12:50
Decidable problems in logic and algebra, Lecture ПОМИ РАН video
29 September
13:00–14:35
Interactive theorem proving and proof-checking, Lecture ПОМИ РАН video
29 September
15:35–17:10
Applications to mathematics and computer verification, Lecture ПОМИ РАН No