Automated Theorem Proving (ATP)

Lecture 2 hours, Blanchette; exercises 2 hours, Kondylidou

Recognized as “Fortgeschrittene Themen der theoretischen Informatik” and “Vertiefende Themen der Informatik”.

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 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 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 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 assistant: Lydia Kondylidou

Place and Time

Schedule

The course consists of the following 15 lectures:

1. Motivation and Preliminaries

2. Preliminaries Continued and Propositional Logic

3. Propositional Logic Continued

4. First-Order Logic

5. Resolution

6. General Resolution

7. Resolution Continued

8. Semantic Tableaux

9. Rewrite Systems

10. Termination

11. Completion

12. Superposition

13. Superposition Continued

14. Efficient Saturation Procedures and Outlook

15. Mystery Lecture