A Mechanized Translation from Higher-Order Logic to Set Theory
From MaRDI portal
Publication:5747659
DOI10.1007/978-3-642-14052-5_23zbMath1291.68355OpenAlexW2129510553MaRDI QIDQ5747659
Alexander Krauss, Andreas Schropp
Publication date: 14 September 2010
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-14052-5_23
Related Items
Classification of alignments between concepts of formal mathematical systems, Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation, Making PVS accessible to generic services by interpretation in a universal format, Combining higher-order logic with set theory formalizations, Unnamed Item, From types to sets by local type definition in higher-order logic, Higher-Order Tarski Grothendieck as a Foundation for Formal Proof., A consistent foundation for Isabelle/HOL, A logical framework combining model and proof theory, A Foundational View on Integration Problems, Formalising foundations of mathematics, From Types to Sets by Local Type Definitions in Higher-Order Logic, Experiences from exporting major proof assistant libraries, Semantics of Mizar as an Isabelle object logic, A formalization of the Smith normal form in higher-order logic
Uses Software
