Automated Reasoning – Suggested Readings

Reformatted slides

Most recent version of these lecture notes: Course material Winter 2017/2018.

Previous lectures in this series

Slides, exercises, exam sheets
Summer 2010 | Summer 2008 | Summer 2006 | Summer 2004


English-German dictionary of deduction-related terms [PDF] [PS]

Further reading

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.

Previous | Up | Next
Uwe Waldmann <>, 2011-07-19.
Imprint | Data Protection