Handbook of Automated Reasoning

The Handbook of Automated Reasoning (ISBN 0444508139, 2128 pages) is a collection of survey articles on the field of automated reasoning. Published in June 2001 by MIT Press, it is edited by John Alan Robinson and Andrei Voronkov. Volume 1 describes methods for classical logic, first-order logic with equality and other theories, and induction. Volume 2 covers higher-order, non-classical and other kinds of logic.

Index

Leo Bachmair, Harald Ganzinger. Resolution Theorem Proving, pp. 19–99.
Reiner Hähnle. Tableaux and Related Methods, pp. 100–178.
Anatoli Degtyarev, Andrei Voronkov. The Inverse Method, pp. 179–272.
Matthias Baaz, Uwe Egly, Alexander Leitsch. Normal Form Transformations, pp. 273–333.
Andreas Nonnengart, Christoph Weidenbach. Computing Small Clause Normal Forms, pp. 335–367.

Robert Nieuwenhuis, Alberto Rubio. Paramodulation-Based Theorem Proving, pp. 371–443.
Franz Baader, Wayne Snyder. Unification Theory, pp. 445–532.
Nachum Dershowitz, David Plaisted. Rewriting, pp. 535–610.
Anatoli Degtyarev, Andrei Voronkov. Equality Reasoning in Sequent-Based Calculi, pp. 611–706.
Shang-Ching Chou, Xiao-Shang Gao. Automated Reasoning in Geometry, pp. 707–749.
Alexander Bockmayr, Volker Weispfenning. Solving Numerical Constraints, pp. 751–842.

Jürgen Dix, Ulrich Furbach, Ilkka Niemelä. Nonmonotonic Reasoning: Towards Efficient Calculi and Implementations, pp. 1241–1354.
Matthias Baaz, Christian Fermüller, Gernot Salzer. Automated Deduction for Many-Valued Logics, pp. 1355–1402.
Hans-Jürgen Ohlbach, Andreas Nonnengart, Maarten De Rijke, Dov Gabbay. Encoding Two-Valued Nonclassical Logics in Classical Logic, pp. 1403–1486.
Arild Waaler. Connections in Nonclassical Logics, pp. 1487–1578.

Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Daniele Nardi. Reasoning in Expressive Description Logics, pp. 1581–1634.
Edmund Clarke, Holger Schlingloff. Model Checking, pp. 1635–1790.
Christian Fermüller, Alexander Leitsch, Ullrich Hustadt, Tanel Tammet. Resolution Decision Procedures, pp. 1791–1849.

I.V. Ramakrishnan, R.Sekar, Andrei Voronkov. Term Indexing, pp. 1853–1964.
Christoph Weidenbach. Combining Superposition, Sorts and Splitting, pp. 1965–2013.
Reinhold Letz, Gernot Stenz. Model Elimination and Connection Tableau Procedures, pp. 2015–2114.