Handbook of Automated Reasoning

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

This article is issued from Wikipedia - version of the Friday, April 08, 2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.