**Automated theorem proving** (**ATP**) or **automated deduction**, currently the most well-developed subfield of *automated reasoning* (AR), is the proving of mathematical theorems by a computer program.

Depending on the underlying logic, the problem of deciding the validity of a formula varies from trivial to impossible. For the frequent case of propositional logic, the problem is decidable but NP-complete, and hence only exponential-time algorithms are believed to exist for general proof tasks. For a first order predicate calculus, with no (“proper”) axioms, Gödel’s completeness theorem states that the theorems (provable statements) are exactly the logically valid well-formed formulas, so identifying valid formulas is recursively enumerable: given unbounded resources, any valid formula can eventually be proven.

However, *invalid* formulas (those that are *not* entailed by a given theory), cannot always be recognized.

A simpler, but related, problem is proof verification, where an existing proof for a theorem is certified valid. For this, it is generally required that each individual proof step can be verified by a primitive recursive function or program, and hence the problem is always decidable.

### Some techniques for theorem proving

- First-order resolution with unification
- Lean theorem proving
- Model elimination
- Method of analytic tableaux
- Superposition and term rewriting
- Model checking
- Mathematical induction
- Binary decision diagrams
- DPLL
- Higher-order unification

————————————

## Further reading

## How to make it as easily as possible?

A **lean theorem prover** is an automated theorem prover implemented in a minimum amount of code. Lean provers are generally^{[citation needed]} implemented in Prolog, and make proficient use of the backtracking engine and logic variables of that language. Lean provers can be as small as a few hundred bytes of source code.

The following is a small Prolog implementation:

propexp=

not_(propexp);

or_(propexp,propexp);

and_(propexp,propexp);

implies_(propexp,propexp);

s_(symbol); a ; b ; c.

**The beef is that this procedural definition for a theorem can be converted into an atomistic model so that each domain will be transformed into a symbolic element. **

**Therefore**, proving the theorem means running the top element of the theorem. The principle is exactly the same as in source code simulation (see SimulationWare).

When those variable a, b and c will be captured from the original code, this work will enable proving source code sequences written in Java or similar languages.

### Some links:

- http://en.wikipedia.org/wiki/Lean_theorem_prover
- http://en.wikipedia.org/wiki/Automated_theorem_proving

## Leave a comment

Comments feed for this article