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.