Isabelle (proof assistant)

Last updated
Isabelle
Original author(s) Lawrence Paulson
Developer(s) University of Cambridge
Technical University of Munich, et al.
Initial release1986;38 years ago (1986) [1]
Stable release
Isabelle2024 / May 2024;6 months ago (2024-05)
Written in Standard ML, Scala
Operating system Linux, Windows, macOS
Type Mathematics
License BSD
Website isabelle.in.tum.de

The Isabelle [a] automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As a Logic for Computable Functions (LCF) style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring, yet supporting, explicit proof objects.

Contents

Isabelle is available inside a flexible system framework allowing for logically safe extensions, which comprise both theories and implementations for code-generating, documenting, and specific support for a variety of formal methods. It can be seen as an integrated development environment (IDE) for formal methods. In recent years, a substantial number of theories and system extensions have been collected in the Isabelle Archive of Formal Proofs (Isabelle AFP) [2]

Isabelle was named by Lawrence Paulson after Gérard Huet's daughter. [3]

The Isabelle theorem prover is free software, released under the revised BSD license.

Features

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 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 (SMT) solvers (including CVC4) and resolution-based automated theorem provers (ATPs), including E, SPASS, and Vampire (the Metis [b] proof method reconstructs resolution proofs generated by these ATPs). [4] It also features two model finders (counterexample generators): Nitpick [5] and Nunchaku. [6]

Isabelle features locales which are modules that structure large proofs. A locale fixes types, constants, and assumptions within a specified scope [5] so that they do not have to be repeated for every lemma.

Isar ("intelligible semi-automated reasoning") is Isabelle's formal proof language. It is inspired by the Mizar system. [5]

Example proof

