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) Formalization of mathematics in connection with theorem provers (68V20) Set theory (03E99)

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)

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

Describes a project that uses

Uses Software

• Mizar
• Isabelle

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)