Handbook of Automated Reasoning
{{italic title}}
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
= Volume 1 =
;History
{{Ordered list |start=1
| Martin Davis. [http://www.cs.nyu.edu/faculty/davism/early.ps The Early History of Automated Deduction], pp. 3–15.
}}
;Classical Logic
{{Ordered list |start=2
|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
{{Ordered list |start=7
|Robert Nieuwenhuis, Alberto Rubio. Paramodulation-Based Theorem Proving, pp. 371–443.
|Franz Baader, Wayne Snyder. [http://lat.inf.tu-dresden.de/research/papers/2001/BaaderSnyderHandbook.ps.gz Unification Theory], pp. 445–532.
|Nachum Dershowitz, David Plaisted. [http://www.cs.tau.ac.il/~nachum/papers/hand-final.pdf 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
{{Ordered list |start=13
|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
{{Ordered list |start=15
|Peter B. Andrews. [http://gtps.math.cmu.edu/har15.ps.gz Classical Type Theory], pp. 965–1007.
|Gilles Dowek. [https://who.rocq.inria.fr/Gilles.Dowek/Publi/unification.ps Higher-Order Unification and Matching], pp. 1009–1062.
|Frank Pfenning. [https://www.cs.cmu.edu/~fp/papers/handbook01.pdf Logical Frameworks], pp. 1063–1147.
|Henk Barendregt, Herman Geuvers. [http://www.ncc.up.pt/~nam/aulas/0506/t_coq/barendregt01proofassistants.pdf Proof-Assistants Using Dependent Type Systems], pp. 1149–1238.
}}
;Nonclassical Logics
{{Ordered list |start=19
|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
{{Ordered list |start=23
|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
{{Ordered list |start=26
|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
- [https://mitpress.mit.edu/books/handbook-automated-reasoning-volume-1 MIT press page]
Category:2001 non-fiction books
Category:Handbooks and manuals