# Handbook of Automated Reasoning

The Handbook of Automated Reasoning (.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("//upload.wikimedia.org/wikipedia/commons/6/65/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("//upload.wikimedia.org/wikipedia/commons/d/d6/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("//upload.wikimedia.org/wikipedia/commons/a/aa/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("//upload.wikimedia.org/wikipedia/commons/4/4c/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}ISBN0444508139, 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
### Volume 1
#### History

* 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.

#### Induction

* 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.

#### Implementation

* 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.