Handbook of Automated Reasoning: Volume I
Published on 21. June 2001
Book
Hardback
996 pages
978-0-444-82949-8 (ISBN)
Description
This first volume of the "Handbook of Automated Reasoning" includes topics such as: the early history of automated deduction, classical logic - resolution theorem proving, and tableaux and related methods.
More details
Series
Language
English
Place of publication
United States
Publishing group
Elsevier Science & Technology
Target group
Professional and scholarly
Dimensions
Height: 240 mm
Width: 165 mm
Weight
2060 gr
ISBN-13
978-0-444-82949-8 (9780444829498)
Copyright in bibliographic data and cover images is held by Nielsen Book Services Limited or by the publishers or by their respective licensors: all rights reserved.
Schweitzer Classification
Persons
Content
Part I. History
1. The Early History of Automated Deduction (Martin Davis)
Part II. Classical Logic.
2. Resolution Theorem Proving (Leo Bachmair, Harald Ganzinger)
3. Tableaux and Related Methods (Reiner Haehnle)
4. The Inverse Method (Anatoli Degtyarev, Andrei Voronkov)
5. Normal Form Transformations (Matthias Baaz, Uwe Egly, Alexander Leitsch)
6. Computing Small Clause Normal Forms (Andreas Nonnengart, Christoph Weidenbach)
Part III. Equality and other theories.
7. Paramodulation-Based Theorem Proving (Robert Nieuwenhuis, Albert Rubio)
8. Unification Theory (Franz Baader, Wayne Snyder)
9. Rewriting (Nachum Dershowitz, David A. Plaisted)
10. Equality Reasoning in Sequent-Based Calculi (Anatoli Degtyarev, Andrei Voronkov)
11. Automated Reasoning in Geometry (Shang-Ching Chou, Xiao-Shan Gao)
12. Solving Numerical Constraints (Alexander Bockmayr, Volker Weispfenning)
Part IV. Induction.
13. The Automation of Proof by Mathematical Induction (Alan Bundy)
14. Inductionless Induction (Hubert Comon)
1. The Early History of Automated Deduction (Martin Davis)
Part II. Classical Logic.
2. Resolution Theorem Proving (Leo Bachmair, Harald Ganzinger)
3. Tableaux and Related Methods (Reiner Haehnle)
4. The Inverse Method (Anatoli Degtyarev, Andrei Voronkov)
5. Normal Form Transformations (Matthias Baaz, Uwe Egly, Alexander Leitsch)
6. Computing Small Clause Normal Forms (Andreas Nonnengart, Christoph Weidenbach)
Part III. Equality and other theories.
7. Paramodulation-Based Theorem Proving (Robert Nieuwenhuis, Albert Rubio)
8. Unification Theory (Franz Baader, Wayne Snyder)
9. Rewriting (Nachum Dershowitz, David A. Plaisted)
10. Equality Reasoning in Sequent-Based Calculi (Anatoli Degtyarev, Andrei Voronkov)
11. Automated Reasoning in Geometry (Shang-Ching Chou, Xiao-Shan Gao)
12. Solving Numerical Constraints (Alexander Bockmayr, Volker Weispfenning)
Part IV. Induction.
13. The Automation of Proof by Mathematical Induction (Alan Bundy)
14. Inductionless Induction (Hubert Comon)