Links und Funktionen


Inhaltsbereich

Automated Theorem Proving (ATP)

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

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 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 Moodle using this registration key: ATP2425

Place and Time

Activity Time Place Start End
Lecture Tue 16-18 c.t. Amalienstr. 73a, room 112 15.10.2024 04.02.2025
Group exercise Wed 16-18 c.t. Richard-Wagner-Str. 10, D 105 23.10.2024 05.02.2025

We will make videos of the Tuesday 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.

Schedule

The course consists of 15 lectures:

  1. Motivation and Preliminaries
    slides · exercises · solutions

  2. Preliminaries Continued and Propositional Logic
    slides · exercises · solutions

  3. Propositional Logic Continued
    slides · exercises · solutions

  4. First-Order Logic
    slides · exercises · solutions

  5. Resolution
    slides · exercises · solutions

  6. General Resolution
    slides · exercises · solutions

  7. Resolution Continued
    slides · exercises · solutions

  8. Semantic Tableaux
    slides · exercises · solutions

  9. Rewrite Systems
    slides · exercises · solutions

  10. Termination
    slides · exercises · solutions

  11. Completion
    slides · exercises · solutions

  12. Superposition
    slides · exercises · solutions

  13. Superposition Continued
    slides · exercises · solutions

  14. Efficient Saturation Procedures and Outlook
    slides · exercises · solutions

  15. Mystery Lecture + Mock Exam Q&A

Materials

The slides of the lectures are available above under Schedule. The exercise sheets are also available there. Solutions will be gradually be made available there as well. 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 course aims at teaching concepts. Therefore, the exam is on paper. It is also closed book. A handout will be provided with the most important definitions. You will be given 120 minutes to complete the exam.

The first exam (“final exam”) will take place on 11 February 2025 from 14:00 in Oettingenstr. 67, B 001. You will have 120 minutes at your disposal. Registration is open on Moodle.

If you need some adjustments to compensate for disabilities or impairments, please contact the lecturer well before the exam.

The course is being taught for the first time at the LMU. A mock exam, together with answers, is available so that you can practice.

Artikelaktionen


Funktionsleiste