Math gifts

- Art Gallery -

The Handbook of Automated Reasoning (ISBN 0444508139, 2128 pages) is a collection of survey articles on the field of automated reasoning. Published on 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.

Volume 1


Martin Davis. The Early History of Automated Deduction, pp. 3–15.

Classical Logic

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.

Equality and Other Theories

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.


Alan Bundy. The Automation of Proof by Mathematical Induction, pp. 845–911.
Hubert Comon. Inductionless Induction, pp. 913–962.

Volume 2

Higher-Order Logic and Logical Frameworks

Peter B. Andrews. Classical Type Theory, pp. 965–1007.
Gilles Dowek. Higher-Order Unification and Matching, pp. 1009–1062.
Frank Pfenning. Logical Frameworks, pp. 1063–1147.
Henk Barendregt, Herman Geuvers. Proof-Assistants Using Dependent Type Systems, pp. 1149–1238.

Nonclassical Logics

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.

Decidable Classes and Model Building

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.

External links

MIT press page

Undergraduate Texts in Mathematics

Graduate Texts in Mathematics

Graduate Studies in Mathematics

Mathematics Encyclopedia



Hellenica World - Scientific Library

Retrieved from ""
All text is available under the terms of the GNU Free Documentation License