Interactive theorem proving
Encyclopedia
In computer science
and mathematical logic
, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proof
s by man-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
.
-based Proof General, developed at the University of Edinburgh
.
Catalogues
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
and mathematical logic
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proof
Formal proof
A formal proof or derivation is a finite sequence of sentences each of which is an axiom or follows from the preceding sentences in the sequence by a rule of inference. The last sentence in the sequence is a theorem of a formal system...
s by man-machine collaboration. This involves some sort of interactive proof editor, or other interface
User interface
The user interface, in the industrial design field of human–machine interaction, is the space where interaction between humans and machines occurs. The goal of interaction between a human and a machine at the user interface is effective operation and control of the machine, and feedback from the...
, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer
Computer
A computer is a programmable machine designed to sequentially and automatically carry out a sequence of arithmetic or logical operations. The particular sequence of operations can be changed readily, allowing the computer to solve more than one kind of problem...
.
Comparison
| Name | | Latest version | | Developer(s) | | Implementation language | | Features | |||||
|---|---|---|---|---|---|---|---|---|---|
| Higher-order logic 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... | Dependent type Dependent type In computer science and logic, a dependent type is a type that depends on a value. Dependent types play a central role in intuitionistic type theory and in the design of functional programming languages like ATS, Agda and Epigram.... s | Small kernel | Proof automation | Proof by reflection | Program extraction | ||||
| ACL2 | 4.3 | Matt Kaufmann Matt Kaufmann Matt Kaufmann is a Senior Research Scientist in the Department of Computer Sciences at the University of Texas at Austin, USA. He was a recipient of the 2005 ACM Software System Award along with Robert S. Boyer and J Strother Moore, for his work on the The Boyer-Moore Theorem Prover.- External... and J Strother Moore J Strother Moore J Strother Moore is a computer scientist, and he is a co-developer of the Boyer–Moore string search algorithm and the Boyer–Moore automated theorem prover, Nqthm. An example of the workings of the Boyer–Moore string search algorithm is given... |
Common Lisp Common Lisp Common Lisp, commonly abbreviated CL, is a dialect of the Lisp programming language, published in ANSI standard document ANSI INCITS 226-1994 , . From the ANSI Common Lisp standard the Common Lisp HyperSpec has been derived for use with web browsers... |
||||||
| Agda | 2.2.10 | Ulf Norell (Chalmers Chalmers University of Technology Chalmers University of Technology , is a Swedish university located in Gothenburg that focuses on research and education in technology, natural science and architecture.-History:... ) |
Haskell Haskell Haskell may refer to:*Haskell , a standardized pure functional programming language with non-strict semantics* Haskell Indian Nations University, a four year degree granting university in Lawrence, Kansas which offers free tuition to members of registered Native American tribes in the United... |
||||||
| Coq Coq In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification... |
8.3pl2 | INRIA | OCaml | ||||||
| Isabelle/HOL | 2011 | Larry Paulson (Cambridge University of Cambridge The University of Cambridge is a public research university located in Cambridge, United Kingdom. It is the second-oldest university in both the United Kingdom and the English-speaking world , and the seventh-oldest globally... ), Tobias Nipkow (München) and Makarius Wenzel (Paris-Sud) |
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... |
||||||
| LEGO LEGO (proof assistant) LEGO is a proof assistant developed by Randy Pollack at the University of Edinburgh. It implements several type theories: the Edinburgh Logical Framework , the Calculus of Constructions , the Generalized Calculus of Constructions and the Unified Theory of Dependent Types .... |
1.3.1 | Randy Pollack (Edinburgh University of Edinburgh The University of Edinburgh, founded in 1583, is a public research university located in Edinburgh, the capital of Scotland, and a UNESCO World Heritage Site. The university is deeply embedded in the fabric of the city, with many of the buildings in the historic Old Town belonging to the university... ) |
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... |
||||||
| NuPRL NuPRL NuPRL is a higher-order proof development system developed at Cornell University. It was founded by Joseph L. Bates and Robert L. Constable in 1979 and, since then, many have contributed to the development of NuPRL.... |
5 | Cornell University Cornell University Cornell University is an Ivy League university located in Ithaca, New York, United States. It is a private land-grant university, receiving annual funding from the State of New York for certain educational missions... |
Common Lisp Common Lisp Common Lisp, commonly abbreviated CL, is a dialect of the Lisp programming language, published in ANSI standard document ANSI INCITS 226-1994 , . From the ANSI Common Lisp standard the Common Lisp HyperSpec has been derived for use with web browsers... |
||||||
| PVS Prototype Verification System The Prototype Verification System is a specification language integrated with support tools and a theorem prover.It was developed at the Computer Science Laboratory of SRI International in California. PVS is based on a kernel consisting of an extension of Church's theory of types with dependent... |
5.0 | SRI International SRI International SRI International , founded as Stanford Research Institute, is one of the world's largest contract research institutes. Based in Menlo Park, California, the trustees of Stanford University established it in 1946 as a center of innovation to support economic development in the region. It was later... |
Common Lisp Common Lisp Common Lisp, commonly abbreviated CL, is a dialect of the Lisp programming language, published in ANSI standard document ANSI INCITS 226-1994 , . From the ANSI Common Lisp standard the Common Lisp HyperSpec has been derived for use with web browsers... |
||||||
| Twelf Twelf Twelf is an implementation of the logical framework LF. It is used for logic programming and for the formalization of programming language theory.-Introduction:... |
1.7.1 | Frank Pfenning Frank Pfenning Frank Pfenning is a professor of computer science, and adjunct professor in the department of philosophy, at Carnegie Mellon University. He received his Ph.D. from the Carnegie Mellon University Department of Mathematics in 1987, for his dissertation entitled Proof Transformations in Higher-Order... and Carsten Schürmann |
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... |
||||||
Other proof assistants
- CoqCoqIn computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification...
- Which allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification. - HOL theorem proverHOL theorem proverHOL denotes a family of interactive theorem proving systems sharingsimilar logics and implementation strategies....
s - A family of tools ultimately derived from the LCF theorem proverLCF theorem proverLogic 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...
. In these systems the logical core is a library of their programming language. Theorems represent new elements of the language and can only be introduced via "strategies" which guarantee logical correctness. Strategy composition gives users the ability to produce significant proofs with relatively few interactions with the system. Members of the family include:- HOL4 - The "primary descendant". Moscow MLMoscow MLMoscow ML is an implementation of Standard ML.The codebase is derived from Caml Light.The latest release is 2.01. Supported platforms include Unix, Windows, Mac OS and .NET.- External links :*...
based. - HOL Light - A thriving "minimalist fork". OCaml based.
- IsabelleIsabelle theorem proverThe Isabelle theorem prover is an interactive theorem prover, successor of the Higher Order Logic theorem prover. It is an LCF-style theorem prover , so it is based on a small logical core guaranteeing logical correctness...
- With a BSD license. Based on Standard MLStandard MLStandard 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...
. - ProofPower - Went proprietary, then returned to open source. Based on Standard MLStandard MLStandard 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...
.
- HOL4 - The "primary descendant". Moscow ML
- ACL2 - a programming language, a first-order logical theory, and a theorem prover (with both interactive and automatic modes) in the Boyer-Moore tradition.
- Prototype Verification SystemPrototype Verification SystemThe Prototype Verification System is a specification language integrated with support tools and a theorem prover.It was developed at the Computer Science Laboratory of SRI International in California. PVS is based on a kernel consisting of an extension of Church's theory of types with dependent...
(PVS) - a proof language and system based on higher-order logic. - LEGO
- MizarMizar systemThe Mizar system consists of a language for writing strictly formalized mathematical definitions and proofs, a computer program which is able to check proofs written in this language, and a library of definitions and proved theorems which can be referenced and used in new articles. Mizar has goals...
- A proof assistant based on first-order logic, in a natural deduction style, and Tarski-Grothendieck set theoryTarski-Grothendieck set theoryTarski–Grothendieck set theory is an axiomatic set theory that was introduced as part of the Mizar system for formal verification of proofs. Its characteristic axiom is Tarski's axiom . The theory is a non-conservative extension of Zermelo–Fraenkel set theory...
. - PhoXPhoXIn automated theorem proving, PhoX is a proof assistant based on higher-order logic which is eXtensible. The user gives PhoX an initial goal and guides it through subgoals and evidence to prove that goal; internally, it constructs natural deduction trees...
- A proof assistant based on higher-order logic which is eXtensible. - MINLOGMINLOGMINLOG is a proof assistant developed at the University of Munich by the team of Helmut Schwichtenberg.MINLOG is based on first order natural deduction calculus...
- A proof assistant based on first-order minimal logic. - Matita - A light system based on the Calculus of Inductive Constructions.
- Jape - Java based.
- TPS and ETPS - Interactive theorem provers also based on simply-typed lambda calculus, but based on an independent formulationQ0 LogicQ0 is Peter Andrews' formulation of the simply-typed lambda calculus,and provides a foundation for mathematics comparable to first-order logic plus set theory.It is a form of higher-order logic and closely related to the logics of the...
of the logical theory and independent implementation. - Yarrow
- Typelab
User interface
A popular front-end for proof assistants is the EmacsEmacs
Emacs is a class of text editors, usually characterized by their extensibility. GNU Emacs has over 1,000 commands. It also allows the user to combine these commands into macros to automate work.Development began in the mid-1970s and continues actively...
-based Proof General, developed at the University of Edinburgh
University of Edinburgh
The University of Edinburgh, founded in 1583, is a public research university located in Edinburgh, the capital of Scotland, and a UNESCO World Heritage Site. The university is deeply embedded in the fabric of the city, with many of the buildings in the historic Old Town belonging to the university...
.
See also
- Automated theorem provingAutomated theorem provingAutomated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
- Computer-assisted proofComputer-assisted proofA computer-assisted proof is a mathematical proof that has been at least partially generated by computer.Most computer-aided proofs to date have been implementations of large proofs-by-exhaustion of a mathematical theorem. The idea is to use a computer program to perform lengthy computations, and...
- Proof verification
- QED manifesto
- Satisfiability Modulo TheoriesSatisfiability Modulo TheoriesIn computer science, the Satisfiability Modulo Theories problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality...
External links
- "Introduction" in Certified Programming with Dependent Types.
- Introduction to the Coq Proof Assistant (with a general introduction to interactive theorem proving)
- Interactive Theorem Proving for Agda Users
Catalogues
- Digital Math by Category: Tactic Provers
- Automated Deduction Systems and Groups
- Theorem Proving and Automated Reasoning Systems
- Database of Existing Mechanized Reasoning Systems
- NuPRL: Other Systems
- Specific Logical Frameworks and Implementations
- DMOZ: Science: Math: Logic and Foundations: Computational Logic: Logical Frameworks