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 41 to 60 of 63.
Sorted by year (- Röckl, Christine; Hirschkoff, Daniel; Berghofer, Stefan: Higher-order abstract syntax with induction in Isabelle/HOL: formalizing the (\pi)-calculus and mechanizing the theory of contexts (2001)
- Anderson, Penny; Basin, David: Program development schemata as derived rules (2000)
- Basin, David; Clavel, Manuel; Meseguer, José: Rewriting logic as a metalogical framework (2000)
- Basin, David; Matthews, Seán: Structuring metatheory on inductive definitions (2000)
- Farmer, William M.; Guttman, Joshua D.: A set theory with support for partial functions (2000)
- Formisano, Andrea; Omodeo, Eugenio: An equational re-engineering of set theories (2000)
- Formisano, Andrea; Omodeo, Eugenio G.; Temperini, Marco: Goals and benchmarks for automated map reasoning (2000)
- Staples, Mark: Interfaces for refining recursion and procedures (2000)
- Bertot, Yves (ed.); Dowek, Gilles (ed.); Hirschowitz, André (ed.); Paulin, Christine (ed.); Théry, Laurent (ed.): Theorem proving in higher order logics. 12th international conference, TPHOLs ’99. Nice, France, September 14--17, 1999. Proceedings (1999)
- Paulson, Lawrence C.: A generic tableau prover and its integration with Isabelle (1999)
- Paulson, Lawrence C.: Final coalgebras as greatest fixed points in ZF set theory (1999)
- Staples, Mark: Representing WP semantics in Isabelle/ZF (1999)
- Dennis, Louise; Bundy, Alan; Green, Ian: Using a generalisation critic to find bisimulations for coinductive proofs (1997)
- Paulson, Lawrence C.: Mechanizing coinduction and corecursion in higher-order logic (1997)
- Paulson, Lawrence C.: Tool support for logics of programs (1997)
- Rasmussen, Ole: An embedding of Ruby in Isabelle (1996)
- Simons, Martin; Weber, Matthias: An approach to literate and structured formal developments (1996)
- Agerholm, Sten; Gordon, Mike: Experiments with ZF set theory in HOL and Isabelle (1995)
- Paulson, Lawrence C.: Set theory for verification. II: Induction and recursion (1995)
- Howe, Douglas J.; Stoller, Scott D.: An operational approach to combining classical set theory and functional programming languages (1994)