		Search-engine friendly clone of the ACL2 documentation.

Introduction-to-the-theorem-prover

Architecture-of-the-prover

A simple overview of how the prover works

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.
fertilization — using an equivalence hypothesis by substituting one side for the other in the goal. When under induction, ACL2 may decide to restrict the substitution as follows, using its so-called cross-fertilization heuristic: substitute only into one side of the conclusion, thus using an inductive hypothesis in preparation for possible generalization in advance of another induction. Note that cross-fertilization is used only when generalization is enabled: with the hint :do-not '(generalize), only full fertilization is applied.
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 subgoals 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.

For more information about how ACL2 orchestrates its proof techniques, see hints-and-the-waterfall.