16.10.2018: IntroSlides   Slides

18.10.2018: Slides   Script

23.10.2018: Slides  Script

25.10.2018: Slides  Script  Figures

30.10.2018: Slides  Script

06.11.2018: Slides  Script  Errata: Slides

08.11.2018: Slides  Script

13.11.2018: Slides

15.11.2018: Slides  Script

20.11.2018: Slides  Script

22.11.2018: Slides

27.11.2018: Slides

29.11.2018: Slides  Script

04.12.2018: Slides  Script

06.12.2018: Slides  Script

11.12.2018: Slides

18.12.2018: Slides

08.01.2019: Slides

10.01.2019: Slides  Script

15.01.2019: Slides

17.01.2019: Slides  Script


  • English-German dictionary of deduction-related terms: [pdf]  [ps]

Course material from other lectures

Propositional logic, first-order logic, tableaux calculi

  • Melvin Fitting:
    First-Order Logic and Automated Theorem Proving.
    Springer-Verlag, New York, 1996.
  • Uwe Schöning:
    Logik für Informatiker.
    Spektrum Akademischer Verlag, 2000
  • Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh (Editors)
    Handbook of Satisfiability
    IOS Press, 2009
  • Uwe Schöning, Jacobo Torán:
    The Satisfiability Problem - Algorithms and Analyses
    Lehmanns Verlag, 2013

Termination, well-founded orderings, confluence, unification

  • Franz Baader and Tobias Nipkow:
    Term Rewriting and All That.
    Cambridge Univ. Press, 1998

Further readings

  • Leo Bachmair and Harald Ganzinger
    Resolution Theorem Proving, in "Handbook of Automated Reasoning", pages 19-99.
    Elsevier, 2001.
  • Robert Nieuwenhuis and Albert Rubio
    Paramodulation-Based Theorem Proving, in "Handbook of Automated Reasoning", pages 371-443.
    Elsevier, 2001.
  • Andreas Nonnengart and Christoph Weidenbach
    Computing small clause normal forms, in "Handbook of Automated Reasoning", pages 335-367.
    Elsevier, 2001.
  • Christoph Weidenbach
    Combining Superposition, Sorts and Splitting, in "Handbook of Automated Reasoning", pages 1965-2012.
    Elsevier, 2001.