You are previewing Handbook of Automated Reasoning.
O'Reilly logo
Handbook of Automated Reasoning

Book Description

Handbook of Automated Reasoning

Table of Contents

  1. Cover image
  2. Title page
  3. Table of Contents
  4. Copyright page
  5. Preface
  6. List of contributors
  7. List of second readers
  8. Volume 1.
    1. Part I: History
      1. Chapter 1: The Early History of Automated Deduction: Dedicated to the memory of Hao Wang
        1. 1 Presburger's Procedure
        2. 2 Newell, Shaw & Simon, and H. Gelernter
        3. 3 First-Order Logic
        4. Index
    2. Part II: Classical Logic
      1. Chapter 2: Resolution Theorem Proving
        1. 1 Introduction
        2. 2 Preliminaries
        3. 3 Standard Resolution
        4. 4 A Framework for Saturation-Based Theorem Proving
        5. 5 General Resolution
        6. 6 Basic Resolution Strategies
        7. 7 Refined Techniques for Defining Orderings and Selection Functions
        8. 8 Global Theorem Proving Methods
        9. 9 First-Order Resolution Methods
        10. 10 Effective Saturation of First-Order Theories
        11. 11 Concluding Remarks
        12. Acknowledgments
        13. Index
      2. Chapter 3: Tableaux and Related Methods
        1. 1 Introduction
        2. 2 Preliminaries
        3. 3 The Tableau Method
        4. 4 Clause Tableaux
        5. 5 Tableaux as a Framework
        6. 6 Comparing Calculi
        7. 7 Historical Remarks & Resources
        8. Acknowledgments
        9. Notation
        10. Index
      3. Chapter 4: The Inverse Method
        1. 1 Introduction
        2. 2 Preliminaries
        3. 3 Cooking classical logic
        4. 4 Applying the recipe to nonclassical logics
        5. 5 Naming and connections with resolution
        6. 6 Season your meal: strategies and redundancies
        7. 7 Path calculi
        8. 8 Logics without the contraction rules
        9. 9 Conclusion
        10. Acknowledgments
        11. Index
      4. Chapter 5: Normal Form Transformations
        1. 1 Introduction
        2. 2 Notation and Definitions
        3. 3 On the Concept of Normal Form
        4. 4 Equivalence-Preserving Normal Forms
        5. 5 Skolem Normal Form
        6. 6 Conjunctive Normal Form
        7. 7 Normal Forms in Nonclassical Logics
        8. 8 Conclusion
        9. Acknowledgments
        10. Index
      5. Chapter 6: Computing Small Clause Normal Forms
        1. 1 Introduction
        2. 2 Preliminaries
        3. 3 Standard CNF-Translation
        4. 4 Formula Renaming
        5. 5 Skolemization
        6. 6 Simplification
        7. 7 Bibliographic Notes
        8. 8 Implementation Notes
        9. Acknowledgments
        10. Index
    3. Part III: Equality and other theories
      1. Chapter 7: Paramodulation-Based Theorem Proving
        1. 1 About this chapter
        2. 2 Preliminaries
        3. 3 Paramodulation calculi
        4. 4 Saturation procedures
        5. 5 Paramodulation with constrained clauses
        6. 6 Paramodulation with built-in equational theories
        7. 7 Symbolic constraint solving
        8. 8 Extensions
        9. 9 Perspectives
        10. Index
      2. Chapter 8: Unification Theory
        1. 1 Introduction
        2. 2 Syntactic unification
        3. 3 Equational unification
        4. 4 Syntactic methods for <span xmlns="http://www.w3.org/1999/xhtml" xmlns:epub="http://www.idpf.org/2007/ops" xmlns:mml="http://www.w3.org/1998/Math/MathML" class="italic">E</span>-unification-unification
        5. 4.4 Strategies and refinements of basic narrowing
        6. 5 Semantic approaches to <span xmlns="http://www.w3.org/1999/xhtml" xmlns:epub="http://www.idpf.org/2007/ops" xmlns:mml="http://www.w3.org/1998/Math/MathML" class="italic">E</span>-unification-unification
        7. 6 Combination of unification algorithms
        8. 7 Further topics
        9. Index
      3. Chapter 9: Rewriting
        1. 1 Introduction
        2. 2 Terminology
        3. 3 Normal Forms and Validity
        4. 4 Termination Properties
        5. 5 Church-Rosser Properties
        6. 6 Completion
        7. 7 Relativized Rewriting
        8. 8 Equational Theorem Proving
        9. 9 Conditional Rewriting
        10. 10 Programming
        11. Acknowledgments
        12. Index
      4. Chapter 10: Equality Reasoning in Sequent-Based Calculi
        1. 1 Introduction
        2. 2 Translation of logic with equality into logic without equality
        3. 3 Free variable systems
        4. 4 Early history
        5. 5 Simultaneous rigid <span xmlns="http://www.w3.org/1999/xhtml" xmlns:epub="http://www.idpf.org/2007/ops" xmlns:mml="http://www.w3.org/1998/Math/MathML" class="italic">E</span>-unification-unification
        6. 6 Incomplete procedures for rigid <span xmlns="http://www.w3.org/1999/xhtml" xmlns:epub="http://www.idpf.org/2007/ops" xmlns:mml="http://www.w3.org/1998/Math/MathML" class="italic">E</span>-unification-unification
        7. 7 Sequent-based calculi and paramodulation
        8. 8 Equality elimination
        9. 9 Equality reasoning in nonclassical logics
        10. 10 Conclusion and open problems
        11. Calculi and inference rules
        12. Index
      5. Chapter 11: Automated Reasoning in Geometry
        1. 1 A history review of automated reasoning in geometry
        2. 2 Algebraic approaches to automated reasoning in geometry
        3. 3 Coordinate-free approaches to automated reasoning in geometry
        4. 4 AI approaches to automated reasoning in geometry
        5. 5 Final remarks
        6. Acknowledgments
        7. Index
      6. Chapter 12: Solving Numerical Constraints
        1. 1 Introduction
        2. 2 Linear constraints over fields
        3. 3 Linear diophantine constraints
        4. 4 Non-linear constraints over continuous domains
        5. 5 Non-linear diophantine constraints
        6. Acknowledgments
        7. Index
    4. Part IV: Induction
      1. Chapter 13: The Automation of Proof by Mathematical Induction
        1. 1 Introduction
        2. 2 Induction Rules
        3. 3 Recursive Definitions and Datatypes
        4. 4 Inductive Proof Techniques
        5. 5 Theoretical Limitations of Inductive Inference
        6. 6 Special Search Control Problems
        7. 7 Rippling
        8. 8 The Productive Use of Failure
        9. 9 Existential Theorems
        10. 10 Interactive Theorem Proving
        11. 11 Inductive Theorem Provers
        12. 12 Conclusion
        13. Acknowledgments
        14. Main Index
        15. Name Index
      2. Chapter 14: Inductionless Induction
        1. 1 Introduction
        2. 2 Formal background
        3. 3 General Setting of the Inductionless Induction Method
        4. 4 Inductive completion methods
        5. 5 Examples of Axiomatizations A from the Literature
        6. 6 Ground Reducibility
        7. 7 A comparison between inductive proofs and proofs by consistency
        8. Acknowledgments
        9. Index
  9. Volume 2.
    1. Part V: Higher-order logic and logical frameworks
      1. Chapter 15: Classical Type Theory
        1. Preface
        2. 1 Introduction to type theory
        3. 2 Metatheoretical foundations
        4. 3 Proof search
        5. 4 Conclusion
        6. Acknowledgments
        7. Index
      2. Chapter 16: Higher-Order Unification and Matching
        1. 1 Type Theory and Other Set Theories
        2. 2 Simply Typed λ-calculus
        3. 3 Undecidability
        4. 4 Huet's Algorithm
        5. 5 Scopes Management
        6. 6 Decidable Subcases
        7. 7 Unification in λ-calculus with Dependent Types
        8. Acknowledgments
        9. Index
      3. Chapter 17: Logical Frameworks
        1. 1 Introduction
        2. 2 Abstract syntax
        3. 3 Judgments and deductions
        4. 4 Meta-programming and proof search
        5. 5 Representing meta-theory
        6. 6 Appendix: the simply-typed λ-calculus
        7. 7 Appendix: the dependently typed λ-calculus
        8. 8 Conclusion
        9. Index
      4. Chapter 18: Proof-Assistants Using Dependent Type Systems
        1. 1 Proof checking
        2. 2 Type-theoretic notions for proof checking
        3. 3 Type systems for proof checking
        4. 4 Proof-development in type systems
        5. 5 Proof assistants
        6. Acknowledgments
        7. Index
        8. Name index
    2. Part VI: Nonclassical logics
      1. Chapter 19: Nonmonotonic Reasoning: Towards Efficient Calculi and Implementations
        1. Preface
        2. Overall Organization
        3. 1 General Nonmonotonic Logics
        4. 2 Automating General Nonmonotonic Logics
        5. 3 From Automated Reasoning to Disjunctive Logic Programming
        6. 4 Nonmonotonic Semantics of Logic Programs
        7. 5 Implementing Nonmonotonic Semantics
        8. 6 Benchmarks
        9. 7 Conclusion
        10. Index
      2. Chapter 20: Automated Deduction for Many-Valued Logics
        1. 1 Introduction
        2. 2 What is a many-valued logic?
        3. 3 Classification of proof systems for many-valued logics
        4. 4 Signed logic: reasoning classically about finitely-valued logics
        5. 5 Signed resolution
        6. 6 An example
        7. 7 Optimization of transformation rules
        8. 8 Remarks on infinitely-valued logics
        9. Acknowledgments
        10. Index
      3. Chapter 21: Encoding Two-Valued Nonclassical Logics in Classical Logic
        1. 1 Introduction
        2. 2 Background
        3. 3 Encoding consequence relations
        4. 4 The standard relational translation
        5. 5 The functional translation
        6. 6. The semi-functional translation
        7. 7 Variations and alternatives
        8. 8 Conclusion
        9. Index
      4. Chapter 22: Connections in Nonclassical Logics
        1. 1 Introduction
        2. 2 Prelude: Connections in classical first–order logic
        3. 3 Labelled systems
        4. 4 Propositional intuitionistic logic
        5. 5 First-order intuitionistic logic
        6. 6 Normal modal logics up to S4
        7. 7 The S5 family
        8. Acknowledgments
        9. Index
    3. Part VII: Decidable classes and model building
      1. Chapter 23: Reasoning in Expressive Description Logics
        1. 1 Introduction
        2. 2 Description Logics
        3. 3 Description Logics and Propositional Dynamic Logics
        4. 4 Unrestricted Model Reasoning
        5. 5 Finite Model Reasoning
        6. 6 Beyond Basic Description Logics
        7. 7 Conclusions
        8. Index
      2. Chapter 24: Model Checking
        1. 1 Introduction
        2. 2 Logical Languages, Expressiveness
        3. 3 Second Order Languages
        4. 4 Model Transformations and Properties
        5. 5 Equivalence reductions
        6. 6 Completeness
        7. 7 Decision Procedures
        8. 8 Basic Model Checking Algorithms
        9. 9 Modelling of Reactive Systems
        10. 10 Symbolic Model Checking
        11. 11 Partial Order Techniques
        12. 12 Bounded Model Checking
        13. 13 Abstractions
        14. 14 Compositionality and Modular Verification
        15. 15 Further Topics
        16. Acknowledgments
        17. List of symbols used in this chapter
        18. Index
      3. Chapter 25: Resolution Decision Procedures
        1. 1 Introduction
        2. 2 Notation and definitions
        3. 3 Decision procedures based on ordering refinements
        4. 4 Hyperresolution as decision procedure
        5. 5 Resolution decision procedures for description logics
        6. 6 Related work
        7. Index
    4. Part VIII: Implementation
      1. Chapter 26: Term Indexing
        1. 1 Introduction
        2. 2 Background
        3. 3 Data structures for representing terms and indexes
        4. 4 A common framework for indexing
        5. 5 Path indexing
        6. 6 Discrimination trees
        7. 7 Adaptive automata
        8. 8 Automata-driven indexing
        9. 9 Code trees
        10. 10 Substitution trees
        11. 11 Context trees
        12. 12 Unification factoring
        13. 13 Multiterm indexing
        14. 14 Issues in perfect filtering
        15. 15 Indexing modulo AC-theories
        16. 16 Elements of term indexing
        17. 17 Indexing in practice
        18. 18 Conclusion
        19. Index
      2. Chapter 27: Combining Superposition, Sorts and Splitting
        1. 1 What This Chapter is (not) About
        2. 2 Foundations
        3. 3 A First Simple Prover
        4. 4 Inference and Reduction Rules
        5. 5 Global Design Decisions
        6. Appendix
        7. Index
      3. Chapter 28: Model Elimination and Connection Tableau Procedures
        1. 1 Introduction
        2. 2 Clausal Tableaux and Connectedness
        3. 3 Further Structural Refinements of Clausal Tableaux
        4. 4 Global Pruning Methods in Model Elimination
        5. 5 Shortening of Proofs
        6. 6 Completeness of Connection Tableaux
        7. 7 Architectures of Model Elimination Implementations
        8. 8 Implementation of Refinements by Constraints
        9. 9 Experimental Results
        10. 10 Outlook
        11. Acknowledgments
        12. Index
  10. Concept index