Mechanizing set theory. Cardinal arithmetic and the axiom of choice

DOI10.1007/BF00283132MaRDI QIDQ5961491zbMATH OpenOpenAlexWikidataFDO

Authors Lawrence C. Paulson, Krzysztof Grąbczewski

Publication date 3 August 1997

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf00283132

zbMATH Keywords

axiom of choiceproof assistantcardinal arithmeticZermelo-Fraenkel set theoryIsabelle Logical Framework

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Ordinal and cardinal numbers (03E10) Axiom of choice and related propositions (03E25)

Recommendations

• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
• The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF
• Set theory for verification. I: From foundations to functions
• Mathematical Knowledge Management

Cited in

(15)

• Formalizing ordinal partition relations using Isabelle/HOL
• The formal verification of the ctm approach to forcing
• scientific article; zbMATH DE number 7649968 (Why is no real title available?)
• Explaining Gabriel-Zisman localization to the computer
• Formalization of Forcing in Isabelle/ZF
• Mechanizing Nonstandard Real Analysis
• Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis
• From LCF to Isabelle/HOL
• Cardinals in Isabelle/HOL
• Ordinal arithmetic: Algorithms and mechanization
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
• Mathematical Knowledge Management
• Computational logic: its origins and applications
• First steps towards a formalization of forcing
• Computer proofs about finite and regular sets: The unifying concept of subvariance.

Describes a project that uses

Uses Software

• Coq
• Isabelle
• IMPS

This page was built for publication: Mechanizing set theory. Cardinal arithmetic and the axiom of choice

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