Mechanizing set theory. Cardinal arithmetic and the axiom of choice
From MaRDI portal
Publication:5961491
DOI10.1007/BF00283132zbMath0868.03005OpenAlexW2073127449WikidataQ114018501 ScholiaQ114018501MaRDI QIDQ5961491
Krzysztof Grąbczewski, Lawrence Charles Paulson
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
axiom of choicecardinal arithmeticIsabelle Logical Frameworkproof assistantZermelo-Fraenkel set theory
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (12)
Formalization of Forcing in Isabelle/ZF ⋮ Ordinal arithmetic: Algorithms and mechanization ⋮ Computational logic: its origins and applications ⋮ Explaining Gabriel-Zisman localization to the computer ⋮ The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf ⋮ The formal verification of the ctm approach to forcing ⋮ Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis ⋮ Computer proofs about finite and regular sets: The unifying concept of subvariance. ⋮ Unnamed Item ⋮ From LCF to Isabelle/HOL ⋮ First steps towards a formalization of forcing ⋮ Mechanizing Nonstandard Real Analysis
Uses Software
This page was built for publication: Mechanizing set theory. Cardinal arithmetic and the axiom of choice