Isabelle allows proofs to be written in two different styles, the procedural and the declarative. Procedural proofs specify a series of tactics (theorem proving functions/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.[ citation needed ]

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 2 ∉ ℚ"prooflet ?x = "sqrt 2"assume"?x ∈ ℚ"thenobtain m n :: nat where     sqrt_rat: "¦?x¦ = m / n"and lowest_terms: "coprime m n"by (rule Rats_abs_nat_div_natE)   hence"m^2 = ?x^2 * 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   qedwith‹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

Applications

Isabelle has been used to aid formal methods for the specification, development and verification of software and hardware systems.

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, as mentioned, 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. [7]

Larry Paulson keeps a list of research projects that use Isabelle. [10] [ dead link ]

Alternatives

Several languages and systems provide similar functions:

Notes

Related Research Articles

Automated theorem proving is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major motivating factor for the development of computer science.

L4 is a family of second-generation microkernels, used to implement a variety of types of operating systems (OS), though mostly for Unix-like, Portable Operating System Interface (POSIX) compliant types.

In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

HOL denotes a family of interactive theorem proving systems using similar (higher-order) logics and implementation strategies. Systems in this family follow the LCF approach as they are implemented as a library which defines an abstract data type of proven theorems such that new objects of this type can only be created using the functions in the library which correspond to inference rules in higher-order logic. As long as these functions are correctly implemented, all theorems proven in the system must be valid. As such, a large system can be built on top of a small trusted kernel.

Logic for Computable Functions (LCF) is an interactive automated theorem prover developed at Stanford and Edinburgh by Robin Milner and collaborators in early 1970s, based on the theoretical foundation of logic of computable functions previously proposed by Dana Scott. Work on the LCF system introduced the general-purpose programming language ML to allow users to write theorem-proving tactics, supporting algebraic data types, parametric polymorphism, abstract data types, and exceptions.

<span class="mw-page-title-main">ACL2</span> Programming language and theorem prover

ACL2 is a software system consisting of a programming language, an extensible theory in a first-order logic, and an automated theorem prover. ACL2 is designed to support automated reasoning in inductive logical theories, mostly for software and hardware verification. The input language and implementation of ACL2 are written in Common Lisp. ACL2 is free and open-source software.

<span class="mw-page-title-main">Mizar system</span>

The Mizar system consists of a formal language for writing mathematical definitions and proofs, a proof assistant, which is able to mechanically check proofs written in this language, and a library of formalized mathematics, which can be used in the proof of new theorems. The system is maintained and developed by the Mizar Project, formerly under the direction of its founder Andrzej Trybulec.

E is a high-performance theorem prover for full first-order logic with equality. It is based on the equational superposition calculus and uses a purely equational paradigm. It has been integrated into other theorem provers and it has been among the best-placed systems in several theorem proving competitions. E is developed by Stephan Schulz, originally in the Automated Reasoning Group at TU Munich, now at Baden-Württemberg Cooperative State University Stuttgart.

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification is a key incentive for formal specification of systems, and is at the core of formal methods. It represents an important dimension of analysis and verification in electronic design automation and is one approach to software verification. The use of formal verification enables the highest Evaluation Assurance Level (EAL7) in the framework of common criteria for computer security certification.

<span class="mw-page-title-main">Proof assistant</span> Software tool to assist with the development of formal proofs by human–machine collaboration

In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human–machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.

<span class="mw-page-title-main">Thomas Callister Hales</span> American mathematician

Thomas Callister Hales is an American mathematician working in the areas of representation theory, discrete geometry, and formal verification. In representation theory he is known for his work on the Langlands program and the proof of the fundamental lemma over the group Sp(4). In discrete geometry, he settled the Kepler conjecture on the density of sphere packings, the honeycomb conjecture, and the dodecahedral conjecture. In 2014, he announced the completion of the Flyspeck Project, which formally verified the correctness of his proof of the Kepler conjecture.

<span class="mw-page-title-main">Michael J. C. Gordon</span> British computer scientist

Michael John Caldwell Gordon was a British computer scientist.

In computer science, in particular in knowledge representation and reasoning and metalogic, the area of automated reasoning is dedicated to understanding different aspects of reasoning. The study of automated reasoning helps produce computer programs that allow computers to reason completely, or nearly completely, automatically. Although automated reasoning is considered a sub-field of artificial intelligence, it also has connections with theoretical computer science and philosophy.

<span class="mw-page-title-main">Lawrence Paulson</span> American computer scientist

Lawrence Charles Paulson is an American computer scientist. He is a Professor of Computational Logic at the University of Cambridge Computer Laboratory and a Fellow of Clare College, Cambridge.

In computer science, separation logic is an extension of Hoare logic, a way of reasoning about programs. It was developed by John C. Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang, drawing upon early work by Rod Burstall. The assertion language of separation logic is a special case of the logic of bunched implications (BI). A CACM review article by O'Hearn charts developments in the subject to early 2019.

In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings. The name is derived from the fact that these expressions are interpreted within ("modulo") a certain formal theory in first-order logic with equality. SMT solvers are tools that aim to solve the SMT problem for a practical subset of inputs. SMT solvers such as Z3 and cvc5 have been used as a building block for a wide range of applications across computer science, including in automated theorem proving, program analysis, program verification, and software testing.

Interactive Theorem Proving (ITP) is an annual international academic conference on the topic of automated theorem proving, proof assistants and related topics, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics.

Tobias Nipkow is a German computer scientist.

<span class="mw-page-title-main">Grigore Roșu</span> Computer science professor

Grigore Roșu is a computer science professor at the University of Illinois at Urbana-Champaign and a researcher in the Information Trust Institute. He is known for his contributions in runtime verification, the K framework, matching logic, and automated coinduction.

In computer science, interference freedom is a technique for proving partial correctness of concurrent programs with shared variables. Hoare logic had been introduced earlier to prove correctness of sequential programs. In her PhD thesis under advisor David Gries, Susan Owicki extended this work to apply to concurrent programs.

References

  1. ↑ Paulson, L. C. (1986). "Natural deduction as higher-order resolution". The Journal of Logic Programming. 3 (3): 237–258. arXiv: cs/9301104 . doi:10.1016/0743-1066(86)90015-4. S2CID   27085090.
  2. ↑ Eberl, Manuel; Klein, Gerwin; Nipkow, Tobias; Paulson, Larry; Thiemann, René. "Archive of Formal Proofs" . Retrieved 1 May 2021.
  3. ↑ Gordon, Mike (1994-11-16). "1.2 History". Isabelle and HOL. Cambridge AR Research (The Automated Reasoning Group). Archived from the original on 2017-03-05. Retrieved 2016-04-28.
  4. ↑ Jasmin Christian Blanchette, Lukas Bulwahn, Tobias Nipkow, "Automatic Proof and Disproof in Isabelle/HOL", in: Cesare Tinelli, Viorica Sofronie-Stokkermans (eds.), International Symposium on Frontiers of Combining Systems – FroCoS 2011, Springer, 2011.
  5. 1 2 3 Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich & Christoph Weidenbach, "A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality", Journal of Automated Reasoning61:333–365 (2018).
  6. ↑ Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli, "Model Finding for Recursive Functions in SMT", in: Nicola Olivetti, Ashish Tiwari (eds.), 8th International Joint Conference on Automated Reasoning, Springer, 2016.
  7. ↑ Eberl, Manuel; Klein, Gerwin; Nipkow, Tobias; Paulson, Larry; Thiemann, René. "Archive of Formal Proofs" . Retrieved 22 October 2019.
  8. ↑ 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.
  9. ↑ Strniša, Rok; Parkinson, Matthew (7 February 2011). "Lightweight Java". Archive of Formal Proofs (February 2011 ed.). ISSN   2150-914X . Retrieved 2019-11-25.
  10. ↑ "Projects - Isabelle Community Wiki".

Further reading

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.