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
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.
- Dozent*in: Richard Bubel
- Dozent*in: Lukas Grätz
- Dozent*in: Reiner Hähnle