Automated-Therom Proving

Automated-Therom proving is the proving of correctness of mathematical theorems using computer programs. The specific logic used in ATP (automated-theorem proving) may cause the problem to range from trivial to impossible. If first-order logic is used, then proving theorems is recursively enumerable, i.e. any valid theorem can eventually be proven.

Related to ATP is the problem of proof verification. This is where an existing proof of a theorem is proven valid.

nteractive theorem provers are ones in which a user is required to give 'hints' to the system. Although automatic theorem provers have been able to prove hard problems, these are rare and in general interactive theorem provers are more equipped to prove the harder problems. Though, this success depends on the proficiency of the user.

Theorem proving in general is using a set of basic axioms and inference rules in order to prove a theorem either backwards, forwards or both. There are other techniques of theorem proving, such as brute force theorem proving which checks against many states, and hybried theorem proving which use model checking as an inference rule.

Provers may also be written to prove specific problems. Examples of this include the four-colour theorem and a win for the first player in connect 4 using perfect play.

A specific theorem prover inplemented in Prolog is a lean theorem prover called leanCoP.