Incremental lecture notes:
Complete lecture notes [PDF]
Complete slides [PDF]
Slides, lecture notes, exercises, exam sheets
Winter 2010/2021 |
Winter 2019/2020 |
Winter 2018/2019 |
Winter 2017/2018 |
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.
Franz Baader and Tobias Nipkow:
Term Rewriting and All That.
Cambridge Univ. Press,
1998.
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.
Christoph Weidenbach:
Automated Reasoning (Chapter 2).
Textbook draft, available for registered participants in the lecture Nextcloud
(same link as for the online session recordings),
2021.
Leo Bachmair and Harald Ganzinger:
Resolution theorem proving,
in Handbook of Automated Reasoning, pages 19-99.
Elsevier,
2001.
Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh (eds.):
Handbook of Satisfiability.
IOS Press,
2009.
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.