Website for the course on Automated Theorem Proving


The course is given in digital form. All information will be made available at the Moodle course website before the first lecture.


  • Theoretical foundations of calculi for automated theorem proving in first-order logic 
  • Correctness and completeness proofs 
  • Algorithms and data structures used in first-order logic theorem provers 
  • Comparison of different approaches to first-order theorem proving 
  • Foundations of modern SAT and SMT solvers 

Robinson, Voronkov: Handbook of Automated Reasoning, 2 vols., North-Holland 


Highly recommended is participation in the lecture “Aussagen- und Prädiketenlogik” or a similar module on propositional and first-order logic. Basic training in mathematics should be sufficient.