Guiding the ACL2 Theorem Prover

Now that you have seen the theorem prover in action you might be curious as to how you guide it.

Look at the picture above. It is meant to suggest that *Q* is an
important lemma needed for the proof of *P*. Note that to lead the
prover to the proof of *P* the user first proves *Q*. In a way, the
formulation and proof of *Q* is a hint to the prover about how to prove
*P*.

The user usually doesn't think of *Q* or recognize the need to prove
it separately until he or she sees the theorem prover **fail** to prove
*P* without it ``knowing'' *Q*.

The way the user typically discovers the need for *Q* is to look at
failed proofs.