Become a Readings Member to make your shopping experience even easier. Sign in or sign up for free!

Become a Readings Member. Sign in or sign up for free!

Hello Readings Member! Go to the member centre to view your orders, change your details, or view your lists, or sign out.

Hello Readings Member! Go to the member centre or sign out.

Handbook of Automated Reasoning
Hardback

Handbook of Automated Reasoning

$386.95
Sign in or become a Readings Member to add this title to your wishlist.

6 ½ X 9 7/16 in Part V. Higher-order logic and logical frameworks.

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

  1. Introduction to type theory.

  2. Metath eoretical 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. Undecidab ility.

  4. Huet’s Algorithm.

  5. Scopes Ma nagement.

  6. Decidable Subcases.

  7. Unif ication in &lgr;-calculus with Dependent Types.

Bibliogr aphy. 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

Read More
In Shop
Out of stock
Shipping & Delivery

$9.00 standard shipping within Australia
FREE standard shipping within Australia for orders over $100.00
Express & International shipping calculated at checkout

MORE INFO
Format
Hardback
Publisher
Elsevier Science & Technology
Country
United States
Date
21 June 2001
Pages
1188
ISBN
9780444508126

6 ½ X 9 7/16 in Part V. Higher-order logic and logical frameworks.

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

  1. Introduction to type theory.

  2. Metath eoretical 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. Undecidab ility.

  4. Huet’s Algorithm.

  5. Scopes Ma nagement.

  6. Decidable Subcases.

  7. Unif ication in &lgr;-calculus with Dependent Types.

Bibliogr aphy. 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

Read More
Format
Hardback
Publisher
Elsevier Science & Technology
Country
United States
Date
21 June 2001
Pages
1188
ISBN
9780444508126