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 61 to 63 of 63.
- Paulson, Lawrence C.: A fixedpoint approach to implementing (co)inductive definitions (1994)
- Paulson, Lawrence C.: Set theory for verification: I. from foundations to functions (1993) ioport
- Paulson, Lawrence C.: Set theory for verification. I: From foundations to functions (1993)