To order this title, and for more information, click here
Edited By Alan Robinson, 96 Highland Avenue, Greenfield, Massachusetts, USA Andrei Voronkov, University of Manchester, Computer Science Department, Oxford Road, Manchester, M13 9LP, UK.
Contents 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.
Books and book related electronic products are priced in US dollars (USD), euro (EUR), and Great Britain Pounds (GBP). USD prices apply to the Americas and Asia Pacific. EUR prices apply in Europe and the Middle East. GBP prices apply to the UK and all other countries.
Home | Elsevier Sites | Privacy Policy | Terms and Conditions | Feedback | Site Map | A Reed Elsevier Company