Isabelle (proof assistant)


The Isabelle automated theorem prover is an interactive theorem prover, a higher order logic theorem prover. It is an LCF-style theorem prover. It is thus based on small logical core to increase the trustworthiness of proofs without requiring explicit proof objects.

Features

Isabelle is generic: it provides a meta-logic, which is used to encode object logics like first-order logic, higher-order logic or Zermelo–Fraenkel set theory. The most widely used object logic is Isabelle/HOL, although significant set theory developments were completed in Isabelle/ZF. Isabelle's main proof method is a higher-order version of resolution, based on higher-order unification.
Though interactive, Isabelle features efficient automatic reasoning tools, such as a term rewriting engine and a tableaux prover, various decision procedures, and, through the Sledgehammer proof-automation interface, external satisfiability modulo theories solvers and resolution-based automated theorem provers, including E and SPASS. It also features two model finders : Nitpick and Nunchaku.
Isabelle features locales which are modules that structure large proofs. A locale fixes types, constants, and assumptions within a specified scope so that they do not have to be repeated for every lemma.
Isar is Isabelle's formal proof language. It is inspired by the Mizar system.
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. Many of the formal proofs are maintained in the Archive of Formal Proofs, which contains at least 500 articles with over 2 million lines of proof in total.
The Isabelle theorem prover is free software, released under the revised BSD license.
Isabelle was named by Lawrence Paulson after Gérard Huet's daughter.

Example proof

Isabelle allows proofs to be written in two different styles, the procedural and the declarative. Procedural proofs specify a series of tactics to apply; while reflecting the procedure that a human mathematician might apply to proving a result, they are typically hard to read as they do not describe the outcome of these steps. Declarative proofs, on the other hand, specify the actual mathematical operations to be performed, and are therefore more easily read and checked by humans.
The procedural style has been deprecated in recent versions of Isabelle.
For example, a declarative proof by contradiction in Isar that the square root of two is not rational can be written as follows.

sqrt2_not_rational:

?x =

m n :: nat
sqrt_rat: lowest_terms:


eq: of_nat_eq_iff power2_eq_square fastforce
simp
simp
-
k ..
eq simp
simp
simp


lowest_terms simp
False odd_one blast

Applications

Isabelle has been used to aid formal methods for the specification, development and verification of software and hardware systems.
Larry Paulson keeps a that use Isabelle.

Alternatives

Several proof assistants provide similar functionality to Isabelle, including: