The course discusses the techniques behind automated theorem provers. Among others the topics are:
Tableau-based and resolution-based calculi including their variants:
- regular tableau,
- strong and weak connection tableaus,
- lock resolution,
- SOS resolution,
- DPLL, theories (SMT prover) etc. and
- correctness and completeness proof of the different calculi
Implementation near techniques like efficient indexing of terms are also discussed.
- Dozent*in: Richard Bubel
- Dozent*in: Antonio Enrique Flores Montoya
- Dozent*in: Reiner Hähnle