Background knowledge in ACL2 logic for theorem prover tutorial

You might think that in order to use the theorem prover you have to know the mathematical logic supported by ACL2. But you need to know a lot less about it than you might think.

Technically, a theorem is a formula that can be derived from axioms by using rules of inference. Thus, to do a proof you have to know (a) the syntax of formulas, (b) the axioms, and (c) the rules of inference. Traditionally, these things are spelled out in excruciating detail in treatments of mathematical logic — and for good reason.

The whole point of proving theorems is that it is a way to determine that a
formula is ``always true'' (under some model of the axioms). By ``always
true'' we actually mean what logicians mean when they say the formula is
*valid*: true in the model, for all possible values of the variables.
Here by ``model of the axioms'' we mean an understanding of the meaning of the
various function symbols so that the axioms are true for all values of the
variables. If the variables in your conjecture can take on an infinite number
of values, proof is often the **only** way to determine that a conjecture
is ``always true.'' So if proof is being used to determine that a
questionable formula is always true the proof must be carried out flawlessly.
Thus, the (a) syntax, (b) axioms, and (c) rules of inference must be described
precisely and followed to the letter.

But formal mathematical logic was invented to explain how people reason. To the extent that logic mimics human reasoning, proofs can be seen as just extremely carefully crafted arguments. Given that ACL2 is responsible for following the rules ``to the letter,'' your main job is ``explain'' the big leaps.

To use the theorem prover you must understand (a) the syntax, because you must be able to write formulas flawlessly. But you don't have to know (b) the axioms and (c) the rules of inference at nearly the same level of precision, as long as you understand the basic structure and language of proofs.

Below is part of a proof of a certain theorem. You ought to be able to
understand the following. Since what we describe is a proof of one case of
the formula, we hope that you're *convinced* that the formula holds for
that case.

Read this and follow the links to confirm that you understand what happens.
Be sure to then use your browser's **Back Button** to return to this page
and continue.

**An Annotated Proof of**

(implies (true-listp z) (equal (rev (rev z)) z))

``We will prove that reversing the reverse of a

The

(implies (endp z) (implies (true-listp z) (equal (rev (rev z)) z))).

This formula is equivalent, by

(implies (and (endp z) (true-listp z)) (equal (rev (rev z)) z))

(implies (and (not (consp z)) (true-listp z)) (equal (rev (rev z)) z))

(implies (and (not (consp z)) (equal z nil)) (equal (rev (rev z)) z))

Then using the second *hypothesis*, just

(implies (and (not (consp z)) (equal z nil)) (equal (rev (rev nil)) nil))

Since the *conclusion* involves no variables, we can

(implies (and (not (consp z)) (equal z nil)) T)

But this is an

Now it is time for a little quiz. There are just three questions.

**Q1**: The case above was the Base Case of an inductive proof of

(implies (true-listp z) (equal (rev (rev z)) z))

in which we did induction on the structure of the linear list

Below are four commonly given answers; choose one. Then look

Induction Step -- Choice (i): (implies (not (endp z)) (implies (true-listp z) (equal (rev (rev z)) z)))Induction Step -- Choice (ii): (implies (true-listp (cdr z)) (equal (rev (rev (cdr z))) (cdr z)))Induction Step -- Choice (iii): (implies (and (not (endp z)) (equal (rev (rev (cdr x))) (cdr x))) (implies (true-listp z) (equal (rev (rev z)) z)))Induction Step -- Choice (iv): (implies (and (not (endp z)) (implies (true-listp (cdr z)) (equal (rev (rev (cdr z))) (cdr z)))) (implies (true-listp z) (equal (rev (rev z)) z)))

**Q2**: To prove the Induction Step we must prove one or more of the
goals below.

Which combinations are sufficient to imply the Induction Step? Decide what
is required and then look

Induction Step: (implies (andc(impliesp'q')) (impliespq))

and beside each candidate subgoal we show its structure in those terms.

Subgoal (i): (implies (and (not (endp z)) ; (implies (andc(true-listp z)) ;p) (true-listp (cdr z))) ;p')Subgoal (ii): (implies (and (not (endp z)) ; (implies (andc(true-listp z) ;p(equal (rev (rev (cdr z))) (cdr z))) ;q') (equal (rev (rev z)) z)) ;q)Subgoal (iii): (implies (and (not (endp z)) ; (implies (andc(equal (rev (rev (cdr z))) (cdr z))) ;q') (equal (rev (rev z)) z)) ;q)Subgoal (iv): (implies (and (not (endp z)) ; (implies (andc(true-listp (cdr z)) ;p'(equal (rev (rev (cdr z))) (cdr z))) ;q') (equal (rev (rev z)) z)) ;q)

**Q3**: Suppose you know the theorem

Theorem: (implies (p (f x)) (equal (g (h x)) x))

and you wish to rewrite the target

Goal Conjecture: (implies (and (q (f a)) (r a)) (s (g (h a))))

What must you prove to relieve the hypothesis of *Theorem*?

After you've thought about it, look

**End of the Quiz**

If this page made sense, you're ready to read the introduction to the theorem prover.

If you are reading this as part of the tutorial introduction to the theorem
prover, use your browser's **Back Button** now to return to introduction-to-the-theorem-prover.