- Isabelle (theorem prover)
Infobox Software
name = Isabelle
caption =
collapsible =
author =
developer =
released =
latest release version =
latest release date =
latest maintenance version =
latest maintenance date =
latest preview version =
latest preview date =
frequently updated =
programming language =
operating system = Linux, Solaris
platform =
size =
language =
status =
genre = Mathematics
license =
website = http://isabelle.in.tum.de/The Isabelle theorem prover is an interactive theorem proving framework, a successor of theHOL theorem prover . It is an LCF-style theorem prover (written inStandard ML ), so it is based on a small logical core guaranteeing logical correctness. Isabelle is generic: it provides a meta-logic (a weaktype theory ), which is used to encode object logics like FOL, HOL orZFC . Isabelle's main proof method is a higher-order version of resolution, based on higher-orderunification . Though interactive, Isabelle also features efficient automatic decision procedures, such as aterm 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, likeGödel's completeness theorem , Gödel's theorem about the consistency of theaxiom of choice , theprime number theorem , correctness of security protocols, and properties of programming language semantics.Isabelle theorem prover isfree software , released under the revisedBSD license .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)))
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 [http://www.skokodyn.com/strangeset/Isar_example.pdf declarative proof style] .
Usage
Among other places, Isabelle has been applied by
Hewlett-Packard in the design of theHP 9000 line of server'sRunway bus where it discovered a number of bugs uncaught by previous testing and simulation [Philip Wadler 's [http://portal.acm.org/citation.cfm?id=274933 "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] .ee also
*
Formal methods 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"
* 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"External links
* [http://isabelle.in.tum.de/ Isabelle website]
* [http://afp.sourceforge.net/ The Archive of Formal Proofs]
* [http://savannah.nongnu.org/projects/isarmathlib IsarMathLib]
Wikimedia Foundation. 2010.