Interactive theorem proving
Encyclopedia
In computer science
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

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

     - 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 prover
    HOL theorem prover
    HOL denotes a family of interactive theorem proving systems sharingsimilar logics and implementation strategies....

    s - A family of tools ultimately derived from the LCF theorem prover
    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...

    . 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 ML
      Moscow ML
      Moscow 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.
    • Isabelle
      Isabelle theorem prover
      The 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 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...

      .
    • ProofPower - Went proprietary, then returned to open source. Based on 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...

      .
  • 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 System
    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...

     (PVS) - a proof language and system based on higher-order logic.
  • LEGO
  • Mizar
    Mizar system
    The 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 theory
    Tarski-Grothendieck set theory
    Tarski–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...

    .
  • PhoX
    PhoX
    In 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.
  • MINLOG
    MINLOG
    MINLOG 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 formulation
    Q0 Logic
    Q0 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 Emacs
Emacs
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 proving
    Automated theorem proving
    Automated 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 proof
    Computer-assisted proof
    A 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 Theories
    Satisfiability Modulo Theories
    In 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


Catalogues
The source of this article is wikipedia, the free encyclopedia.  The text of this article is licensed under the GFDL.
 
x
OK