Нашли опечатку? Выделите ее мышкой и нажмите Ctrl+Enter
Название: Classical Type Theory, Chapter 15 of Handbook of Automated Reasoning, Volume 2, 965-1007.
Автор: Andrews P.B.
Аннотация:
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.