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 maj ...

is a higher-order logic (HOL) theorem prover, written in

Standard ML Standard ML (SML) 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 the ...

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 lic ...

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 foundat ...

), 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 as ...

(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 reduc ...

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

-based

s (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): NitpickJasmin 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 as ...

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

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 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 Applied science, practical discipli ...

, 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: 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 non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collectio ...

, 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 ...

, 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 OCaml ( , formerly Objective Caml) is a general-purpose programming language, general-purpose, multi-paradigm programming language which extends the Caml dialect of ML (programming language), ML with object-oriented programming, object-oriented ...

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 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 interlocking ...

, 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 ...

, 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 it ...

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 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

Notes

References

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

Features

Example proof

Applications

Alternatives

Notes

References

Further reading

External links