Lecture: Automated Theorem Proving


  • Propositional Calculus: syntax, semantics, satisfiability, validity, clause normal form, resolution calculus, model construction, optimiesations
  • First-Order Logic: syntax, semantics, Skolemisation, Herbrand models, unification, resolution calculus, well-founded orderings, refutational completeness
  • Theorem Proving with Equality: term replacement systems, Church-Rosser theorem, Knuth-Bendix completion, paramodulation calculus, superpositions calculus
  • Application Flow of Saturation Procedures: given clause algorithm, completeness and fairness
  • Decidable fragments of First-Order Logic: Bernays-Schönfinkel class, monadic fragment, two-variable fragment, guarded fragment, resolution-based decision procedures
  • Other Theorem Proving Methods: chaining calculus, disconnection calculus, instantiation calculus



Tuesday: 12:30 — 14:00 in O27/121
Friday: 10:15 — 11:45 in O27/121
Consultation Hours: after the lectures or by appointment


The exercises take place within the lecture time slots about every two weeks. The exact dates are announced in the lecture. 


The lecture notes, slides, and exercises are available through Moodle. The lecture notes can be printed through the Script printing system of SGI.

Literature and References

General reading material for the lecture:

  • John Alan Robinson, Andrei Voronkov (Eds.). Handbook of Automated Reasoning, Elsevier and MIT Press 2001, ISBN 0-444-50813-9,0-262-18223-8: Volume 1, Chapter 2, Chapter 6, Chapter 7
  • Uwe Schöning. Logik für Informatiker. Spektrum. ISBN 3-8274-1005-3
  • Melvin Fitting. First-Order Logic and Automated Theorem Proving. Springer. ISBN 0-387-94593-8
  • Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge Univ. Press, 1998, ISBN 978-0521779203

    Technical Information

    Type:Lecture for Master Students (3V / 1Ü)
    Credit Points:6
    Curriculae:Theoretische und Mathematische Methoden der Informatik (Kernfach/Kernmodul)
    Theoretische Informatik (Vertiefungsmodul)
    Intelligente Systeme (Vertiefungsmodul)
    Related Lectures:     Intelligente Handlungsplanung
    Grundlagen des Semantic Web