Book description
Handbook of Automated Reasoning
Table of contents
- Cover image
- Title page
- Table of Contents
- Copyright page
- Preface
- List of contributors
- List of second readers
-
Volume 1.
- Part I: History
-
Part II: Classical Logic
-
Chapter 2: Resolution Theorem Proving
- 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
- Acknowledgments
- Index
- Chapter 3: Tableaux and Related Methods
- Chapter 4: The Inverse Method
- Chapter 5: Normal Form Transformations
- Chapter 6: Computing Small Clause Normal Forms
-
Chapter 2: Resolution Theorem Proving
-
Part III: Equality and other theories
- Chapter 7: Paramodulation-Based Theorem Proving
- Chapter 8: Unification Theory
- Chapter 9: Rewriting
-
Chapter 10: Equality Reasoning in Sequent-Based Calculi
- 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
- Calculi and inference rules
- Index
- Chapter 11: Automated Reasoning in Geometry
- Chapter 12: Solving Numerical Constraints
-
Part IV: Induction
-
Chapter 13: The Automation of Proof by Mathematical Induction
- 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
- Acknowledgments
- Main Index
- Name Index
- Chapter 14: Inductionless Induction
-
Chapter 13: The Automation of Proof by Mathematical Induction
-
Volume 2.
- Part V: Higher-order logic and logical frameworks
-
Part VI: Nonclassical logics
- Chapter 19: Nonmonotonic Reasoning: Towards Efficient Calculi and Implementations
-
Chapter 20: Automated Deduction for Many-Valued Logics
- 1 Introduction
- 2 What is a many-valued logic?
- 3 Classification of proof systems for many-valued logics
- 4 Signed logic: reasoning classically about finitely-valued logics
- 5 Signed resolution
- 6 An example
- 7 Optimization of transformation rules
- 8 Remarks on infinitely-valued logics
- Acknowledgments
- Index
- Chapter 21: Encoding Two-Valued Nonclassical Logics in Classical Logic
- Chapter 22: Connections in Nonclassical Logics
-
Part VII: Decidable classes and model building
- Chapter 23: Reasoning in Expressive Description Logics
-
Chapter 24: Model Checking
- 1 Introduction
- 2 Logical Languages, Expressiveness
- 3 Second Order Languages
- 4 Model Transformations and Properties
- 5 Equivalence reductions
- 6 Completeness
- 7 Decision Procedures
- 8 Basic Model Checking Algorithms
- 9 Modelling of Reactive Systems
- 10 Symbolic Model Checking
- 11 Partial Order Techniques
- 12 Bounded Model Checking
- 13 Abstractions
- 14 Compositionality and Modular Verification
- 15 Further Topics
- Acknowledgments
- List of symbols used in this chapter
- Index
- Chapter 25: Resolution Decision Procedures
-
Part VIII: Implementation
-
Chapter 26: Term Indexing
- 1 Introduction
- 2 Background
- 3 Data structures for representing terms and indexes
- 4 A common framework for indexing
- 5 Path indexing
- 6 Discrimination trees
- 7 Adaptive automata
- 8 Automata-driven indexing
- 9 Code trees
- 10 Substitution trees
- 11 Context trees
- 12 Unification factoring
- 13 Multiterm indexing
- 14 Issues in perfect filtering
- 15 Indexing modulo AC-theories
- 16 Elements of term indexing
- 17 Indexing in practice
- 18 Conclusion
- Index
- Chapter 27: Combining Superposition, Sorts and Splitting
-
Chapter 28: Model Elimination and Connection Tableau Procedures
- 1 Introduction
- 2 Clausal Tableaux and Connectedness
- 3 Further Structural Refinements of Clausal Tableaux
- 4 Global Pruning Methods in Model Elimination
- 5 Shortening of Proofs
- 6 Completeness of Connection Tableaux
- 7 Architectures of Model Elimination Implementations
- 8 Implementation of Refinements by Constraints
- 9 Experimental Results
- 10 Outlook
- Acknowledgments
- Index
-
Chapter 26: Term Indexing
- Concept index
Product information
- Title: Handbook of Automated Reasoning
- Author(s):
- Release date: June 2001
- Publisher(s): North Holland
- ISBN: 9780080532790
You might also like
book
Fisher Investments on Technology
The sixth installment of the Fisher Investments On series is a comprehensive guide to understanding and …
book
Knowledge Representation and Reasoning
Knowledge representation is at the very core of a radical idea for understanding intelligence. Instead of …
book
Generic Inference: A Unifying Theory for Automated Reasoning
This book provides a rigorous algebraic study of the most popular inference formalisms with a special …
book
The VimL Primer
Build on your editor's capabilities and tailor your editing experience with VimL, the powerful scripting language …