Course on Automated Theorem Proving
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” (propositional and first-order logic) or a similar module. Basic training in mathematics should be sufficient.
- Dozent*in: Richard Bubel
- Dozent*in: Lukas Grätz
- Dozent*in: Reiner Hähnle