Most recent version of these lecture notes: Course material Winter 2017/2018.
English-German dictionary of deduction-related terms [PDF] [PS]
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.