Automated Theorem Proving in First-Order and Higher-Order Logic

Thursday, 16:15 -17:45, Room: HS 002, Bldg.: 45

Special  Course, Logic and Computation, 6 Credit Points

Background Needed:     
Basic knowledge about first-order logic and resolution based theorem proving is useful.
For some introductory reading see below (e.g. Huth, Fitting).

Related Modules:          
Automated Reasoning (Vorlesung)
Einführung in die Computationale Logik (Vorlesung)


Christoph Benzmueller, Room 2.12, Tel. 4574,  Email:

Preliminary Module Outline

The following module outline is preliminary and may be changed: Due to the overlap with the two related modules mentioned above the idea is to concentrate more on semantics and mechanisation of higher-order logic. This means that we will probably skip Lectures 1-5 and instead more deeply concentrate on the topics of Lectures 6-12.

Lecture 1-4 : Theorem Proving in Classical Propositional and First-Order Logic
Lecture 5: First-Order Theorem Provers in Practice
Lecture 6-8: Introduction to Classical Higher-Order Logic
Lecture 9+10: Theorem Proving in Higher-order Logic
Lecture 11: Landscape of Higher-Order Semantics

Lecture 12: Higher-Order Theorem Provers in Practice


They are included in the slides below. Here are the solutions (version from 22.July after lecture).


Slides-I (Lectures I-VI), Slides-II (Lectures VII-X)

Student contributions: Eyad Alkassar, Joerg-Mueller, Ruzica-Piskac-I, Ruzica-Piskac-II, Mohammed-Abushammala, Andrey Shadrin, Anna Marchenkova, Marc Wagner, Matthias Berg, Robert Grabowski


Oral exam at the end of term;  here is the schedule.

Theorem Provers


A bunch of other provers can be found at


Introduction to first-order logic and deduction systems:
Introduction to higher-order logic:
Introduction to typed lambda-calculus:
At the core of the lecture:
Other useful reading: