book announcement

To: types@cis.upenn.edu
Subject: book announcement
From: Andrei Voronkov <voronkov@cs.man.ac.uk>
Date: Sat, 10 Nov 2001 10:45:46 +0000 (GMT)

Handbook of Automated Reasoning (in 2 volumes)

Alan Robinson and Andrei Voronkov (eds)
Elsevier Science and MIT Press, 2001

Web page: http://www.cs.man.ac.uk/~voronkov/handbook-ar/index.html

Table of contents:

---------------------------------------------------------

VOLUME I

The Early History of Automated Deduction
Martin Davis
pp. 3-15

Resolution Theorem Proving
Leo Bachmair and Harald Ganzinger
pp. 19-99

Tableaux and Related Methods
Reiner H"ahnle
pp. 100-178

The Inverse Method
Anatoli Degtyarev and Andrei Voronkov
pp. 179-272

Normal Form Transformations
Matthias Baaz, Uwe Egly, and Alexander Leitsch
pp. 273-333

Computing Small Clause Normal Forms
Andreas Nonnengart and Christoph Weidenbach
pp. 335-367

Paramodulation-Based Theorem Proving
Robert Nieuwenhuis and Albert Rubio
pp. 371-443

Unification Theory
Franz Baader and Wayne Snyder
pp. 445-532

Rewriting
Nachum Dershowitz and David A. Plaisted
pp. 535-610

Equality Reasoning in Sequent-Based Calculi
Anatoli Degtyarev and Andrei Voronkov
pp. 611-706

Automated Reasoning in Geometry
Shang-Ching Chou and Xiao-Shan Gao
pp. 707-749

Solving Numerical Constraints
Alexander Bockmayr and Volker Weispfenning
pp. 751-842

The Automation of Proof by Mathematical Induction
Alan Bundy
pp. 845-911

Inductionless Induction
Hubert Comon
pp. 913-962

---------------------------------------------------------

VOLUME II

Classical Type Theory
Peter B. Andrews
pp. 965-1007

Higher-Order Unification and Matching
Gilles Dowek
pp. 1009-1062

Logical Frameworks
Frank Pfenning
pp. 1063-1147

Proof-Assistants Using Dependent Type Systems
Henk Barendregt and Herman Geuvers
pp. 1149-1238

Nonmonotonic Reasoning: Towards Efficient Calculi and Implementations
J"urgen Dix, Ulrich Furbach, and Ilkka Niemel"a
pp. 1241-1354

Automated Deduction for Many-Valued Logics
Matthias Baaz, Christian G. Ferm"uller, and Gernot Salzer
pp. 1355-1402

Encoding Two-Valued Nonclassical Logics in Classical Logic
Hans J"urgen Ohlbach, Andreas Nonnengart, Maarten de Rijke, and Dov M. Gabbay
pp. 1403-1486

Connections in Nonclassical Logics
Arild Waaler
pp. 1487-1578

Reasoning in Expressive Description Logics
Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, and Daniele Nardi
pp. 1581-1634

Model Checking
Edmund M. Clarke and Bernd-Holger Schlingloff
pp. 1635-1790

Resolution Decision Procedures
Christian G. Ferm"uller, Alexander Leitsch, Ullrich Hustadt, and Tanel Tammet
pp. 1791-1849

Term Indexing
I.V. Ramakrishnan, R. Sekar, and Andrei Voronkov
pp. 1853-1964

Combining Superposition, Sorts and Splitting
Christoph Weidenbach
pp. 1965-2013

Model Elimination and Connection Tableau Procedures
Reinhold Letz and Gernot Stenz
pp. 2015-2114