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.