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 |
