Automated Theorem Proving

Timisoara, Summer Semester 2018


The first 9 lectures took place in May.

The next lectures are:


There are 36 exercises in homeworks.pdf.

For the admission to the examination it is necessary to solve at least 18 exercises before the lectures on 10th of June.

Every additional 9 exercises counts as an additional point at the final mark of 1 to 10. (For exercises 32 and 35-36 use the definitions and examples from the lecture notes.) You can bring the solution to the next lecture or you can send it by e-mail in advance.

In case you send your homeworks by e-mail, please use my address

Also please use as name of the file[s] your name and the number of the homework, e. g. like Popescu-I-3.pdf or Ionescu-P-4.jpg. Please do not use Windows Word files (*.doc) because the special symbols are not shown correctly on different systems. If you do not have alternative to Word, then please print the file using the option "Print to file" and send this file too.


  • Introduction
  • Propositional Logic

    Additional Material

    Lecture notes: Introduction-to-ATP-Jebelean-5-Jun-2018.pdf.

    The contents of the lecture is very similar to the transcript by Martin Koehler of previous lectures: pdf file. (May contain some typos and small errors.)

    For more details (some of which are not covered in the lecture) I recommend: Bruno Buchberger: Logic for Computer Science pdf file. This material is copyrighted and is available only for the students of this lecture and only for the purpose of study related to it.

    The home page of the similar lecture in Linz: WS 2016 may give you an idea about the contents and the homeworks, although the current lecture will not be exactly the same.