The Isabelle
automated theorem prover
Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a m ...
is a
higherorder logic (HOL) theorem prover, written in
Standard ML
Standard ML (SML) is a generalpurpose, modular, functional programming language with compiletime type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of th ...
and
Scala. As an
LCFstyle theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring yet supporting explicit proof objects.
Isabelle is available inside a flexible system framework allowing for logically safe extensions, which comprise both theories as well as implementations for codegeneration, documentation, and specific support for a variety of
formal methods
In computer science, formal methods are mathematically rigorous techniques for the specification, development, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the exp ...
. It can be seen as an
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)
Isabelle was named by
Lawrence Paulson after
Gérard Huet
Gérard Pierre Huet (; born 7 July 1947) is a French computer scientist, linguist and mathematician. He is senior research director at INRIA and mostly known for his major and seminal contributions to type theory, programming language theory and ...
's daughter.
The Isabelle theorem prover is
free software
Free software or libre software is computer software distributed under terms that allow users to run the software for any purpose as well as to study, change, and distribute it and any adapted versions. Free software is a matter of liberty, no ...
, released under the revised
BSD license
BSD licenses are a family of permissive free software licenses, imposing minimal restrictions on the use and distribution of covered software. This is in contrast to copyleft licenses, which have sharealike requirements. The original BSD lic ...
.
Features
Isabelle is generic: it provides a
metalogic
Metalogic is the study of the metatheory of logic. Whereas ''logic'' studies how logical systems can be used to construct valid and sound arguments, metalogic studies the properties of logical systems.Harry GenslerIntroduction to Logic Routledge ...
(a weak
type theory
In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a founda ...
), which is used to encode object logics like
firstorder logic
Firstorder logic—also known as predicate logic, quantificational logic, and firstorder predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. Firstorder logic uses quant ...
(FOL),
higherorder logic
mathematics and logic, a higherorder logic is a form of predicate logic that is distinguished from firstorder logic by additional quantifiers and, sometimes, stronger semantics. Higherorder logics with their standard semantics are more express ...
(HOL) or
Zermelo–Fraenkel set theory
In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such a ...
(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 higherorder version of
resolution, based on higherorder
unification.
Though interactive, Isabelle features efficient automatic reasoning tools, such as a
term rewriting
In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewrite engines, or re ...
engine and a
tableaux prover, various decision procedures, and, through the Sledgehammer proofautomation interface, external
satisfiability modulo theories
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 inv ...
(SMT) solvers (including
CVC4
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 inv ...
) and
resolutionbased
automated theorem prover
Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a m ...
s (ATPs), including
E and
SPASS
SPASS is an automated theorem prover for firstorder logic with equality developed at the Max Planck Institute for Computer Science and using the superposition calculus. The name originally stood for ''Synergetic Prover Augmenting Superposition ...
(the Metis proof method reconstructs resolution proofs generated by these ATPs). It also features two
model
A model is an informative representation of an object, person or system. The term originally denoted the plans of a building in late 16thcentury English, and derived via French and Italian ultimately from Latin ''modulus'', a measure.
Models c ...
finders (
counterexample
A counterexample is any exception to a generalization. In logic a counterexample disproves the generalization, and does so rigorously in the fields of mathematics and philosophy. For example, the fact that "John Smith is not a lazy student" is a ...
generators): Nitpick
[Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich & Christoph Weidenbach]
"A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality"
''Journal of Automated Reasoning'' 61:333–365 (2018). 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
Lemma may refer to:
Language and linguistics
* Lemma (morphology), the canonical, dictionary or citation form of a word
* Lemma (psycholinguistics), a mental abstraction of a word about to be uttered
Science and mathematics
* Lemma (botany), a ...
.
Isar ("intelligible semiautomated reasoning") is Isabelle's formal proof language. It is inspired by the Mizar system
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 ...
.[
]
Example proof
Isabelle allows proofs to be written in two different styles, the procedural and the declarative. Procedural proofs specify a series of tactics
Tactic(s) or Tactical may refer to:
* Tactic (method), a conceptual action implemented as one or more specific tasks
** Military tactics, the disposition and maneuver of units on a particular sea or battlefield
** Chess tactics
In chess, a ta ...
(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.
For example, a declarative proof by contradiction
In logic and mathematics, proof by contradiction is a form of proof that establishes the truth or the validity of a proposition, by showing that assuming the proposition to be false leads to a contradiction. Proof by contradiction is also know ...
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:
(rule Rats_abs_nat_div_natE)
(auto simp add: power2_eq_square)
eq: of_nat_eq_iff power2_eq_square fastforce
simp
simp

k ..
eq simp
simp
simp
(rule gcd_greatest)
lowest_terms simp
False odd_one blast
Applications
Isabelle has been used to aid formal methods
In computer science, formal methods are mathematically rigorous techniques for the specification, development, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the exp ...
for the specification, development and verification of software and hardware systems.
Isabelle has been used to formalize numerous theorems from mathematics
Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...
and computer science
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to practical disciplines (includin ...
, like Gödel's completeness theorem
Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in firstorder logic.
The completeness theorem applies to any firstorder theory: I ...
, Gödel's theorem about the consistency of the axiom of choice
In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of nonempty sets is nonempty''. Informally put, the axiom of choice says that given any collection ...
, the prime number theorem
In mathematics, the prime number theorem (PNT) describes the asymptotic distribution of the prime numbers among the positive integers. It formalizes the intuitive idea that primes become less common as they become larger by precisely quantifying t ...
, 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.
* In 2009, the L4.verified project at NICTA
NICTA (formerly named National ICT Australia Ltd) was Australia's Information and Communications Technology (ICT) Research Centre of Excellence and is now known as CSIRO's Data61. The term "Centre of Excellence" is common marketing terminology ...
produced the first formal proof of functional correctness of a generalpurpose operating system kernel:[
] the seL4 (secure embedded L4) microkernel
In computer science, a microkernel (often abbreviated as μkernel) is the nearminimum amount of software that can provide the mechanisms needed to implement an operating system (OS). These mechanisms include lowlevel address space manageme ...
. 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.
* The definition of the programming language Lightweight Java was proven typesound in Isabelle.
Larry Paulson keeps a list of research projects that use Isabelle.
Alternatives
Several languages and systems provide similar functionality:
* Agda, written in Haskell
Haskell () is a generalpurpose, staticallytyped, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research and industrial applications, Haskell has pioneered a number of programming lang ...
* Coq, written in OCaml
OCaml ( , formerly Objective Caml) is a generalpurpose, multiparadigm programming language which extends the Caml dialect of ML with objectoriented features. OCaml was created in 1996 by Xavier Leroy, Jérôme Vouillon, Damien Doligez, D ...
* Lean, written in C++
* LEGO
Lego ( , ; stylized as LEGO) is a line of plastic construction toys that are manufactured by The Lego Group, a privately held company based in Billund, Denmark. The company's flagship product, Lego, consists of variously colored interlocki ...
, written in Standard ML of New Jersey
* Mizar system
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 ...
, written in Free Pascal
Free Pascal Compiler (FPC) is a compiler for the closely related programminglanguage dialects Pascal and Object Pascal. It is free software released under the GNU General Public License, witexception clausesthat allow static linking against ...
* Metamath
Metamath is a formal language and an associated computer program (a proof checker) for archiving, verifying, and studying mathematical proofs. Several databases of proved theorems have been developed using Metamath covering standard results in ...
, written in ANSI C
ANSI C, ISO C, and Standard C are successive standards for the C programming language published by the American National Standards Institute (ANSI) and ISO/IEC JTC 1/SC 22/WG 14 of the International Organization for Standardization (ISO) and the ...
* Prover9, written in C, with a GUI written in Python
* Twelf, written in Standard ML
Standard ML (SML) is a generalpurpose, modular, functional programming language with compiletime type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of th ...
Notes
References
Further reading
* Lawrence C. Paulson
"The Foundation of a Generic Theorem Prover"
''Journal of Automated Reasoning'', Volume 5, Issue 3 (September 1989), pages: 363–397, .
* Lawrence C. Paulson and Tobias Nipkow
Tobias Nipkow (born 1958) is a German computer scientist.
Career
Nipkow received his Diplom (MSc) in computer science from the Department of Computer Science of the Technische Hochschule Darmstadt in 1982, and his Ph.D. from the University of M ...
"Isabelle Tutorial and User's Manual"
1990.
* M. A. Ozols, K. A. Eastaughffe, and A. Cant
"DOVE: A Tool for 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 HigherOrder Logic"
2020.
External links
* {{Official website, https://isabelle.in.tum.de
Isabelle on Stack Overflow
The Archive of Formal Proofs
IsarMathLib
Proof assistants
Free theorem provers
Software using the BSD license