A brief explanation of propositional calculus
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
is equivalent to:
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,
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
(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
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 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
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
propositional calculus will convert it to
Many users are surprised that the first conjunct above does not have
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:
The formula above is a tautology. It contains three variables,
formula1: (IMPLIES P (IMPLIES Q R)) formula2: (IMPLIES (AND P Q) R)
then we wish to test the formula
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 T
So we see that the formula always returns
Recall that in the original example at the top of this page we were trying to prove the formula
This formula is an
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:
is always true no matter what Boolean values
(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
A very simple example of this is with Double Negation.
is a tautology. This means that if we were trying to prove
we could transform it to
(implies p ...).
But if we were trying to prove:
we could not prove it by using Double Negation! The formula above claims
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.