Isabelle (theorem prover)

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 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.

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 the HP 9000 line of server's Runway 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.

Игры ⚽ Поможем решить контрольную работу

Look at other dictionaries:

  • LCF (theorem prover) — LCF (Logic for Computable Functions) is an interactive automated theorem prover developed at the universities of Edinburgh and Stanford by Robin Milner and others. LCF introduced the general purpose programming language ML to allow users to write …   Wikipedia

  • ISABELLE — Aktuelle Version: Isabelle2008 Betriebssystem: unixoide Kategorie: Theorembeweiser Lizenz: BSD Lizenz …   Deutsch Wikipedia

  • Isabelle (Theorembeweiser) — Isabelle Aktuelle Version Isabelle2011 Betriebssystem unixoide Programmier­sprache Standard ML Kategorie Theorembeweiser Lizenz …   Deutsch Wikipedia

  • HOL theorem prover family — HOL (Higher Order Logic) denotes a family of interactive theorem proving systems sharingsimilar logics and implementation strategies. Systems in this family follow the LCF approach as they are implemented as a library in some programming language …   Wikipedia

  • Prime number theorem — PNT redirects here. For other uses, see PNT (disambiguation). In number theory, the prime number theorem (PNT) describes the asymptotic distribution of the prime numbers. The prime number theorem gives a general description of how the primes are… …   Wikipedia

  • Gödel's completeness theorem — is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first order logic. It was first proved by Kurt Gödel in 1929. A first order formula is called logically valid if… …   Wikipedia

  • Automated theorem proving — (ATP) or automated deduction, currently the most well developed subfield of automated reasoning (AR), is the proving of mathematical theorems by a computer program. Decidability of the problem Depending on the underlying logic, the problem of… …   Wikipedia

  • Interactive theorem proving — is the field of computer science and mathematical logic concerned with tools to develop formal proofs by man machine collaboration. This involves some sort of proof assistant: an interactive proof editor, or other interface, with which a human… …   Wikipedia

  • List of mathematical logic topics — Clicking on related changes shows a list of most recent edits of articles to which this page links. This page links to itself in order that recent changes to this page will also be included in related changes. This is a list of mathematical logic …   Wikipedia

  • Formal verification — In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”