## What is a Mechanical Theorem Prover?

A **mechanical theorem prover** is a computer program that finds
proofs of theorems.

The ideal mechanical theorem prover is **automatic**: you give
it a formula and it gives you a proof of that formula or tells you
there is no proof.

Unfortunately, automatic theorem provers can be built only for very
simple logics (e.g., **propositional calculus**) and even then
practical considerations (e.g., how many
centuries you are willing to wait) limit the problems they can solve.