swMATH ID: 4973
Software Authors: Lawrence C. Paulson
Description: 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)
Homepage: http://isabelle.in.tum.de/website-Isabelle2012/dist/library/ZF/README.html
Keywords: theorem prover; set theory; Zermelo-Fraenkel
Related Software: Isabelle; Coq; Isabelle/HOL; Mizar; HOL; Isar; ML; Nuprl; HOL Light; Archive Formal Proofs; PVS; Metamath; ProofPeer; Nominal Isabelle; TPS; Automath; IMPS; Twelf; Isabelle/Isar; NQTHM
Cited in: 65 Documents

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
Representing WP semantics in Isabelle/ZF. Zbl 0944.68163
Staples, Mark
all top 5

Cited by 89 Authors

13 Paulson, Lawrence Charles
4 Basin, David A.
4 Brown, Chad Edward
3 Formisano, Andrea
3 Kaliszyk, Cezary
3 Krauss, Alexander
3 Omodeo, Eugenio Giovanni
3 Pąk, Karol
2 Blanchette, Jasmin Christian
2 Farmer, William M.
2 Fleuriot, Jacques D.
2 Nipkow, Tobias
2 Obua, Steven
2 Röckl, Christine
2 Scott, Phil
2 Staples, Mark
2 Temperini, Marco
1 Agerholm, Sten
1 Anderson, Penny
1 Aspinall, David
1 Ayari, Abdelwaheb
1 Back, Ralph-Johan
1 Beckmann, Arnold
1 Berghofer, Stefan
1 Bertot, Yves
1 Bodeveix, Jean-Paul
1 Bouzy, Aymeric
1 Bulwahn, Lukas
1 Bundy, Alan
1 Caminati, Marco Bright
1 Clavel, Manuel
1 Cortier, Véronique
1 Dennis, Louise Abigail
1 Dimitracopoulos, Costas
1 Dowek, Gilles
1 Dunne, Ciarán
1 Felty, Amy P.
1 Filali, Mamoun
1 Fontaine, Pascal
1 Franke, Andreas
1 Gabbay, Murdoch James
1 Green, Ian
1 Gunther, Emmanuel
1 Guttman, Joshua D.
1 Hayes, Ian J.
1 Helke, Steffen
1 Hemer, David
1 Hirschkoff, Daniel
1 Hirschowitz, André
1 Howe, Douglas J.
1 Kamareddine, Fairouz D.
1 Kammüller, Florian
1 Kerber, Manfred
1 Kirst, Dominik
1 Kohlhase, Michael
1 Lange, Christoph
1 Lochbihler, Andreas
1 Löwe, Benedikt
1 Manolios, Panagiotis
1 Matthews, Seán
1 Meseguer Guaita, José
1 Momigliano, Alberto
1 Niqui, Milad
1 Norrish, Michael
1 Pagano, Miguel
1 Paulin, Christine
1 Popescu, Andrei
1 Preoteasa, Viorel
1 Ranise, Silvio
1 Rasmussen, Ole Hjorth
1 Rowat, Colin
1 Rusinowitch, Michaël
1 Sánchez Terraf, Pedro
1 Schropp, Andreas
1 Sieg, Wilfried
1 Simons, Martin
1 Smolka, Gert
1 Stoller, Scott D.
1 Strooper, Paul A.
1 Théry, Laurent
1 Traytel, Dmitry
1 Vroon, Daron
1 Walsh, Patrick M.
1 Weber, Matthias
1 Wells, Joe B.
1 Wenzel, Makarius
1 Zălinescu, Eugen
1 Zarba, Calogero G.
1 Zhan, Bohua

Citations by Year