The Isabelle
automated theorem prover is a
higher-order logic (HOL) theorem prover, written in
Standard ML and
Scala. As an
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.
Isabelle is available inside a flexible system framework allowing for logically safe extensions, which comprise both theories as well as implementations for code-generation, 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
Lawrence Charles Paulson (born 1955) 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.
Education
Paulson graduated from the ...
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 share-alike requirements. The original BSD lice ...
.
Features
Isabelle is generic: it provides a
meta-logic
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 fou ...
), which is used to encode object logics like
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
(FOL),
higher-order logic
mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order 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 ...
(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
Resolution(s) may refer to:
Common meanings
* Resolution (debate), the statement which is debated in policy debate
* Resolution (law), a written motion adopted by a deliberative body
* New Year's resolution, a commitment that an individual mak ...
, based on higher-order
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 red ...
engine and a
tableaux prover, various decision procedures, and, through the Sledgehammer proof-automation 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 involvi ...
(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 involvi ...
) and
resolution
Resolution(s) may refer to:
Common meanings
* Resolution (debate), the statement which is debated in policy debate
* Resolution (law), a written motion adopted by a deliberative body
* New Year's resolution, a commitment that an individual mak ...
-based
automated theorem provers (ATPs), including
E and
SPASS
SPASS is an automated theorem prover for first-order 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 wi ...
(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 16th-century 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.
Isar ("intelligible semi-automated 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 in ...
.[
]
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
** Political tact ...
(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 known ...
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
Verify or verification may refer to:
General
* Verification and validation, in engineering or quality management systems, is the act of reviewing, inspecting or testing, in order to establish and document that a product, service or system meets ...
of software and hardware systems.
Isabelle has been used to formalize numerous theorems from 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 (includi ...
, 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 first-order logic.
The completeness theorem applies to any first-order theory: ...
, 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 non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collection ...
, the prime number theorem, correctness of security protocol
A security protocol (cryptographic protocol or encryption protocol) is an abstract or concrete protocol that performs a security-related function and applies cryptographic methods, often as sequences of cryptographic primitives. A protocol describe ...
s, and properties of programming language semantics
In programming language theory, semantics is the rigorous mathematical study of the meaning of programming languages. Semantics assigns computational meaning to valid strings in a programming language syntax.
Semantics describes the processe ...
. 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 u ...
produced the first formal proof of functional correctness of a general-purpose operating system kernel:[
] the seL4 (secure embedded L4) microkernel
In computer science, a microkernel (often abbreviated as μ-kernel) is the near-minimum amount of software that can provide the mechanisms needed to implement an operating system (OS). These mechanisms include low-level address space management, ...
. 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 Lightweight Java (LJ) is a fully formalized and extensible minimal imperative fragment of Java. The language was designed for academic purposes within the Computer Laboratory, University of Cambridge. The definition of LJ was proven type-sound in ...
was proven type-sound in Isabelle.
Larry Paulson keeps a list of research projects that use Isabelle.
Alternatives
Several languages and systems provide similar functionality:
* Agda Agda may refer to:
* Agda (programming language), the programming language and theorem prover
* Agda (Golgafrinchan), the character in ''The Hitchhiker's Guide to the Galaxy'' by Douglas Adams
* Liten Agda, the heroine of a Swedish legend
* Agda M ...
, written in Haskell
Haskell () is a general-purpose, statically-typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research and industrial applications, Haskell has pioneered a number of programming lan ...
* Coq
Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof ...
, written in OCaml
* Lean
Lean, leaning or LEAN may refer to:
Business practices
* Lean thinking, a business methodology adopted in various fields
** Lean construction, an adaption of lean manufacturing principles to the design and construction process
** Lean governm ...
, written in C++
C++ (pronounced "C plus plus") is a high-level general-purpose programming language created by Danish computer scientist Bjarne Stroustrup as an extension of the C programming language, or "C with Classes". The language has expanded significan ...
* LEGO, written in Standard ML of New Jersey
Standard ML of New Jersey (SML/NJ; Standard Meta-Language of New Jersey) is a free and open-source compiler and programming environment for the Standard ML programming language. Aside from its runtime system, which is written in C, SML/NJ is wr ...
* 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 in ...
, written in Free Pascal
Free Pascal Compiler (FPC) is a compiler for the closely related programming-language dialects Pascal and Object Pascal. It is free software released under the GNU General Public License, witexception clausesthat allow static linking against its ...
* 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 th ...
* Prover9 Prover9 is an automated theorem prover for first-order and equational logic developed by William McCune.
Description
Prover9 is the successor of the Otter theorem prover also developed by William McCune. Prover9 is noted for producing relatively ...
, written in C, with a GUI written in Python
Python may refer to:
Snakes
* Pythonidae, a family of nonvenomous snakes found in Africa, Asia, and Australia
** ''Python'' (genus), a genus of Pythonidae found in Africa and Asia
* Python (mythology), a mythical serpent
Computing
* Python (pro ...
* Twelf Twelf is an implementation of the logical framework LF developed by Frank Pfenning and Carsten Schürmann at Carnegie Mellon University. It is used for logic programming and for the formalization of programming language theory.
Introduction
At i ...
, written in Standard ML
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 ...
"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 Higher-Order 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