## 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.