Isabelle/ZF
Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. The main application is the formalization of mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware or software and proving properties of computer languages and protocols. Isabelle/ZF formalizes the greater part of elementary set theory, including relations, functions, injections, surjections, ordinals and cardinals. Results proved include Cantor’s Theorem, the Recursion Theorem, the Schroeder-Bernstein Theorem, and (assuming AC) the Wellordering Theorem. Isabelle/ZF also provides theories of lists, trees, etc., for formalizing computational notions. It supports inductive definitions of infinite-branching trees for any cardinality of branching. (ZF: Zermelo-Fraenkel Set Theory)
Keywords for this software
References in zbMATH (referenced in 63 articles , 1 standard article )
Showing results 1 to 20 of 63.
Sorted by year (- Sieg, Wilfried; Walsh, Patrick: Natural formalization: deriving the Cantor-Bernstein theorem in ZF (2021)
- Gunther, Emmanuel; Pagano, Miguel; Sánchez Terraf, Pedro: First steps towards a formalization of forcing (2019)
- Kaliszyk, Cezary; Pąk, Karol: Semantics of Mizar as an Isabelle object logic (2019)
- Kirst, Dominik; Smolka, Gert: Categoricity results and large model constructions for second-order ZF in dependent type theory (2019)
- Zhan, Bohua: Formalization of the fundamental group in untyped set theory using auto2 (2019)
- Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy: Friends with benefits. Implementing corecursion in foundational proof assistants (2017)
- Kaliszyk, Cezary; Pąk, Karol: Presentation and manipulation of Mizar properties in an Isabelle object logic (2017)
- Obua, Steven; Scott, Phil; Fleuriot, Jacques: ProofScript: proof scripting for the masses (2016)
- Brown, Chad E.: Reconsidering pairs and functions as sets (2015)
- Obua, Steven; Fleuriot, Jacques; Scott, Phil; Aspinall, David: Type inference for ZFH (2015)
- Paulson, Lawrence C.: A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle (2015)
- Caminati, Marco B.; Kerber, Manfred; Lange, Christoph; Rowat, Colin: Set theory or higher order logic to represent auction concepts in Isabelle? (2014)
- Felty, Amy; Momigliano, Alberto: Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (2012)
- Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias: Automatic proof and disproof in Isabelle/HOL (2011)
- Norrish, Michael: Mechanised computability theory (2011)
- Krauss, Alexander: Partial and nested recursive function definitions in higher-order logic (2010)
- Krauss, Alexander; Schropp, Andreas: A mechanized translation from higher-order logic to set theory (2010)
- Beckmann, Arnold (ed.); Dimitracopoulos, Costas (ed.); Löwe, Benedikt (ed.): Logic and theory of algorithms. 4th conference on computability in Europe, CiE 2008, Athens, Greece, June 15--20, 2008. Proceedings (2008)
- Niqui, Milad: Coinductive formal reasoning in exact real arithmetic (2008)
- Paulson, Lawrence C.: The relative consistency of the axiom of choice -- mechanized using Isabelle/ZF (2008)