Master Practical: Automated Theorem Provers (SoSe 2026)
Instructor: Massin Guerdi
2+2 hours per week
LSF: TBA
Moodle: TBA
Overview
Automated theorem proving is a subfield of mathematical logic that concerns itself with proving mathematical theorems fully automatically using computer programs, called automated theorem provers. They can be used as stand-alone programs to solve logic problems or in tandem with interactive theorem provers (also called proof assistants) to discharge proof obligations that arise in interactive proofs.
In this course, we will focus on practical aspects of automated theorem provers and their implementation.
Organization
The course is divided into two parts. In the first part of the course, participants will receive a brief introduction to automated theorem proving, focused on practical aspects.
This will be followed by a project phase, with students working in teams of 2-4 people.
Each team is tasked with delivering a short presentation on relevant background material (such as research articles), proposing, implementing and documenting a project, as well as giving a final project presentation.
Participation is limited to 20 master students.
Prerequisites
Familiarity with basic aspects of mathematical logic, such as those taught in the bachelor's lecture "Logik und diskrete Strukturen", is required.
The practical complements the lecture Automated Theorem Proving that was offered in the winter term 2025/26. If you are interested in the practical, we highly recommend reviewing the course materials from the lecture.
Place and Time
The given schedule is tentative and subject to change.
| Activity | Time | Place | Start | End |
|---|---|---|---|---|
| Lecture | Tue, 16-18 c.t. | Oettingenstr. 67, Room 161 | 2026-04-14 | 2026-05-26 |
| Group exercise | Thu, 12-14 c.t. | Oettingenstr. 67, Room 033 | 2026-04-16 | 2026-05-28 |
Due to holidays there are no exercises on 2026-05-14.
Important Dates
The given schedule is tentative and subject to change.
Project proposals due date: Mon., May 25th 2026
Short introductory presentations: Tue., June 2nd 2026
Final project submission: Fri., July 31st 2026
Final project presentations: between Mon., August 10th 2026 and Fri. August 21st 2026
Registration
Central allocation (Zentralanmeldung) via LSF
Projects
Possible projects include implementing
- Tableau
- First-Order Resolution
- First-Order Superposition
- Higher-Order Superposition
- new indexing techniques
- new heuristics for existing provers
- ...