Master Practical: Automated Theorem Provers

Instructors: Massin Guerdi, Lydia Kondylidou

2+2 hours per week

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 focus on practical aspects of automated theorem provers and their implementation.

Organization

The course is divided into two parts. In the first part of the course, participants will receive a brief introduction to automated theorem proving, focused on practical aspects.

This will be followed by a project phase, with students working in teams of 2-4 people.

Each team is tasked with delivering a presentation on relevant background material (such as research articles), proposing, implementing and documenting a project, as well as giving a final project presentation.

Participation is limited to 30 master students.

Prerequisites

At a minimum, familiarity with basic aspects of mathematical logic, such as those taught in the bachelor’s lecture “Logik und diskrete Strukturen”, is required.

The practical complements the lecture Automated theorem proving that was offered in the winter term 2024/25. If you are interested in the practical, we highly recommend reviewing the course materials from the lecture.

Place and Time

The given end dates are tentative.

The exercise sessions start in the third week of the semester (one week after the first lecture). The exercise session on the 29.05.2025 (Christi Himmelfahrt) and 19.06.2025 (Fronleichnam) are canceled due to holidays.

Moodle

To register for the course, see Moodle.