Type theory, otherwise known as higher-order logic, is an extension of first-order logic which has significant advantages over first-order logic for formalizing certain domains, such as parts of mathematics and specifications for hardware and software. A number of versions of type theory have been developed. Constructive type theory is discussed in [Barendregt and Geuvers 2001] (Chapter 18 of this Handbook). In this chapter we provide an introduction to classical type theory, and discuss methods for automatically proving theorems of classical type theory.

Скачать книгу бесплатно (pdf, 422 Kb)

---

Читать «Classical Type Theory, Chapter 15 of Handbook of Automated Reasoning»