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.
Contents |
[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.
[edit] Usage
Among other places, Isabelle has been applied by Hewlett-Packard in the design of the HP 9000 line of server's Runway bus where it discovered a number of bugs uncaught by previous testing and simulation[1].
[edit] See also
[edit] References
- ^ Philip Wadler's "An Angry Half-Dozen" (1998) attributes this result to: Albert J. Camilleri. "A hybrid approach to verifying liveness in a symmetric multiprocessor". 10th International Conference on Theorem Proving in Higher-Order Logics, Elsa Gunter and Amy Felty, editors, Murray Hill, New Jersey, August 1997. Lecture Notes in Computer Science 1275, Springer Verlag, 1997
- 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
- M. A. Ozols, K. A. Eastaughffe, and A. Cant. "DOVE: Design Oriented Verification and Evaluation". Proceedings of AMAST 97, M. Johnson, editor, Sydney, Australia. Lecture Notes in Computer Science 1349, Springer Verlag, 1997.
- Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel: Isabelle/HOL - A Proof Assistant for Higher-Order Logic
