Automated Theorem Proving WS 22/23

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.

Contents:

  • 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 

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

Prerequisites:

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.