| Original author(s) | Lawrence Paulson |
|---|---|
| Stable release | Isabelle2011 |
| Written in | Standard ML |
| Operating system | Linux, Mac OS X, Windows (Cygwin) |
| Type | Mathematics |
| License | BSD license |
| Website | isabelle.in.tum.de |
The Isabelle theorem prover is an interactive theorem prover, successor of the Higher Order Logic (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 First-order logic (FOL), Higher-order logic (HOL) or Zermelo–Fraenkel set theory (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 reasoning tools, such as a term rewriting engine and a tableaux prover, as well as various decision procedures. 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. The Isabelle theorem prover is free software, released under the revised BSD license.
Contents |
Isabelle's proof language Isar aims to support proofs that are both human-readable and machine-checkable. For example, the proof that the square root of two is not rational can be written as follows.
theorem sqrt2_not_rational: "sqrt (real 2) ∉ ℚ" proof assume "sqrt (real 2) ∈ ℚ" then obtain m n :: nat where n_nonzero: "n ≠ 0" and sqrt_rat: "¦sqrt (real 2)¦ = real m / real n" and lowest_terms: "gcd m n = 1" .. from n_nonzero and sqrt_rat have "real m = ¦sqrt (real 2)¦ * real n" by simp then have "real (m²) = (sqrt (real 2))² * real (n²)" by (auto simp add: power2_eq_square) also have "(sqrt (real 2))² = real 2" by simp also have "... * real (m²) = real (2 * n²)" by simp finally have eq: "m² = 2 * n²" .. hence "2 dvd m²" .. with two_is_prime have dvd_m: "2 dvd m" by (rule prime_dvd_power_two) then obtain k where "m = 2 * k" .. with eq have "2 * n² = 2² * k²" by (auto simp add: power2_eq_square mult_ac) hence "n² = 2 * k²" by simp hence "2 dvd n²" .. with two_is_prime have "2 dvd n" by (rule prime_dvd_power_two) with dvd_m have "2 dvd gcd m n" by (rule gcd_greatest) with lowest_terms have "2 dvd 1" by simp thus False by arith qed
Isabelle has been used to aid formal methods for the specification, development and verification of software and hardware systems.
Larry Paulson keeps a list of research projects that use Isabelle.