Handbook of Automated Reasoning - 1st Edition - ISBN: 9780444508126, 9780080929699

Handbook of Automated Reasoning, Volume II

1st Edition

Print ISBN: 9780444508126
eBook ISBN: 9780080929699
Imprint: North Holland
Published Date: 21st June 2001
Page Count: 1188

Institutional Access

Table 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 Lo


No. of pages:
© North Holland 2001
North Holland
eBook ISBN:
Hardcover ISBN: