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 47 articles , 1 standard article )

Showing results 1 to 20 of 47.
Sorted by year (citations)

1 2 3 next

  1. Brown, Chad E.: Reconsidering pairs and functions as sets (2015)
  2. Paulson, Lawrence C.: A mechanised proof of Gödel’s incompleteness theorems using nominal Isabelle (2015)
  3. Felty, Amy; Momigliano, Alberto: Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (2012)
  4. Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias: Automatic proof and disproof in Isabelle/HOL (2011)
  5. Krauss, Alexander: Partial and nested recursive function definitions in higher-order logic (2010)
  6. Krauss, Alexander; Schropp, Andreas: A mechanized translation from higher-order logic to set theory (2010)
  7. Niqui, Milad: Coinductive formal reasoning in exact real arithmetic (2008)
  8. Paulson, Lawrence C.: The relative consistency of the axiom of choice -- mechanized using Isabelle/ZF (2008)
  9. Wenzel, Makarius; Paulson, Lawrence C.; Nipkow, Tobias: The Isabelle framework (2008)
  10. Brown, Chad E.: Automated reasoning in higher-order logic. Set comprehension and extensionality in Church’s type theory (2007)
  11. Brown, Chad E.: Encoding functional relations in scunak. (2007)
  12. Gabbay, Murdoch J.: A general mathematics of names (2007)
  13. Brown, Chad E.: Combining type theory and untyped set theory (2006)
  14. Krauss, Alexander: Partial recursive functions in higher-order logic (2006)
  15. Zălinescu, Eugen; Cortier, Véronique; Rusinowitch, Michaël: Relating two standard notions of secrecy (2006)
  16. Back, Ralph-Johan; Preoteasa, Viorel: An algebraic treatment of procedure refinement to support mechanical verification (2005)
  17. Fontaine, Pascal; Ranise, Silvio; Zarba, Calogero G.: Combining lists with non-stably infinite theories (2005)
  18. Manolios, Panagiotis; Vroon, Daron: Ordinal arithmetic: Algorithms and mechanization (2005)
  19. Paulson, Lawrence C.: The relative consistency of the axiom of choice mechanized using Isabelle/ZF (2003)
  20. Bodeveix, Jean-Paul; Filali, Mamoun: Type synthesis in B and the translation of B to PVS (2002)

1 2 3 next