# Handbook of Automated Reasoning, Volume II

## 1st Edition

**Editors:**Alan Robinson Andrei Voronkov

**Hardcover ISBN:**9780444508126

**eBook ISBN:**9780080929699

**Imprint:**North Holland

**Published Date:**21st June 2001

**Page Count:**1188

**View all volumes in this series:**Handbook of Automated Reasoning

## Table of Contents

Part V. Higher-order logic and logical frameworks.

Chapter 15. Classical Type Theory (Peter B. Andrews).

- Introduction to type theory.

- Metatheoretical foundations.

- Proof search.

- Conclusion.

Bibliography. Index.

Chapter 16. Higher-Order Unification and Matching (Gilles Dowek).

- Type Theory and Other Set Theories.

- Simply Typed &lgr;-calculus.

- Undecidability.

- Huet's Algorithm.

- Scopes Management.

- Decidable Subcases.

- Unification in &lgr;-calculus with Dependent Types.

Bibliography. Index.

Chapter 17. Logical Frameworks (Frank Pfenning).

- Introduction.

- Abstract syntax.

- Judgments and deductions.

- Meta-programming and proof search.

- Representing meta-theory.

- Appendix: the simply-typed &lgr;-calculus.

- Appendix: the dependently typed &lgr;-calculus.

- Conclusion.

Bibliography. Index.

Chapter 18. Proof-Assistants Using Dependent Type Systems (Henk Barendregt, Herman Geuvers).

- Proof checking.

- Type-theoretic notions for proof checking.

- Type systems for proof checking.

- Proof-development in type systems.

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

- General Nonmonotonic Logics.

- Automating General Nonmonotonic Logics.
- From Automated Reasoning to Disjunctive Logic Programming.

- Nonmonotonic Semantics of Logic Programs.

- Implementing Nonmonotonic Semantics.

- Benchmarks.

- Conclusion.

Bibliography. Index.

Chapter 20. Automated Deduction for Many-Valued Logics
(Matthias Baaz, Christian G. Fermuller, Gernot Salzer).

- Introduction.

- What is a many-valued logic?

- Classification of proof systems for many-valued logics.

- Signed logic: reasoning classically about finitely-valued logics.

- Signed resolution.

- An example.

- Optimization of transformation rules.

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

- Introduction.

- Background.

- Encoding consequence relations.

- The standard relational translation.

- The functional translation.

- The semi-functional translation.

- Variations and alternatives.

- Conclusion.

Bibliography. Index.

Chapter 22. Connections in Nonclassical Logics (Arild Waaler).

- Introduction.

- Prelude: Connections in classical first-order logic.

- Labelled systems.

- Propositional intuitionistic logic.

- First--order intuitionistic logic.

- Normal modal logics up to S4.

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

- Introduction.

- Description Logics.

- Description Logics and Propositional Dynamic Logics.

- Unrestricted Model Reasoning.

- Finite Model Reasoning.

- Beyond Basic Description Logics.

- Conclusions.

Bibliography. Index.

Chapter 24. Model Checking (Edmund M. Clarke, Bernd-Holger Schlingloff).

- Introduction.

- Logical Languages, Expressiveness.

- Second Order Languages.

- Model Transformations and Properties.

- Equivalence reductions.

- Completeness.

- Decision Procedures.

- Basic Model Checking Algorithms.

- Modelling of Reactive Systems.

- Symbolic Model Checking.
- Partial Order Techniques.

- Bounded Model Checking.

- Abstractions.

- Compositionality and Modular Verification.

- Further Topics.

Bibliography. Index.

Chapter 25. Resolution Decision Procedures (Christian G. Fermuller, Alexander Leitsch, Ullrich Hustadt, Tanel Tammet).

- Introduction.

- Notation and definitions.

- Decision procedures based on ordering refinements.

- Hyperresolution as decision procedure.

- Resolution decision procedures for description logics.

- Related work.

Bibliography. Index.

Part VIII. Implementation.

Chapter 26. Term Indexing (R. Sekar, I.V. Ramakrishnan, Andrei Voronkov).

- Introduction.

- Background.

- Data structures for representing terms and indexes.

- A common framework for indexing.

- Path indexing.

- Discrimination trees.

- Adaptive automata.

- Automata-driven indexing.

- Code trees.

- Substitution trees.

- Context trees.

- Unification factoring.

- Multiterm indexing.

- Issues in perfect filtering.

- Indexing modulo AC-theories.

- Elements of term indexing.

- Indexing in practice.

- Conclusion.

Bibliography. Index.

Chapter 27. Combining Superposition, Sorts and Splitting (Christoph Weidenbach).

- What This Chapter is (not) About.

- Foundations.

- A First Simple Prover.

- Inference and Reduction Rules.

- Global Design Decisions.

Bibliography. A Links to Saturation Based Provers. Index.

Chapter 28. Model Elimination and Connection Tableau Procedures

(Reinhold Letz, Gernot Stenz).

- Introduction.

- Clausal Tableaux and Connectedness.

- Further Structural Refinements of Clausal Tableaux.

- Global Pruning Methods in Model Elimination.

- Shortening of Proofs.

- Completeness of Connection Tableaux.

- Architectures of Model Elimination Implementations.

- Implementation of Refinements by Constraints.

- Experimental Results.

- Outlook.

Bibliography. Index. Concept index.

## Description

Part V. Higher-order logic and logical frameworks.

Chapter 15. Classical Type Theory (Peter B. Andrews).

