Automated proof checking

From Infogalactic: the planetary knowledge core
(Redirected from Proof checking)
Jump to: navigation, search

Lua error in package.lua at line 80: module 'strict' not found.

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.

Because of this small size, some automated proof checking systems can have less than a thousand lines of core code, and are thus themselves amenable to both hand-checking and automated software verification.

The Mizar system, HOL Light, and Metamath are examples of automated proof checking systems.

Automated proof checking can be done either as a batch operation, or interactively, as part of an interactive theorem proving system.

Field journals and conferences

See also

External links

  • Lua error in package.lua at line 80: module 'strict' not found.
  • Metamath: a proof checking system with an extensive collection of machine-readable proofs covering a considerable range of mathematical fields
  • Digimath: Freek Wiedijk's alphabetic list of systems
  • MathSystem: Mathematical Software systems


<templatestyles src="Asbox/styles.css"></templatestyles>

<templatestyles src="Asbox/styles.css"></templatestyles>