Lecture "Automated Reasoning" - Literature
[Most recent version of these lecture notes:
Course material Winter 2017/2018.]
- English-German dictionary of deduction-related terms: [pdf] [ps]
Propositional logic, first-order logic, tableaux calculi
- 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
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.
