LIMITED OFFER
Save 50% on book bundles
Immediately download your ebook while waiting for your print delivery. No promo code is needed.
Book sale: Save up to 25% on print and eBooks. No promo code needed.
Save up to 25% on print and eBooks.
Handbook of Automated Reasoning
1st Edition - June 21, 2001
Editors: Andrei Voronkov, Alan J.A. Robinson
Hardback ISBN:
9 7 8 - 0 - 4 4 4 - 8 2 9 4 9 - 8
Purchase Options
Part I. History
Chapter 1. The Early History of Automated Deduction (Martin Davis).
1. Presburger's Procedure.
2. Newell, Shaw & Simon, and H. Gelernter.
3. First-Order Logic.
Bibliography. Index.
Part II. Classical Logic.
Chapter 2. Resolution Theorem Proving (Leo Bachmair, Harald Ganzinger).
1. Introduction.
2. Preliminaries.
3. Standard Resolution.
4. A Framework for Saturation-Based Theorem Proving.
5. General Resolution.
6. Basic Resolution Strategies.
7. Refined Techniques for Defining Orderings and Selection Functions.
8. Global Theorem Proving Methods.
9. First-Order Resolution Methods.
10. Effective Saturation of First-Order Theories.
11. Concluding Remarks.
Bibliography. Index.
Chapter 3. Tableaux and Related Methods (Reiner Hähnle).
1. Introduction.
2. Preliminaries.
3. The Tableau Method.
4. Clause Tableaux.
5. Tableaux as a Framework.
6. Comparing Calculi.
7. Historical Remarks & Resources
Bibliography. Notation. Index.
Chapter 4. The Inverse Method (Anatoli Degtyarev, Andrei Voronkov).
1. Introduction.
2. Preliminaries.
3. Cooking classical logic.
4. Applying the recipe to nonclassical logics.
5. Naming and connections with resolution.
6. Season your meal: strategies and redundancies
7. Path calculi
8. Logics without the contraction rules
9. Conclusion
Bibliography. Index
Chapter 5. Normal Form Transformations (Matthias Baaz, Uwe Egly, Alexander Leitsch).
1. Introduction.
2. Notation and Definitions.
3. On the Concept of Normal Form.
4. Equivalence-Preserving Normal Forms.
5. Skolem Normal Form.
6. Conjunctive Normal Form.
7. Normal Forms in Nonclassical Logics.
8. Conclusion.
Bibliography. Index.
Chapter 6. Computing Small Clause Normal Forms (Andreas Nonnengart, Christoph Weidenbach).
1. Introduction.
2. Preliminaries.
3. Standard CNF-Translation.
4. Formula Renaming.
5. Skolemization.
6. Simplification.
7. Bibliographic Notes.
8. Implementation Notes.
Bibliography. Index.
Part III. Equality and other theories.
Chapter 7. Paramodulation-Based Theorem Proving (Robert Nieuwenhuis, Albert Rubio).
1. About this chapter.
2. Preliminaries.
3. Paramodulation calculi.
4. Saturation procedures.
5. Paramodulation with constrained clauses.
6. Paramodulation with built-in equational theories.
7. Symbolic constraint solving.
8. Extensions.
9. Perspectives.
Bibliography. Index.
Chapter 8. Unification Theory (Franz Baader, Wayne Snyder).
1. Introduction.
2. Syntactic unification.
3. Equational unification.
4. Syntactic methods for E-unification.
5. Semantic approaches to E-unification.
6. Combination of unification algorithms.
7. Further topics.
Bibliography. Index.
Chapter 9. Rewriting (Nachum Dershowitz, David A. Plaisted).
1. Introduction.
2. Terminology.
3. Normal Forms and Validity.
4. Termination Properties.
5. Church-Rosser Properties.
6. Completion.
7. Relativized Rewriting.
8. Equational Theorem Proving.
9. Conditional Rewriting.
10. Programming.
Bibliography. Index.
Chapter 10. Equality Reasoning in Sequent-Based Calculi (Anatoli Degtyarev, Andrei Voronkov).
1. Introduction.
2. Translation of logic with equality into logic without equality.
3. Free variable systems.
4. Early history.
5. Simultaneous rigid E-unification.
6. Incomplete procedures for rigid E-unification.
7. Sequent-based calculi and paramodulation.
8. Equality elimination.
9. Equality reasoning in nonclassical logics.
10. Conclusion and open problems.
Bibliography. Calculi and inference rules. Index.
Chapter 11. Automated Reasoning in Geometry (Shang-Ching Chou, Xiao-Shan Gao).
1. A history review of automated reasoning in geometry.
2. Algebraic approaches to automated reasoning in geometry.
3. Coordinate-free approaches to automated reasoning in geometry.
4. AI approaches to automated reasoning in geometry.
5. Final remarks. Bibliography. Index.
Chapter 12. Solving Numerical Constraints (Alexander Bockmayr, Volker Weispfenning).
1. Introduction.
2. Linear constraints over fields.
3. Linear diophantine constraints.
4. Non-linear constraints over continuous domains.
5. Non-linear diophantine constraints.
Bibliography. Index.
Part IV. Induction.
Chapter 13. The Automation of Proof by Mathematical Induction (Alan Bundy).
1. Introduction.
2. Induction Rules.
3. Recursive Definitions and Datatypes.
4. Inductive Proof Techniques.
5. Theoretical Limitations of Inductive Inference.
6. Special Search Control Problems.
7. Rippling.
8. The Productive Use of Failure.
9. Existential Theorems.
10. Interactive Theorem Proving.
11. Inductive Theorem Provers.
12. Conclusion. Bibliography.
Main Index. Name Index.
Chapter 14. Inductionless Induction (Hubert Comon).
1. Introduction.
2. Formal background.
3. General Setting of the Inductionless Induction Method.
4. Inductive completion methods.
5. Examples of Axiomatizations A from the Literature.
6. Ground Reducibility.
7. A comparison between inductive proofs and proofs by consistency.
Bibliography. Index.
Chapter 1. The Early History of Automated Deduction (Martin Davis).
1. Presburger's Procedure.
2. Newell, Shaw & Simon, and H. Gelernter.
3. First-Order Logic.
Bibliography. Index.
Part II. Classical Logic.
Chapter 2. Resolution Theorem Proving (Leo Bachmair, Harald Ganzinger).
1. Introduction.
2. Preliminaries.
3. Standard Resolution.
4. A Framework for Saturation-Based Theorem Proving.
5. General Resolution.
6. Basic Resolution Strategies.
7. Refined Techniques for Defining Orderings and Selection Functions.
8. Global Theorem Proving Methods.
9. First-Order Resolution Methods.
10. Effective Saturation of First-Order Theories.
11. Concluding Remarks.
Bibliography. Index.
Chapter 3. Tableaux and Related Methods (Reiner Hähnle).
1. Introduction.
2. Preliminaries.
3. The Tableau Method.
4. Clause Tableaux.
5. Tableaux as a Framework.
6. Comparing Calculi.
7. Historical Remarks & Resources
Bibliography. Notation. Index.
Chapter 4. The Inverse Method (Anatoli Degtyarev, Andrei Voronkov).
1. Introduction.
2. Preliminaries.
3. Cooking classical logic.
4. Applying the recipe to nonclassical logics.
5. Naming and connections with resolution.
6. Season your meal: strategies and redundancies
7. Path calculi
8. Logics without the contraction rules
9. Conclusion
Bibliography. Index
Chapter 5. Normal Form Transformations (Matthias Baaz, Uwe Egly, Alexander Leitsch).
1. Introduction.
2. Notation and Definitions.
3. On the Concept of Normal Form.
4. Equivalence-Preserving Normal Forms.
5. Skolem Normal Form.
6. Conjunctive Normal Form.
7. Normal Forms in Nonclassical Logics.
8. Conclusion.
Bibliography. Index.
Chapter 6. Computing Small Clause Normal Forms (Andreas Nonnengart, Christoph Weidenbach).
1. Introduction.
2. Preliminaries.
3. Standard CNF-Translation.
4. Formula Renaming.
5. Skolemization.
6. Simplification.
7. Bibliographic Notes.
8. Implementation Notes.
Bibliography. Index.
Part III. Equality and other theories.
Chapter 7. Paramodulation-Based Theorem Proving (Robert Nieuwenhuis, Albert Rubio).
1. About this chapter.
2. Preliminaries.
3. Paramodulation calculi.
4. Saturation procedures.
5. Paramodulation with constrained clauses.
6. Paramodulation with built-in equational theories.
7. Symbolic constraint solving.
8. Extensions.
9. Perspectives.
Bibliography. Index.
Chapter 8. Unification Theory (Franz Baader, Wayne Snyder).
1. Introduction.
2. Syntactic unification.
3. Equational unification.
4. Syntactic methods for E-unification.
5. Semantic approaches to E-unification.
6. Combination of unification algorithms.
7. Further topics.
Bibliography. Index.
Chapter 9. Rewriting (Nachum Dershowitz, David A. Plaisted).
1. Introduction.
2. Terminology.
3. Normal Forms and Validity.
4. Termination Properties.
5. Church-Rosser Properties.
6. Completion.
7. Relativized Rewriting.
8. Equational Theorem Proving.
9. Conditional Rewriting.
10. Programming.
Bibliography. Index.
Chapter 10. Equality Reasoning in Sequent-Based Calculi (Anatoli Degtyarev, Andrei Voronkov).
1. Introduction.
2. Translation of logic with equality into logic without equality.
3. Free variable systems.
4. Early history.
5. Simultaneous rigid E-unification.
6. Incomplete procedures for rigid E-unification.
7. Sequent-based calculi and paramodulation.
8. Equality elimination.
9. Equality reasoning in nonclassical logics.
10. Conclusion and open problems.
Bibliography. Calculi and inference rules. Index.
Chapter 11. Automated Reasoning in Geometry (Shang-Ching Chou, Xiao-Shan Gao).
1. A history review of automated reasoning in geometry.
2. Algebraic approaches to automated reasoning in geometry.
3. Coordinate-free approaches to automated reasoning in geometry.
4. AI approaches to automated reasoning in geometry.
5. Final remarks. Bibliography. Index.
Chapter 12. Solving Numerical Constraints (Alexander Bockmayr, Volker Weispfenning).
1. Introduction.
2. Linear constraints over fields.
3. Linear diophantine constraints.
4. Non-linear constraints over continuous domains.
5. Non-linear diophantine constraints.
Bibliography. Index.
Part IV. Induction.
Chapter 13. The Automation of Proof by Mathematical Induction (Alan Bundy).
1. Introduction.
2. Induction Rules.
3. Recursive Definitions and Datatypes.
4. Inductive Proof Techniques.
5. Theoretical Limitations of Inductive Inference.
6. Special Search Control Problems.
7. Rippling.
8. The Productive Use of Failure.
9. Existential Theorems.
10. Interactive Theorem Proving.
11. Inductive Theorem Provers.
12. Conclusion. Bibliography.
Main Index. Name Index.
Chapter 14. Inductionless Induction (Hubert Comon).
1. Introduction.
2. Formal background.
3. General Setting of the Inductionless Induction Method.
4. Inductive completion methods.
5. Examples of Axiomatizations A from the Literature.
6. Ground Reducibility.
7. A comparison between inductive proofs and proofs by consistency.
Bibliography. Index.
- No. of pages: 996
- Language: English
- Published: June 21, 2001
- Imprint: North Holland
- Hardback ISBN: 9780444829498
AV
Andrei Voronkov
Affiliations and expertise
University of Manchester, Computer Science Department, Oxford Road, Manchester, M13 9LP, UK.AR
Alan J.A. Robinson
Affiliations and expertise
96 Highland Avenue, Greenfield, Massachusetts, USA