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
  1. Martin Davis. The Early History of Automated Deduction, pp. 3–15.
Classical Logic
  1. Leo Bachmair, Harald Ganzinger. Resolution Theorem Proving, pp. 19–99.
  2. Reiner Hähnle. Tableaux and Related Methods, pp. 100–178.
  3. Anatoli Degtyarev, Andrei Voronkov. The Inverse Method, pp. 179–272.
  4. Matthias Baaz, Uwe Egly, Alexander Leitsch. Normal Form Transformations, pp. 273–333.
  5. Andreas Nonnengart, Christoph Weidenbach. Computing Small Clause Normal Forms, pp. 335–367.
Equality and Other Theories
  1. Robert Nieuwenhuis, Alberto Rubio. Paramodulation-Based Theorem Proving, pp. 371–443.
  2. Franz Baader, Wayne Snyder. Unification Theory, pp. 445–532.
  3. Nachum Dershowitz, David Plaisted. Rewriting, pp. 535–610.
  4. Anatoli Degtyarev, Andrei Voronkov. Equality Reasoning in Sequent-Based Calculi, pp. 611–706.
  5. Shang-Ching Chou, Xiao-Shang Gao. Automated Reasoning in Geometry, pp. 707–749.
  6. Alexander Bockmayr, Volker Weispfenning. Solving Numerical Constraints, pp. 751–842.
Induction
  1. Alan Bundy. The Automation of Proof by Mathematical Induction, pp. 845–911.
  2. Hubert Comon. Inductionless Induction, pp. 913–962.

Volume 2

Higher-Order Logic and Logical Frameworks
  1. Peter B. Andrews. Classical Type Theory, pp. 965–1007.
  2. Gilles Dowek. Higher-Order Unification and Matching, pp. 1009–1062.
  3. Frank Pfenning. Logical Frameworks, pp. 1063–1147.
  4. Henk Barendregt, Herman Geuvers. Proof-Assistants Using Dependent Type Systems, pp. 1149–1238.
Nonclassical Logics
  1. Jürgen Dix, Ulrich Furbach, Ilkka Niemelä. Nonmonotonic Reasoning: Towards Efficient Calculi and Implementations, pp. 1241–1354.
  2. Matthias Baaz, Christian Fermüller, Gernot Salzer. Automated Deduction for Many-Valued Logics, pp. 1355–1402.
  3. Hans-Jürgen Ohlbach, Andreas Nonnengart, Maarten De Rijke, Dov Gabbay. Encoding Two-Valued Nonclassical Logics in Classical Logic, pp. 1403–1486.
  4. Arild Waaler. Connections in Nonclassical Logics, pp. 1487–1578.
Decidable Classes and Model Building
  1. Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Daniele Nardi. Reasoning in Expressive Description Logics, pp. 1581–1634.
  2. Edmund Clarke, Holger Schlingloff. Model Checking, pp. 1635–1790.
  3. Christian Fermüller, Alexander Leitsch, Ullrich Hustadt, Tanel Tammet. Resolution Decision Procedures, pp. 1791–1849.
Implementation
  1. I.V. Ramakrishnan, R.Sekar, Andrei Voronkov. Term Indexing, pp. 1853–1964.
  2. Christoph Weidenbach. Combining Superposition, Sorts and Splitting, pp. 1965–2013.
  3. Reinhold Letz, Gernot Stenz. Model Elimination and Connection Tableau Procedures, pp. 2015–2114.

External links

Categories