Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

41

ITP
2010

favoriteEmaildiscussreport

165views Mathematics» more ITP 2010»

A Mechanized Translation from Higher-Order Logic to Set Theory

14 years 2 months ago

A Mechanized Translation from Higher-Order Logic to Set Theory

Download www4.in.tum.de

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

Real-time Traffic

Automated Translation | Fundamental Primitives | Isabelle’s Inference Kernel | ITP 2010 | Mathematics |

claim paper

Related Content

» The Representation of Program Synthesis in Higher Order Logic

» ProofTheoretic and HigherOrder Extensions of Logic Programming

» Agnostic PAC Learning Concepts in HigherOrder Logic

» A Design Structure for Higher Order Quotients

» Translating specifications from nominal logic to CIC with the theory of contexts

» Importing HOL Light into Coq

» FirstOrder Logic vs FixedPoint Logic in Finite Set Theory

» Extracting Programs from Constructive HOL Proofs Via IZF SetTheoretic Semantics

» Mechanising Hankin and Barendregt using the GordonMelham axioms

Post Info
More Details (n/a)

Added	15 Aug 2010
Updated	15 Aug 2010
Type	Conference
Year	2010
Where	ITP
Authors	Alexander Krauss, Andreas Schropp

Comments (0)