Automated Theorem Proving (ATP, WiSe 2025/26)

Lecture 2 hours, Blanchette; exercises 2 hours, Xu, Bozec, and Kondylidou

Recognized as “Fortgeschrittene Themen der theoretischen Informatik” and “Vertiefende Themen der Informatik”. 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

Place and Time

Note that the group exercises start on the term’s second week.

We will make videos of the lectures available on LMUcast as a convenience to students with schedule conflicts. We will do our best to put the videos online shortly after the lecture, but we offer no guarantees about their 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:

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 Lecture + Mock Exam Q&A

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

The exam is 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.

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.

The course is being taught for the second time at the LMU. Here is the final exam from WiSe 2024/25, together with answers. Here is the retake exam from WiSe 2024/25, together with answers.