Isabelle (proof assistant)
This article includes a list of references, but its sources remain unclear because it has insufficient inline citations. (February 2018) (Learn how and when to remove this template message)
Isabelle/jEdit running on macOS.
|Original author(s)||Lawrence Paulson|
|Developer(s)||University of Cambridge and Technical University of Munich et al.|
2019 / June 2019
|Written in||Standard ML and Scala|
|Operating system||Linux, Windows, Mac OS X|
The Isabelle automated theorem prover is an interactive theorem prover, a higher order logic (HOL) theorem prover. It is an LCF-style theorem prover (written in Standard ML). It is thus based on small logical core (kernel) to increase the trustworthiness of proofs without requiring (yet supporting) explicit proof objects. 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). 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 also features efficient automatic reasoning tools, such as a term rewriting engine and a tableaux prover, various decision procedures, and, through the sledgehammer interface, external Satisfiability modulo theories (SMT) solvers (including CVC4) and resolution-based theorem provers (including E and SPASS).
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 (as of 2019) at least 500 articles with over 2 million lines of proof in total.
Isabelle allows proofs to be written in two different styles, the procedural and the declarative. Procedural proofs specify a series of tactics or procedures 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 (supported by Isabelle's proof language, Isar), 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. The Archive of Formal Proofs also recommends the declarative style.
For example, a declarative proof by contradiction in Isar that the square root of two is not rational can be written as follows.
theorem sqrt2_not_rational: "sqrt (real 2) ∉ ℚ" proof let ?x = "sqrt (real 2)" assume "?x ∈ ℚ" then obtain m n :: nat where sqrt_rat: "¦?x¦ = real m / real n" and lowest_terms: "coprime m n" by (rule Rats_abs_nat_div_natE) hence "real (m^2) = ?x^2 * real (n^2)" by (auto simp add: power2_eq_square) hence eq: "m^2 = 2 * n^2" using of_nat_eq_iff power2_eq_square by fastforce hence "2 dvd m^2" by simp hence "2 dvd m" by simp have "2 dvd n" proof – from ‹2 dvd m› obtain k where "m = 2 * k" with eq have "2 * n^2 = 2^2 * k^2" by simp hence "2 dvd n^2" by simp thus "2 dvd n" by simp qed with ‹2 dvd m› have "2 dvd gcd m n" by (rule gcd_greatest) with lowest_terms have "2 dvd 1" by simp thus False using odd_one by blast qed
- In 2009, the L4.verified project at NICTA produced the first formal proof of functional correctness of a general-purpose operating system kernel: the seL4 (secure embedded L4) microkernel. The proof is constructed and checked in Isabelle/HOL and comprises over 200,000 lines of proof script to verify 7,500 lines of C. The verification covers code, design, and implementation, and the main theorem states that the C code correctly implements the formal specification of the kernel. The proof uncovered 144 bugs in an early version of the C code of the seL4 kernel, and about 150 issues in each of design and specification.
Several proof assistants provide similar functionality to Isabelle, including:
- Coq, similar system written in OCaml
- HOL4, similar to Isabelle's HOL implementation
- Mizar system
- Paulson, L. C. (1986). "Natural deduction as higher-order resolution". The Journal of Logic Programming. 3 (3): 237. arXiv:cs/9301104. doi:10.1016/0743-1066(86)90015-4.
- Eberl, Manuel; Klein, Gerwin; Nipkow, Tobias; Paulson, Larry; Thiemann, René. "Archive of Formal Proofs". Retrieved 22 October 2019.
- Gordon, Mike (1994-11-16). "1.2 History". Isabelle and HOL. Cambridge AR Research (The Automated Reasoning Group). Retrieved 2016-04-28.
- "Archive of Formal Proofs".
- Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon (October 2009). "seL4: Formal verification of an OS kernel" (PDF). 22nd ACM Symposium on Operating System Principles. Big Sky, Montana, US. pp. 207–200.
- 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 (LNCS) Vol. 1349, Springer Verlag, 1997.
- Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel: Isabelle/HOL – A Proof Assistant for Higher-Order Logic.