- Introduction to type theory.

- Metatheoretical foundations.

- Proof search.

- Conclusion.

Bibliography. Index.

Chapter 16. Higher-Order Unification and Matching (Gilles Dowek).

- Type Theory and Other Set Theories.

- Simply Typed &lgr;-calculus.

- Undecidability.

- Huet's Algorithm.

- Scopes Management.

- Decidable Subcases.

- Unification in &lgr;-calculus with Dependent Types.

Bibliography. Index.

Chapter 17. Logical Frameworks (Frank Pfenning).

- Introduction.

- Abstract syntax.

- Judgments and deductions.

- Meta-programming and proof search.

- Representing meta-theory.

- Appendix: the simply-typed &lgr;-calculus.

- Appendix: the dependently typed &lgr;-calculus.

- Conclusion.

Bibliography. Index.

Chapter 18. Proof-Assistants Using Dependent Type Systems (Henk Barendregt, Herman Geuvers).

- Proof checking.

- Type-theoretic notions for proof checking.

- Type systems for proof checking.

- Proof-development in type systems.

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

- General Nonmonotonic Logics.

- Automating General Nonmonotonic Logics.
- From Automated Reasoning to Disjunctive Logic Programming.

- Nonmonotonic Semantics of Logic Programs.

- Implementing Nonmonotonic Semantics.

- Benchmarks.

- Conclusion.

Bibliography. Index.

Chapter 20. Automated Deduction for Many-Valued Logics
(Matthias Baaz, Christian G. Fermuller, Gernot Salzer).

- Introduction.

- What is a many-valued logic?

- Classification of proof systems for many-valued logics.

- Signed logic: reasoning classically about finitely-valued logics.

- Signed resolution.

- An example.

- Optimization of transformation rules.

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

- Introduction.

- Background.

- Encoding consequence relations.

- The standard relational translation.

- The functional translation.

- The semi-functional translation.

- Variations and alternatives.

- Conclusion.

Bibliography. Index.

Chapter 22. Connections in Nonclassical Logics (Arild Waaler).

- Introduction.

- Prelude: Connections in classical first-order logic.

- Labelled systems.

- Propositional intuitionistic logic.

- First--order intuitionistic logic.

- Normal modal logics up to S4.

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

- Introduction.

- Description Logics.

- Description Logics and Propositional Dynamic Logics.

- Unrestricted Model Reasoning.

- Finite Model Reasoning.

- Beyond Basic Description Logics.

- Conclusions.

Bibliography. Index.

Chapter 24. Model Checking (Edmund M. Clarke, Bernd-Holger Schlingloff).

- Introduction.

- Logical Languages, Expressiveness.

- Second Order Languages.

- Model Transformations and Properties.

- Equivalence reductions.

- Completeness.

- Decision Procedures.

- Basic Model Checking Algorithms.

- Modelling of Reactive Systems.

- Symbolic Model Checking.
- Partial Order Techniques.

- Bounded Model Checking.

- Abstractions.

- Compositionality and Modular Verification.

- Further Topics.

Bibliography. Index.

Chapter 25. Resolution Decision Procedures (Christian G. Fermuller, Alexander Leitsch, Ullrich Hustadt, Tanel Tammet).

- Introduction.

- Notation and definitions.

- Decision procedures based on ordering refinements.

- Hyperresolution as decision procedure.

- Resolution decision procedures for description logics.

- Related work.

Bibliography. Index.

Part VIII. Implementation.

Chapter 26. Term Indexing (R. Sekar, I.V. Ramakrishnan, Andrei Voronkov).

- Introduction.

- Background.

- Data structures for representing terms and indexes.

- A common framework for indexing.

- Path indexing.

- Discrimination trees.

- Adaptive automata.

- Automata-driven indexing.

- Code trees.

- Substitution trees.

- Context trees.

- Unification factoring.

- Multiterm indexing.

- Issues in perfect filtering.

- Indexing modulo AC-theories.

- Elements of term indexing.

- Indexing in practice.

- Conclusion.

Bibliography. Index.

Chapter 27. Combining Superposition, Sorts and Splitting (Christoph Weidenbach).

- What This Chapter is (not) About.

- Foundations.

- A First Simple Prover.

- Inference and Reduction Rules.

- Global Design Decisions.

Bibliography. A Links to Saturation Based Provers. Index.

Chapter 28. Model Elimination and Connection Tableau Procedures

(Reinhold Letz, Gernot Stenz).

- Introduction.

- Clausal Tableaux and Connectedness.

- Further Structural Refinements of Clausal Tableaux.

- Global Pruning Methods in Model Elimination.

- Shortening of Proofs.

- Completeness of Connection Tableaux.

- Architectures of Model Elimination Implementations.

- Implementation of Refinements by Constraints.

- Experimental Results.

- Outlook.

Bibliography. Index. Concept index.

## Details

- No. of pages:
- 1188

- Language:
- English

- Copyright:
- © North Holland 2001

- Published:
- 21st June 2001

- Imprint:
- North Holland

- eBook ISBN:
- 9780080929699

- Hardcover ISBN:
- 9780444508126

## About the Editors

### Alan Robinson Editor

### Affiliations and Expertise

96 Highland Avenue, Greenfield, Massachusetts, USA

### Andrei Voronkov Editor

### Affiliations and Expertise

University of Manchester, Computer Science Department, Oxford Road, Manchester, M13 9LP, UK.