Isabelle formalization of set theoretic structures and set comprehensions

DOI10.1007/978-3-319-72453-9_12MaRDI QIDQ4628488zbMATH OpenOpenAlexWikidataFDO

Authors Cezary Kaliszyk, Karol Pąk

Publication date 14 March 2019

Published in Mathematical Aspects of Computer and Information Sciences (Search for Journal in Brave)

Full work available at URL https://zenodo.org/record/1475059

zbMATH Keywords

IsabelleMizarmultiple inheritanceset comprehensionset-theoretic structure

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Set theory (03E99) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Semantics of Mizar as an Isabelle object logic
• Set theory for verification. I: From foundations to functions
• Implementation of the composition-nominative approach to program formalization in Mizar
• Mathematical Knowledge Management
• A mechanized translation from higher-order logic to set theory

Cited in

(12)

• Implementation of the composition-nominative approach to program formalization in Mizar
• Beginners' quest to formalize mathematics: a feasibility study in Isabelle
• Semantics of Mizar as an Isabelle object logic
• scientific article; zbMATH DE number 7204430 (Why is no real title available?)
• Set theory or higher order logic to represent auction concepts in Isabelle?
• Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
• Isabelle/HOL/GST: a formal proof environment for generalized set theories
• Combining higher-order logic with set theory formalizations
• Prime representing polynomial with 10 unknowns -- introduction
• A formal library of set relations and its application to synchronous languages
• Prime representing polynomial with 10 unknowns -- introduction. II
• Prime representing polynomial with 10 unknowns

Describes a project that uses

Uses Software

• Isabelle
• Mizar

This page was built for publication: Isabelle formalization of set theoretic structures and set comprehensions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4628488)