Automated proof checking

From Wikipedia, the free encyclopedia

This article is in need of attention from an expert on the subject. WikiProject Mathematics or the Mathematics Portal may be able to help recruit one. (February 2009)

Automated proof checking is the process of using software for checking proofs for correctness. It is one of the most developed fields in automated reasoning.

Automated proof checking differs from automated theorem proving in that automated proof checking simply mechanically checks the formal workings of an existing proof, instead of trying to develop new proofs or theorems itself. Because of this, the task of automated proof verification is much simpler than that of automated theorem proving, allowing automated proof checking software to be much simpler than automated theorem proving software.

Automated proof checking can be done as a batch operation or as part of interactive theorem proving.

Contents 1 Example 2 Incomplete alphabetic list of proof checking systems 3 See also 4 External links

[edit] Example

An early example of a computable function for automated proof checking can be found in (Gödel 1931), page 186, definition 44, of the function isProofFigure(x) which returns 0 (true) if x is a correct proof and 1 (false) otherwise. The proof x must be represented as a natural number using Gödel numbering.

Another example is definition 45 (Gödel 1931) of proofFor(x,y) which returns 0 (true) if x is a correct proof of the theorem y.

[edit] Incomplete alphabetic list of proof checking systems

Since the construction of the first digital computers, many systems have been constructed for automated proof checking. The following is a vastly incomplete list of systems whose functionality include automatic proof checking.

• Automath
• HOL Light
• Logiweb
• Metamath
• Mizar

[edit] See also

• Computer-aided proof
• Formal verification

[edit] External links

• 1931, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. Monatshefte für Mathematik und Physik 38: 173-98.
  • Hirzel, Martin, 2000, On formally undecidable propositions of Principia Mathematica and related systems I.. A modern translation by the author.
• Julie Rehmeyer (Friday, November 14th, 2008). "How to (really) trust a mathematical proof". ScienceNews. http://www.sciencenews.org/view/generic/id/38623/title/How_to_(really)_trust_a_mathematical_proof. Retrieved 2008-11-14. 
• Metamath: a proof checking system with an extensive collection of machine-readable proofs covering a considerable range of mathematical fields

This artificial intelligence-related article is a stub. You can help Wikipedia by expanding it. v • d • e

This mathematics-related article is a stub. You can help Wikipedia by expanding it. v • d • e