Handbook of Automated Reasoning

Zusammenfassung This second volume of "Handbook of Automated Reasoning" covers topics such as higher-order logic and logical frameworks! higher-order unification and matching! logical frameworks! proof-assistants using dependent type systems! and nonclassical logics. 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. ...

List of 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 &lgr;-calculus.

3. Undecidability.

4. Huet's Algorithm.

5. Scopes Management.

6. Decidable Subcases.

7. Unification in &lgr;-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 &lgr;-calculus.

7. Appendix: the dependently typed &lgr;-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.

Product details

• Authors: A. Robinson, Alan J A Robinson, Alan J. A. Voronkov Robinson, Alan J.A. (96 Highland Avenue Robinson, Alan J.a. Voronkov Robinson, A. Voronkov
• Assisted by: Alan J.A. Robinson (Editor), Alan Robinson (Editor), Alan J. a. Robinson (Editor), Alan J.A. (96 Highland Avenue Robinson (Editor), Andrei Voronkov (Editor), Andrei (University of Manchester Voronkov (Editor), Voronkov Andrei (Editor)
• Publisher: ELSEVIER SCIENCE BV
• Languages: English
• Product format: Hardback
• Released: 21.06.2001
• EAN: 9780444508126
• ISBN: 978-0-444-50812-6
• No. of pages: 1188
• Series: Handbook of Automated Reasonin; Handbook of Automated Reasoning
• Subjects: Natural sciences, medicine, IT, technology > Mathematics > Probability theory, stochastic theory, mathematical statistics; COMPUTERS / Machine Theory, Mathematical theory of computation