Isabelle theorem prover
Encyclopedia
The Isabelle theorem prover is an interactive theorem prover
, successor of the Higher Order Logic (HOL) theorem prover
. It is an LCF-style
theorem prover (written in Standard ML
), so it is based on a small logical core guaranteeing logical correctness. 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). 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
, as well as various decision procedures. 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
. The Isabelle theorem prover is free software
, released under the revised BSD license.
sqrt2_not_rational:
m n :: nat
n_nonzero: sqrt_rat:
lowest_terms: ..
n_nonzero sqrt_rat simp
(auto simp add: power2_eq_square)
simp
simp
eq: ..
..
two_is_prime dvd_m: (rule prime_dvd_power_two)
k ..
eq (auto simp add: power2_eq_square mult_ac)
simp
..
two_is_prime (rule prime_dvd_power_two)
dvd_m (rule gcd_greatest)
lowest_terms simp
False arith
for the specification, development and verification of software and hardware systems.
: 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 8,700 lines of C and 600 lines of assembler. 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 160 bugs in the C code of the seL4 kernel, and about 150 issues in each of design and specification.
Larry Paulson keeps a list of research projects that use Isabelle.
Interactive theorem proving
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 man-machine collaboration...
, successor of the Higher Order Logic (HOL) theorem prover
HOL theorem prover
HOL denotes a family of interactive theorem proving systems sharingsimilar logics and implementation strategies....
. It is an LCF-style
LCF theorem prover
Logic for Computable Functions is an interactive automated theorem prover developed at the universities of Edinburgh and Stanford by Robin Milner and others in 1972. LCF introduced the general-purpose programming language ML to allow users to write theorem-proving tactics. Theorems in the system...
theorem prover (written in Standard ML
Standard ML
Standard ML is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of theorem provers.SML is a modern descendant of the ML...
), so it is based on a small logical core guaranteeing logical correctness. Isabelle is generic: it provides a meta-logic (a weak type theory
Type theory
In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...
), which is used to encode object logics like First-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
(FOL), Higher-order logic (HOL)
Higher-order logic
In mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and a stronger semantics...
or Zermelo–Fraenkel set theory
Zermelo–Fraenkel set theory
In mathematics, Zermelo–Fraenkel set theory with the axiom of choice, named after mathematicians Ernst Zermelo and Abraham Fraenkel and commonly abbreviated ZFC, is one of several axiomatic systems that were proposed in the early twentieth century to formulate a theory of sets without the paradoxes...
(ZFC). Isabelle's main proof method is a higher-order
Higher-order logic
In mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and a stronger semantics...
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
Method of analytic tableaux
In proof theory, the semantic tableau is a decision procedure for sentential and related logics, and a proof procedure for formulas of first-order logic. The tableau method can also determine the satisfiability of finite sets of formulas of various logics. It is the most popular proof procedure...
, as well as various decision procedures. Isabelle has been used to formalize numerous theorems from mathematics and computer science, like Gödel's completeness theorem
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. It was first proved by Kurt Gödel in 1929....
, Gödel's theorem about the consistency of the axiom of choice, the prime number theorem
Prime number theorem
In number theory, the prime number theorem describes the asymptotic distribution of the prime numbers. The prime number theorem gives a general description of how the primes are distributed amongst the positive integers....
, correctness of security
Information security
Information security means protecting information and information systems from unauthorized access, use, disclosure, disruption, modification, perusal, inspection, recording or destruction....
protocols, and properties of programming language semantics
Formal semantics of programming languages
In programming language theory, semantics is the field concerned with the rigorous mathematical study of the meaning of programming languages and models of computation...
. The Isabelle theorem prover is free software
Free software
Free software, software libre or libre software is software that can be used, studied, and modified without restriction, and which can be copied and redistributed in modified or unmodified form either without restriction, or with restrictions that only ensure that further recipients can also do...
, released under the revised BSD license.
Example proof
Isabelle's proof language Isar aims to support proofs that are both human-readable and machine-checkable. For example, the proof that the square root of two is not rational can be written as follows.sqrt2_not_rational:
m n :: nat
n_nonzero: sqrt_rat:
lowest_terms: ..
n_nonzero sqrt_rat simp
(auto simp add: power2_eq_square)
simp
simp
eq: ..
..
two_is_prime dvd_m: (rule prime_dvd_power_two)
k ..
eq (auto simp add: power2_eq_square mult_ac)
simp
..
two_is_prime (rule prime_dvd_power_two)
dvd_m (rule gcd_greatest)
lowest_terms simp
False arith
Applications
Isabelle has been used to aid formal methodsFormal methods
In computer science and software engineering, formal methods are a particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems...
for the specification, development and verification of software and hardware systems.
- The use of Isabelle by Hewlett-PackardHewlett-PackardHewlett-Packard Company or HP is an American multinational information technology corporation headquartered in Palo Alto, California, USA that provides products, technologies, softwares, solutions and services to consumers, small- and medium-sized businesses and large enterprises, including...
in the design of the HP 9000HP 9000HP 9000 is the name for a line of workstation and server computer systems produced by the Hewlett-Packard Company . The native operating system for almost all HP 9000 systems is HP-UX, a derivative of Unix. The HP 9000 brand was introduced in 1984 to encompass several existing technical...
line of servers' Runway busRunway busThe Runway bus is a front side bus developed by Hewlett-Packard for use by its PA-RISC microprocessor family. The Runway bus is a 64-bit wide, split transaction, time multiplexed address and data bus running at 120 MHz...
, leading to the discovery of a number of bugs uncaught by previous testing and simulation.
- 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
L4 microkernel family
L4 is a family of second-generation microkernels, generally used to implement Unix-like operating systems, but also used in a variety of other systems.L4 was a response to the poor performance of earlier microkernel-base operating systems...
) microkernel
Microkernel
In computer science, a microkernel is the near-minimum amount of software that can provide the mechanisms needed to implement an operating system . These mechanisms include low-level address space management, thread management, and inter-process communication...
. The proof is constructed and checked in Isabelle/HOL and comprises over 200,000 lines of proof script to verify 8,700 lines of C and 600 lines of assembler. 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 160 bugs in the C code of the seL4 kernel, and about 150 issues in each of design and specification.
- The programming language Lightweight JavaLightweight JavaLightweight Java 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 Isabelle/HOL....
was proven type-soundType soundnessIn computer science, a programming language with a static type system is considered to be type sound if a well-typed program cannot cause type errors....
in Isabelle.
Larry Paulson keeps a list of research projects that use Isabelle.