Isabelle theorem prover

From Wikipedia, the free encyclopedia

The Isabelle theorem prover is an interactive theorem proving framework, a successor of the HOL theorem prover. It is an LCF-style theorem prover (written in Standard ML), so it is based on a small logical core guaranteeing logical correctness. Isabelle is generic: it provides a meta-logic (a weak type theory), which is used to encode object logics like FOL, HOL or ZFC. Isabelle's main proof method is a higher-order version of resolution, based on higher-order unification. Though interactive, Isabelle also features efficient automatic decision procedures, such as a term rewriting engine (called the simplifier) and a tableaux prover (called the classical reasoner). Isabelle has been used to formalize numerous theorems from mathematics and computer science, like Gödel's completeness theorem, Gödel's theorem about the consistency of the axiom of choice, the prime number theorem, correctness of security protocols, and properties of programming language semantics. Isabelle theorem prover is free software, released under the revised BSD license.

1 Example taken from a theory file
2 See also
3 References
4 External links

[edit] Example taken from a theory file

subsection{*Inductive definition of the even numbers*}

consts Ev :: "nat set"                    | Ev of type set of naturals
inductive Ev                              | Inductive definition, two cases
intros
ZeroI: "0 : Ev"
Add2I: "n : Ev ==> Suc(Suc n) : Ev"

text{* Using the introduction rules: *}
lemma "Suc(Suc(Suc(Suc 0))) \<in> Ev"     | four belongs to Ev
apply(rule Add2I)                         | proof
apply(rule Add2I)
apply(rule ZeroI)
done

text{*A simple inductive proof: *}        
lemma "n:Ev ==> n+n : Ev"                 | 2n is even if n is even
apply(erule Ev.induct)                    | induction
 apply(simp)                              | simplification
 apply(rule Ev.ZeroI)
apply(simp)
apply(rule Ev.Add2I)
apply(rule Ev.Add2I)
apply(assumption)
done

Isabelle also supports a declarative proof style.

This software-related article is a stub. You can help Wikipedia by expanding it.

[edit] See also

Formal methods

[edit] References

Lawrence C. Paulson: The foundation of a generic theorem prover. Journal of Automated Reasoning, Volume 5 , Issue 3 (September 1989), Pages: 363 - 397, ISSN 0168-7433
Lawrence C. Paulson: The Isabelle Reference Manual
Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel: Isabelle/HOL - A Proof Assistant for Higher-Order Logic