A comprehensive resource on automated reasoning and its applications. Automated reasoning has matured into one of the most advanced areas of computer science. It is used in many areas of the field, including software and hardware verification, logic and functional programming, formal methods, knowledge representation, deductive databases, and artificial intelligence. This handbook presents an overview of the fundamental ideas, techniques, and methods in automated reasoning and its applications. The material covers both theory and implementation. In addition to traditional topics, the handbook contains material bridges the gap between automated reasoning and related areas. Examples of this include model checking, nonmonotonic reasoning, numerical constraints, description logics, and implementation of declarative programming languages. The book consists of eight parts.
After an overview of the early history of automated deduction, the areas covered are reasoning methods in first-order logic; equality and other built-in theories; methods of automated reasoning using induction; higher-order logic, which is used in a number of automatic and interactive proof-development systems; automated reasoning in nonclassical logics; decidable classes and model building; and implementation-related questions.

「Nielsen BookData」より

Automated reasoning has matured into one of the most advanced areas of computer science. It is used in many areas of the field, including software and hardware verification, logic and functional programming, formal methods, knowledge representation, deductive databases, and artificial intelligence. This handbook presents an overview of the fundamental ideas, techniques, and methods in automated reasoning and its applications. The material covers both theory and implementation. In addition to traditional topics, the book covers material that bridges the gap between automated reasoning and related areas. Examples include model checking, nonmonotonic reasoning, numerical constraints, description logics, and implementation of declarative programming languages. The book consists of eight parts.
After an overview of the early history of automated deduction, the areas covered are reasoning methods in first-order logic; equality and other built-in theories; methods of automated reasoning using induction; higher-order logic, which is used in a number of automatic and interactive proof-development systems; automated reasoning in nonclassical logics; decidable classes and model building; and implementation-related questions.

「Nielsen BookData」より

[目次]

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 Hahnle). 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.

「Nielsen BookData」より

[目次]

Part V. Higher-order logic and logical frameworks. Chapter 15. Classical Type Theory (Peter B. Andrews). 1. Introduction to type theory. 2. Metatheoretical foundations. 3. Proof search. 4. Conclusion. Bibliography. Index. Chapter 16. Higher-Order Unification and Matching (Gilles Dowek). 1. Type Theory and Other Set Theories. 2. Simply Typed -calculus. 3. Undecidability. 4. Huet's Algorithm. 5. Scopes Management. 6. Decidable Subcases. 7. Unification in -calculus with Dependent Types. Bibliography. Index. Chapter 17. Logical Frameworks (Frank Pfenning). 1. Introduction. 2. Abstract syntax. 3. Judgments and deductions. 4. Meta-programming and proof search. 5. Representing meta-theory. 6. Appendix: the simply-typed -calculus. 7. Appendix: the dependently typed -calculus. 8. Conclusion. Bibliography. Index. Chapter 18. Proof-Assistants Using Dependent Type Systems (Henk Barendregt, Herman Geuvers). 1. Proof checking. 2. Type-theoretic notions for proof checking. 3. Type systems for proof checking. 4. Proof-development in type systems. 5. Proof assistants. Bibliography. Index. Name index. Part VI. Nonclassical logics. Chapter 19. Nonmonotonic Reasoning: Towards Efficient Calculi and Implementations (Jurgen Dix, Ulrich Furbach, Ilkka Niemela). 1. General Nonmonotonic Logics. 2. Automating General Nonmonotonic Logics. 3. From Automated Reasoning to Disjunctive Logic Programming. 4. Nonmonotonic Semantics of Logic Programs. 5. Implementing Nonmonotonic Semantics. 6. Benchmarks. 7. Conclusion. Bibliography. Index. Chapter 20. Automated Deduction for Many-Valued Logics (Matthias Baaz, Christian G. Fermuller, Gernot Salzer). 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. Bibliography. Index. Chapter 21. Encoding Two-Valued Nonclassical Logics in Classical Logic (Hans Jurgen Ohlbach, Andreas Nonnengart, Maarten de Rijke, Dov M. Gabbay). 1. Introduction. 2. Background. 3. Encoding consequence relations. 4. The standard relational translation. 5. The functional translation. 6. The semi-functional translation. 7. Variations and alternatives. 8. Conclusion. Bibliography. Index. Chapter 22. Connections in Nonclassical Logics (Arild Waaler). 1. Introduction. 2. Prelude: Connections in classical first-order logic. 3. Labelled systems. 4. Propositional intuitionistic logic. 5. First--order intuitionistic logic. 6. Normal modal logics up to S4. 7. The S5 family. Bibliography. Index. Part VII. Decidable classes and model building. Chapter 23. Reasoning in Expressive Description Logics (Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Daniele Nardi). 1. Introduction. 2. Description Logics. 3. Description Logics and Propositional Dynamic Logics. 4. Unrestricted Model Reasoning. 5. Finite Model Reasoning. 6. Beyond Basic Description Logics. 7. Conclusions. Bibliography. Index. Chapter 24. Model Checking (Edmund M. Clarke, Bernd-Holger Schlingloff). 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. Bibliography. Index. Chapter 25. Resolution Decision Procedures (Christian G. Fermuller, Alexander Leitsch, Ullrich Hustadt, Tanel Tammet). 1. Introduction. 2. Notation and definitions. 3. Decision procedures based on ordering refinements. 4. Hyperresolution as decision procedure. 5. Resolution decision procedures for description logics. 6. Related work. Bibliography. Index. Part VIII. Implementation. Chapter 26. Term Indexing (R. Sekar, I.V. Ramakrishnan, Andrei Voronkov). 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. Bibliography. Index. Chapter 27. Combining Superposition, Sorts and Splitting (Christoph Weidenbach). 1. What This Chapter is (not) About. 2. Foundations. 3. A First Simple Prover. 4. Inference and Reduction Rules. 5. Global Design Decisions. Bibliography. A Links to Saturation Based Provers. Index. Chapter 28. Model Elimination and Connection Tableau Procedures (Reinhold Letz, Gernot Stenz). 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. Bibliography. Index. Concept index.

「Nielsen BookData」より

書名

Handbook of automated reasoning

著作者等

Robinson Alan J.A.
Robinson J.Alan
Voronkov A. (Andreĭ)
Voronkov Andrei
Robinson Alan