Handbook of Automated Reasoning

Part V. Higher-order logic and logical frameworks.<br><br><br>Chapter 15. Classical Type Theory (Peter B. Andrews).<br><br><br>1. Introduction to type theory.<br> <br>2. Metatheoretical foundations.<br> <br>3. Proof search.<br> <br>4. Conclusion.<br> <br>Bibliography. Index.<br> <br><br>Chapter 16. Higher-Order Unification and Matching (Gilles Dowek).<br><br><br>1. Type Theory and Other Set Theories.<br> <br>2. Simply Typed &lgr;-calculus.<br> <br>3. Undecidability.<br> <br>4. Huet's Algorithm.<br> <br>5. Scopes Management.<br> <br>6. Decidable Subcases.<br> <br>7. Unification in &lgr;-calculus with Dependent Types.<br> <br>Bibliography. Index.<br> <br><br>Chapter 17. Logical Frameworks (Frank Pfenning).<br><br><br>1. Introduction.<br> <br>2. Abstract syntax.<br> <br>3. Judgments and deductions.<br> <br>4. Meta-programming and proof search.<br> <br>5. Representing meta-theory.<br> <br>6. Appendix: the simply-typed &lgr;-calculus.<br> <br>7. Appendix: the dependently typed &lgr;-calculus.<br> <br>8. Conclusion.<br> <br>Bibliography. Index.<br> <br><br>Chapter 18. Proof-Assistants Using Dependent Type Systems (Henk Barendregt, Herman Geuvers).<br><br><br>1. Proof checking.<br> <br>2. Type-theoretic notions for proof checking.<br> <br>3. Type systems for proof checking.<br> <br>4. Proof-development in type systems.<br> <br>5. Proof assistants.<br> <br>Bibliography. Index. Name index.<br> <br><br>Part VI. Nonclassical logics.<br><br><br>Chapter 19. Nonmonotonic Reasoning: Towards Efficient Calculi<br>and Implementations (Jurgen Dix, Ulrich Furbach, Ilkka Niemela).<br><br><br>1. General Nonmonotonic Logics.<br> <br>2. Automating General Nonmonotonic Logics.<br><br>3. From Automated Reasoning to Disjunctive Logic Programming.<br> <br>4. Nonmonotonic Semantics of Logic Programs.<br> <br>5. Implementing Nonmonotonic Semantics.<br> <br>6. Benchmarks.<br> <br>7. Conclusion.<br> <br>Bibliography. Index.<br> <br><br>Chapter 20. Automated Deduction for Many-Valued Logics <br>(Matthias Baaz, Christian G. Fermuller, Gernot Salzer).<br><br><br>1. Introduction.<br> <br>2. What is a many-valued logic?<br> <br>3. Classification of proof systems for many-valued logics.<br> <br>4. Signed logic: reasoning classically about finitely-valued logics.<br> <br>5. Signed resolution.<br> <br>6. An example.<br> <br>7. Optimization of transformation rules.<br> <br>8. Remarks on infinitely-valued logics.<br> <br>Bibliography. Index.<br> <br><br>Chapter 21. Encoding Two-Valued Nonclassical Logics in Classical Logic (Hans Jurgen Ohlbach, Andreas Nonnengart, Maarten de Rijke, Dov M. Gabbay).<br><br><br>1. Introduction.<br> <br>2. Background.<br> <br>3. Encoding consequence relations.<br> <br>4. The standard relational translation.<br> <br>5. The functional translation.<br> <br>6. The semi-functional translation.<br> <br>7. Variations and alternatives.<br> <br>8. Conclusion.<br> <br>Bibliography. Index.<br> <br><br>Chapter 22. Connections in Nonclassical Logics (Arild Waaler).<br><br><br>1. Introduction.<br> <br>2. Prelude: Connections in classical first-order logic.<br> <br>3. Labelled systems.<br> <br>4. Propositional intuitionistic logic.<br> <br>5. First--order intuitionistic logic.<br> <br>6. Normal modal logics up to S4.<br> <br>7. The S5 family.<br> <br>Bibliography. Index.<br> <br><br>Part VII. Decidable classes and model building.<br><br><br>Chapter 23. Reasoning in Expressive Description Logics (Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Daniele Nardi).<br><br><br>1. Introduction.<br> <br>2. Description Logics.<br> <br>3. Description Logics and Propositional Dynamic Logics.<br> <br>4. Unrestricted Model Reasoning.<br> <br>5. Finite Model Reasoning.<br> <br>6. Beyond Basic Description Logics.<br> <br>7. Conclusions.<br> <br>Bibliography. Index.<br> <br><br>Chapter 24. Model Checking (Edmund M. Clarke, Bernd-Holger Schlingloff).<br><br><br>1. Introduction.<br> <br>2. Logical Languages, Expressiveness.<br> <br>3. Second Order Languages.<br> <br>4. Model Transformations and Properties.<br> <br>5. Equivalence reductions.<br> <br>6. Completeness.<br> <br>7. Decision Procedures.<br> <br>8. Basic Model Checking Algorithms.<br> <br>9. Modelling of Reactive Systems.<br> <br>10. Symbolic Model Checking.<br><br>11. Partial Order Techniques.<br> <br>12. Bounded Model Checking.<br> <br>13. Abstractions.<br> <br>14. Compositionality and Modular Verification.<br> <br>15. Further Topics.<br> <br>Bibliography. Index.<br> <br><br>Chapter 25. Resolution Decision Procedures (Christian G. Fermuller, Alexander Leitsch, Ullrich Hustadt, Tanel Tammet).<br><br><br>1. Introduction.<br> <br>2. Notation and definitions.<br> <br>3. Decision procedures based on ordering refinements.<br> <br>4. Hyperresolution as decision procedure.<br> <br>5. Resolution decision procedures for description logics.<br> <br>6. Related work.<br><br>Bibliography. Index.<br> <br><br>Part VIII. Implementation.<br><br>Chapter 26. Term Indexing (R. Sekar, I.V. Ramakrishnan, Andrei Voronkov).<br><br><br>1. Introduction.<br> <br>2. Background.<br> <br>3. Data structures for representing terms and indexes.<br> <br>4. A common framework for indexing.<br> <br>5. Path indexing.<br> <br>6. Discrimination trees.<br> <br>7. Adaptive automata.<br> <br>8. Automata-driven indexing.<br> <br>9. Code trees.<br> <br>10. Substitution trees.<br> <br>11. Context trees.<br> <br>12. Unification factoring.<br> <br>13. Multiterm indexing.<br> <br>14. Issues in perfect filtering.<br> <br>15. Indexing modulo AC-theories.<br> <br>16. Elements of term indexing.<br> <br>17. Indexing in practice.<br> <br>18. Conclusion.<br> <br>Bibliography. Index.<br> <br><br>Chapter 27. Combining Superposition, Sorts and Splitting (Christoph Weidenbach).<br><br><br>1. What This Chapter is (not) About.<br> <br>2. Foundations.<br> <br>3. A First Simple Prover.<br> <br>4. Inference and Reduction Rules.<br> <br>5. Global Design Decisions.<br> <br>Bibliography. A Links to Saturation Based Provers. Index.<br> <br><br>Chapter 28. Model Elimination and Connection Tableau Procedures <br>(Reinhold Letz, Gernot Stenz).<br><br>1. Introduction.<br> <br>2. Clausal Tableaux and Connectedness.<br> <br>3. Further Structural Refinements of Clausal Tableaux.<br> <br>4. Global Pruning Methods in Model Elimination.<br> <br>5. Shortening of Proofs.<br> <br>6. Completeness of Connection Tableaux.<br> <br>7. Architectures of Model Elimination Implementations.<br> <br>8. Implementation of Refinements by Constraints.<br> <br>9. Experimental Results.<br> <br>10. Outlook.<br> <br>Bibliography. Index. Concept index. <br>