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.
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.
External links
MIT press page
Undergraduate Texts in Mathematics
Graduate Studies in Mathematics
Hellenica World - Scientific Library
Retrieved from "http://en.wikipedia.org/"
All text is available under the terms of the GNU Free Documentation License
