Automated Theorem Proving (ATP, WiSe 2026/27)

Lecture 2 hours, Blanchette; exercises 2 hours, Desharnais-Schäfer and Bozec.

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 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

Please register on both LSF and Moodle (Moodle registration key: ATP202627).

Place and Time

Videos from the WiSe 2025/26 edition of the course are available on LMUcast as a convenience to students with scheduling conflicts. We offer no guarantees about the videos' availability or quality.

Schedule

The course consists of 15 lectures:

  1. Motivation and Preliminaries
    slides · exercises

  2. Preliminaries Continued and Propositional Logic
    slides · exercises

  3. Propositional Logic Continued
    slides · exercises

  4. First-Order Logic
    slides · exercises

  5. Resolution
    slides · exercises

  6. General Resolution
    slides · exercises

  7. Resolution Continued
    slides · exercises

  8. Semantic Tableaux (*)
    slides · exercises

  9. Rewrite Systems
    slides · exercises

  10. Termination
    slides · exercises

  11. Completion (*)
    slides · exercises

  12. Superposition
    slides · exercises

  13. Superposition Continued
    slides · exercises

  14. Efficient Saturation Procedures and Outlook (*)
    slides · exercises

  15. Mystery 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-26W27-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.

The lecture notes cover most of the same material as the slides but with more details, especially proofs.

Exams

A regular exam and a retake exam, both scheduled at the end of the semester, will test your understanding. The exams 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. 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 third time at the LMU. Past exams:

To top