Isabelle formalization of set theoretic structures and set comprehensions

DOI10.1007/978-3-319-72453-9_12zbMATH Open1497.68547OpenAlexW2777315468WikidataQ108482127 ScholiaQ108482127MaRDI QIDQ4628488FDOQ4628488

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

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

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)

Cited In (9)

• Prime representing polynomial with 10 unknowns -- introduction. II
• Prime representing polynomial with 10 unknowns
• Combining higher-order logic with set theory formalizations
• Title not available (Why is that?)
• 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
• Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
• Semantics of Mizar as an Isabelle object logic

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)