Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

Six built-in proof techniques are used by ACL2 to decompose the goal formula into subgoals.

*simplification* -- decision procedures and rewriting with previously
proved rules, but actually including a host of other techniques under your
control. Simplification is the only proof technique that can reduce a
formula to 0 subgoals (i.e., prove it) rather than just transform it to other
formulas. The predominant activity in most proofs is simplification. There
are many ways you can affect what the simplifier does to your formulas.
Good users spend most of their time thinking about how to control the
simplifier.

*destructor elimination* -- getting rid of ``destructor terms'' like
`(CAR X)`

and `(CDR X)`

by replacing a variable, e.g., `X`

, by a
``constructor'' term, e.g., `(CONS A B)`

. But you can tell ACL2 about new
destructor/constructor combinations.

*cross-fertilization* -- using an equivalence hypothesis by substituting
one side for the other into the conclusion
*and then throwing the hypothesis away*.
This is a heuristic that helps use an inductive hypothesis and prepare for
another induction.

*generalization* -- replacing a term by a new variable and restricting
the new variable to have some of the properties of the term. You can
control the restrictions imposed on the new variable. This is a heuristic
that prepares the goal for another induction.

*elimination of irrelevance* -- throwing away unnecessary hypotheses.
This is a heuristic that prepares the goal for another induction.

*induction* -- selecting an induction scheme to prove a formula. Inductions
are ``suggested'' by the recursive functions appearing in the formula. But you
can control what inductions are suggested by terms.

But you can add additional techniques, called *clause processors*.

The various techniques are tried in turn, with simplification first and
induction last. Each technique reports one of three outcomes: it found
nothing to change (i.e., the technique doesn't *apply* to that subgoal),
it decided to abort the proof attempt (typically because there is reason to
believe the proof is failing), or it decomposed the goal into *k*
subgoals.

The last outcome has a special case: if *k* is 0 then the technique proved
the goal. Whenever *k* is non-0, the process starts over again with
simplification on each of the *k* subgoals. However, it saves up all the
subgoals for which induction is the only proof technique left to try. That
way you see how it performs on every base case and induction step of one
induction before it launches into another induction.

It runs until you or one of the proof techniques aborts the proof attempt or until all subgoals have been proved.

Note that if simplification produces a subgoal, that subgoal is
re-simplified. This process continues until the subgoal cannot be
simplified further. Only then is the next proof technique is tried. Such
suboals are said to be *stable under simplification*.

While this is happening, the prover prints an English narrative describing the process. Basically, after each goal is printed, the system prints an English paragraph that names the next applicable proof technique, gives a brief description of what that technique does to the subgoal, and says how many new subgoals are produced. Then each subgoal is dealt with in turn.

If the proof is successful, you could read this log as a proof of the conjecture. But output from successful proofs is generally never read because it is not important to The Method described in introduction-to-the-theorem-prover.

The output of an unsuccessful proof attempt concludes with some *key*
*checkpoints* which usually bear looking at.