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)


References in zbMATH (referenced in 63 articles , 1 standard article )

Showing results 21 to 40 of 63.
Sorted by year (citations)
  1. Wenzel, Makarius; Paulson, Lawrence C.; Nipkow, Tobias: The Isabelle framework (2008)
  2. Brown, Chad E.: Automated reasoning in higher-order logic. Set comprehension and extensionality in Church’s type theory (2007)
  3. Gabbay, Murdoch J.: A general mathematics of names (2007)
  4. Brown, Chad E.: Combining type theory and untyped set theory (2006)
  5. Krauss, Alexander: Partial recursive functions in higher-order logic (2006)
  6. Zălinescu, Eugen; Cortier, Véronique; Rusinowitch, Michaël: Relating two standard notions of secrecy (2006)
  7. Back, Ralph-Johan; Preoteasa, Viorel: An algebraic treatment of procedure refinement to support mechanical verification (2005)
  8. Fontaine, Pascal; Ranise, Silvio; Zarba, Calogero G.: Combining lists with non-stably infinite theories (2005)
  9. Manolios, Panagiotis; Vroon, Daron: Ordinal arithmetic: Algorithms and mechanization (2005)
  10. Paulson, Lawrence C.: The relative consistency of the axiom of choice mechanized using Isabelle/ZF (2003)
  11. Bodeveix, Jean-Paul; Filali, Mamoun: Type synthesis in B and the translation of B to PVS (2002)
  12. Brown, Chad E.: Solving for set variables in higher-order theorem proving (2002)
  13. Paulson, Lawrence C.: The reflection theorem: A study in meta-theoretic reasoning (2002)
  14. Ayari, Abdelwaheb; Basin, David: A higher-order interpretation of deductive tableau (2001)
  15. Farmer, William M.: STMM: A set theory for mechanized mathematics (2001)
  16. Formisano, Andrea; Omodeo, Eugenio G.; Temperini, Marco: Layered map reasoning: an experimental approach put to trial on sets (2001)
  17. Helke, Steffen; Kammüller, Florian: Representing hierarchical automata in interactive theorem provers (2001)
  18. Hemer, David; Hayes, Ian; Strooper, Paul: Refinement calculus for logic programming in Isabelle/HOL (2001)
  19. Kohlhase, Michael; Franke, Andreas: MBase: Representing knowledge and context for the integration of mathematical software systems (2001)
  20. Röckl, Christine: A first-order syntax for the (\pi)-calculus in Isabelle/HOL using permutations (2001)