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
(p ---> (q ---> r)) <---> ((p & q) ---> r)where ---> and <---> are meant to be the traditional arrows denoting logical implication and logical equivalence.
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
(implies hyp
concl)
then we say that formula is an implication, that hyp is the hypothesis, and
that concl is the conclusion. If the hypothesis is an and expression, as in
(implies (and hyp1
hyp2
...)
concl)
then we call hyp1 is the first hypothesis,
hyp2 is the second hypothesis, etc.If a term is of the form
(and term1 term2 ...)we say it is a conjunction and that term1 is the first conjunct, term2 is the second conjunct, etc. We treat an
or-term analogously but call it a
disjunction and its arguments are disjuncts.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:
Double 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)))
There are, of course, many others, even with these same names! For example, there is a
dual version of DeMorgan showing how 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
formula1: (IMPLIES P (IMPLIES Q R)) formula2: (IMPLIES (AND P Q) R)then we wish to test the formula
(IFF formula1 formula2):
P Q R formula1 formula2 (IFF formula1 formula2) --------- 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 TSo we see that the formula always returns
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 sigma above)
is always true:
(iff (implies (endp z) formula1'
(implies (true-listp z)
(equal (rev (rev z)) z)))
(implies (and (endp z) formula2'
(true-listp z))
(equal (rev (rev z)) z))).
Thus, if we're trying to prove formula1' it is permitted to try to
to prove formula2' instead, because they return the same truthvalue.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.
That is what Double Negation says.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.
