Isabelle/ZF 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.68163Staples, Mark 1999 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 all top 5 Cited in 13 Serials 12 Journal of Automated Reasoning 4 Journal of Symbolic Computation 3 Formal Aspects of Computing 2 Information and Computation 2 Lecture Notes in Computer Science 1 Studia Logica 1 Journal of Logic and Computation 1 MSCS. Mathematical Structures in Computer Science 1 LMS Journal of Computation and Mathematics 1 Journal of Universal Computer Science 1 Studies in Logic (London) 1 Logical Methods in Computer Science 1 The Review of Symbolic Logic all top 5 Cited in 7 Fields 61 Computer science (68-XX) 40 Mathematical logic and foundations (03-XX) 2 General and overarching topics; collections (00-XX) 1 General algebraic systems (08-XX) 1 Algebraic topology (55-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year