Automated Theorem Proving (ATP, WiSe 2025/26)
Lecture 2 hours, Blanchette; exercises 2 hours, Xu, Bozec, and Kondylidou
For BSc students, the course is officially called Automated Theorem Proving for Bachelor.
Overview
Automated theorem proving is a subfield of mathematical logic that concerns itself with proving mathematical theorems fully automatically using computer programs. These programs are called automated theorem provers. They can be used as standalone 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 review some of the main approaches to automated theorem proving. The course focuses on the theory of theorem proving. Stylistically, the course has a mathematical flavor (with definitions, lemmas, proofs, etc.).
The course is based on the materials from Dr. Uwe Waldmann's courses Automated Reasoning I and Automated Reasoning II at Saarland University. We are grateful to him for letting us use his materials.
Organization
2+2 hours per week
Lecturer: Prof. Dr. Jasmin Blanchette
Teaching assistants: Yiming Xu, PhD, Tanguy Bozec, and Lydia Kondylidou
Please register on both LSF and Moodle (Moodle registration key: ATP202526).
Place and Time
TBD
| Activity | Time | Place | Start Date | End Date |
|---|---|---|---|---|
| Lecture | Tue 16–18 c.t. | Amalienstr. 73a, Room 211 | 03.02.2026 | |
| Group Exercise | Thu 14–16 c.t. | Amalienstr. 73a, Room 211 | 05.02.2026 |
``
Note that the group exercises start the week after the first lecture.
We will make videos of the lectures and the group exercises available on LMUcast as a convenience to students with scheduling conflicts. We will do our best to put the videos online shortly after the respective lectures, but we offer no guarantees about the videos' availability or quality.
Videos from WiSe 2024/25 are also available. The covered content is roughly equivalent to this year's.
Schedule
The course consists of 15 lectures:
Preliminaries Continued and Propositional Logic
slides · exercisesEfficient Saturation Procedures and Outlook (
*)
slides · exercisesMystery Guest
Lectures marked with an asterisk (*) cover material that is relevant for the exams for MSc students but not for BSc students.
Chat
There is a Zulip chat stream associated with the course where you can ask organizational and content-related questions. Please use it if possible, instead of sending us emails, so that your fellow students can also benefit from the answers.
Zulip-Server: https://chat.ifi.lmu.de/
Stream: TCS-25W26-ATP
Materials
The slides of the lectures are available above under Schedule. The exercise sheets are also available there. Solutions for sheet i will be presented on week i + 1 in the group exercise and made available online afterward. All materials are provided for your convenience and are subject to changes.
There are also lecture notes that cover most of the same material as the slides but with more details, especially proofs.
Exams
A written exam at the end of the semester will test your understanding. The exam will be on paper and closed book. A handout will be provided with the most important definitions. You will be given 120 minutes to complete the exam. There will also be a retake exam. Registration is mandatory and will be via LSF.
If you need some adjustments to compensate for disabilities or impairments, please contact the lecturer at least one week before the exam.
A mock exam, together with answers, is available so that you can practice. All of the questions in the mock exam are relevant for both BSc and MSc students.
The course is being taught for the second time at the LMU. Here is the regular exam from WiSe 2024/25, together with answers. Question 2(c) is out of scope for BSc students. Here is the retake exam from WiSe 2024/25, together with answers. Question 1(b) is out of scope for BSc students.