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

It is impossible in this short introduction to teach you propositional calculus if you don't already know it!

A typical use of propositional calculus is to observe that

(implies (endp z) (implies (true-listp z) (equal (rev (rev z)) z)))is equivalent to:

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

If this is surprising and you know propositional calculus, then the problem might be our notation. We're exploiting the tautology

where(p ---> (q ---> r)) <---> ((p & q) ---> r)

If you don't know propositional calculus, we'll say just a few things to help ease your journey.

A *propositional formula*, in ACL2, is any formula
written entirely in terms of variable symbols, `T`

, `NIL`

, and
the propositional functions `AND`

, `OR`

, `NOT`

, `IMPLIES`

, and
`IFF`

. The ``tautology'' above in traditional notation is this
propositional formula in ACL2:

(IFF (IMPLIES P (IMPLIES Q R)) (IMPLIES (AND P Q) R)).

If you have a formula like

(impliesthen we say that formula is anhypconcl)

`and`

expression, as in
(implies (andthen we callhyp1hyp2...)concl)

If a term is of the form

(andwe say it is aterm1term2...)

`or`

-term analogously but call it a
A *tautology* is any propositional formula that can be proved by testing it
under all combinations of Boolean assignments to its variables. We give an
example of such a *truth-table proof* below, but hasten to add that ACL2
does not generally use truth tables to recognize tautologies. It primarily uses
`IF`

-normalization and BDDs to recognize tautologies, which can be seen as a
mix of symbolic manipulation and case analysis.

Many tautologies have names, but ACL2 doesn't refer to them by name because it derives them from first principles. We list a few here because we sometimes use the names in our documentation; more importantly, you should look at these formulas and convince yourself that they're always true for all Boolean values of the variables:

There are, of course, many others, even with these same names! For example, there is a dual version of DeMorgan showing howDouble Negation: (iff (not (not p)) p)DeMorgan: (iff (not (and p q)) (or (not p) (not q)))Distributivity: (iff (and p (or q r)) (or (and p q) (and p r)))Promotion: (iff (implies p (implies q r)) (implies (and p q) r))Implicative Disjunction: (iff (implies p q) (or (not p) q))Contrapositive: (iff (implies p q) (implies (not q) (not p)))Generalized Contrapositive: (iff (implies (and p r) q) (implies (and p (not q)) (not r)))

`not`

distributes over `or`

, a dual version of
Distributivity for `or`

over `and`

, etc.Dealing with propositional calculus will not generally be a problem for you because
it is decidable and ACL2 has procedures that decide propositional formulas. However,
propositional calculus can lead to exponential explosion and can thus explain why
ACL2 has ``gone out to lunch.'' In addition, sometimes if you are curious as to
*why* ACL2 is working on a certain subgoal the reason can be traced back to
propositional calculus.

The most common example of this is that to prove a formula of the form

(implies (implies p1 q1) (implies p2 q2))propositional calculus will convert it to

(and (implies (and p2 (not p1)) q2) (implies (and p2 q1) q2))Many users are surprised that the first conjunct above does not have

`q1`

as a
hypothesis. If you ever stare at an ACL2 goal and say to yourself ``A hypothesis is
missing!'' the chances are that propositional calculus is ``to blame.''
In particular, if you are trying to prove that `(implies p1 q1)`

implies something,
you must deal with the case that `(implies p1 q1)`

is true because `p1`

is false.
Think about it.Now we illustrate the truth table method for deciding tautologies, even though that is not what ACL2 generally uses. Consider the formula called Promotion above:

(IFF (IMPLIES P (IMPLIES Q R)) (IMPLIES (AND P Q) R))

The formula above is a tautology. It contains three variables, `P`

, `Q`

,
and `R`

, and so there are 8 combinations of Boolean assignments to them.
If we let

then we wish to test the formulaformula1: (IMPLIES P (IMPLIES Q R))formula2: (IMPLIES (AND P Q) R)

`(IFF `

`)`

:
P Q RSo we see that the formula always returnsformula1formula2(IFFformula1formula2) --------- T T T T T T T T NIL NIL NIL T T NIL T T T T T NIL NIL T T T NIL T T T T T NIL T NIL T T T NIL NIL T T T T NIL NIL NIL T T T

`T`

and is thus a tautology.Recall that in the original example at the top of this page we were trying to prove the formula

(implies (endp z) (implies (true-listp z) (equal (rev (rev z)) z)))This formula is an instance of

(implies p (implies q r)).The substitution required by the match is

sigma: ((p (endp z)) (q (true-listp z)) (r (equal (rev (rev z)) z)))

Since we know the tautology:

(iff (implies p (implies q r)) (implies (and p q) r)).is always true no matter what Boolean values

`p`

, `q`

, and `r`

have,
then we know this instance of it (obtained by applying the substitution (iff (implies (endp z)Thus, if we're trying to proveformula1'(implies (true-listp z) (equal (rev (rev z)) z))) (implies (and (endp z)formula2'(true-listp z)) (equal (rev (rev z)) z))).

This sketch of propositional reasoning in ACL2 is a little suspect because
we didn't address the possibility that the substitution might replace the
propositional variables by non-propositional terms. But the tautology was
verified only on Boolean values for those variables. This actually
works out because in ACL2 all propositional testing is done against `nil`

and any non-`nil`

value, including `t`

, is as good as another. However,
the tautology allows us to replace one formula by the other only in contexts
in which we just care about propositional truth, i.e., whether the formula
is `nil`

or not. When we prove a formula in ACL2 we are really
establishing that it never returns `nil`

, i.e., no matter what the values
of the variables, the value of the formula is non-`nil`

.

A very simple example of this is with Double Negation.

(iff (not (not p)) p)is a tautology. This means that if we were trying to prove

(implies (not (not p)) ...)we could transform it to

(implies p ...).But if we were trying to prove:

(equal (not (not p)) p)we could not prove it by using Double Negation! The formula above claims that

`(not (not p))`

and `p`

have identical values.
They do not! For example, `(not (not 3))`

is `t`

, not `3`

.
However, `(not (not 3))`

and `t`

are propositionally equivalent (i.e.,
satisfy `iff`

) because one is as good as the other in a test.
As long as you only use propositional formulas in propositional places this aspect of ACL2 should not affect you.

Now please use your browser's **Back Button** to return to the
example proof in logic-knowledge-taken-for-granted.