Generating custom set theories with non-set structured objects

DOI10.1007/978-3-030-81097-9_19zbMath1485.03221OpenAlexW3168025506MaRDI QIDQ2128829

Ciarán Dunne, J. B. Wells, Fairouz Kamareddine

Publication date: 22 April 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-81097-9_19

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (1)

Isabelle/HOL/GST: a formal proof environment for generalized set theories

Uses Software

• Mizar
• Isabelle/ZF
• Metamath
• Transfer
• Lifting
• IsarMathLib

Cites Work

• Unnamed Item
• Set theory for verification. I: From foundations to functions
• A consistent foundation for Isabelle/HOL
• The foundation of a generic theorem prover
• Adding an abstraction barrier to ZF set theory
• A tale of two set theories
• From Types to Sets by Local Type Definitions in Higher-Order Logic
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Extended First-Order Logic
• Mizar: State-of-the-art and Beyond
• Partizan Games in Isabelle/HOLZF
• First Order Logic with Domain Conditions
• Automated Reasoning
• What Do We Want a Foundation to Do?

This page was built for publication: Generating custom set theories with non-set structured objects