Sciweavers

ITP
2010

A Mechanized Translation from Higher-Order Logic to Set Theory

13 years 7 months ago
A Mechanized Translation from Higher-Order Logic to Set Theory
Abstract. In order to make existing formalizations available for settheoretic developments, we present an automated translation of theories from Isabelle/HOL to Isabelle/ZF. This covers all fundamental primitives, particularly type classes. The translation produces LCF-style theorems that are checked by Isabelle’s inference kernel. Type checking is replaced by explicit reasoning about set membership.
Alexander Krauss, Andreas Schropp
Added 15 Aug 2010
Updated 15 Aug 2010
Type Conference
Year 2010
Where ITP
Authors Alexander Krauss, Andreas Schropp
Comments (0)