Sciweavers

CADE
2006
Springer

Combining Type Theory and Untyped Set Theory

15 years 9 days ago
Combining Type Theory and Untyped Set Theory
Abstract. We describe a second-order type theory with proof irrelevance. Within this framework, we give a representation of a form of Mac Lane set theory and discuss automated support for constructing proofs within this set theory. One of the novel aspects of the representation is that one is allowed to use any class (in the set theory) as a type (in the type theory). Such class types allow a natural way of representing partial functions (e.g., the first and second operators on the class of Kuratowski ordered pairs). We also discuss how automated search can be used to construct proofs. In particular, the first-order prover Vampire can be called to solve a challenge problem (the injective Cantor Theorem) which is notoriously difficult for higher-order automated provers.
Chad E. Brown
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2006
Where CADE
Authors Chad E. Brown
Comments (0)