Incremental lecture notes:
Complete lecture notes [PDF]
Complete slides [PDF]
Slides, lecture notes, exercises, exam sheets
Winter 2016/2017 |
Winter 2015/2016 |
Winter 2014/2015 |
Winter 2013/2014 |
Summer 2012 |
Summer 2011 |
Summer 2010 |
Summer 2008 |
Summer 2006 |
Summer 2004
Regrettably, much of the material of the lecture (e.g., optimized normal form transformations and conflict-driven clause learning from Sect. 2 and most of Sect. 3, 5, and 6) is not contained in any current textbook. If you are interested in more information on these topics, you have to consult handbook or journal articles. Note that these are usually not written on a beginner's level.
Melvin Fitting:
First-Order Logic and Automated Theorem Proving.
Springer-Verlag, New York,
1996.
Michael Huth and Mark Ryan:
Logic in Computer Science: Modelling and Reasoning about Systems.
Cambridge Univ. Press,
2000.
Uwe Schöning:
Logik für Informatiker.
Spektrum Akademischer Verlag,
2000.
Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh (eds.):
Handbook of Satisfiability.
IOS Press,
2009.
Franz Baader and Tobias Nipkow:
Term Rewriting and All That.
Cambridge Univ. Press,
1998.
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.