Child pages
  • CSU 290 (Spring 2008)

Versions Compared

Key

  • This line was added.
  • This line was removed.
  • Formatting was changed.

...

All that's missing now is Lemma 4, that says that (rev b) is a true list for any b. I left it as an exercise for you to prove for next time.

...

April 9: Topics for Exam #6

Topics covered include everything we have learned about the ACL2s theorem prover, lectures 25 to 29 on the web page; of course, you should not forget the basics of proving theorems.

Here are the main things we will test.

  1. Understanding ACL2s proof attempts
    That was the largest component of these last two weeks.
    In particular, understand the waterfall model (cf lecture 25), and be able to extract lemmas to be proved when ACL2s is stuck on a proof.
  2. Understand rewriting
    Cf lecture 26 and the textbook, and see below.
  3. Understand decision procedures for propositional reasoning and congruence closure
    Cf lecture 29 and see below.

Rewriting

Recall that when you prove a theorem (possibly with hypotheses) with a conclusion of the form LHS = RHS, this defines a rewrite rule that rewrites occurrences of LHS into RHS. (Note the direction!) Variables in the LHS are taken to be placeholders, that can be substituted for when rewriting happens.

The sequencing of rewrites when rewriting happens is important. The two main rules are:

  1. Rewriting occurs for inner expressions before outer expressions. Thus, if you have an expression (f (g x)), the rewriter will attempt to rewrite (g x) first, and then attempt to rewrite (f ...).
  2. Rewriting occurs with the latest rewrite rules defined tried first, all to way to the oldest rewrite rules. In other words, if two (or more) rewrite rules are applicable to a given expression, the most recently admitted rewrite rule is used.

Decision Procedure for Propositional Reasoning

How does ACL2s decided whether a Boolean expression is a tautology or not? It could build a truth table, but it doesn't. (Well, actually, it almost does - it just uses a more efficient representation than a truth table, that contains essentially the same information.) Here's how it does it. For simplicity, here, I will only consider the case where there are no occurrence of functions others than implies, and, not, and or in the Boolean expression. (It's an interesting exercise to figure out what happens when you do allow other functions.)

First, it rewrites the Boolean expression so that it does not contain any implies, and, or, and not. It does so by replacing every occurrence of those functions by a corresponding if expression. Here are the replacements:

No Format

(implies X Y) -> (if X Y t)
(and X Y) -> (if X Y nil)
(or X Y) -> (if X t Y)
(not X) -> (if X nil t)

(Convince yourself that these are correct by trying out a few examples, that is, seeing whether (or t nil) evaluates to t when replaced by the corresponding if expression, etc.)
Thus, for example:

No Format

(and (not a) a) = (if (if a nil t) a nil)     # expanding out and and not

Once that is done, you are left with a bunch of if expressions. For reasons that will become clear, we want to simplify the condition of those if expressions as much as possible. In particular, we want all if to have simple variables as conditions. To do so, we will apply the following transformation to an if expression that has a non-variable as a condition. (If it's not a variable, it has to be an if expression itself.)

No Format

(if (if X Y Z) V W) -> (if X (if Y V W) (if Z V W))

(Convince yourself that you understand why applying this transformation does not change the value returned by the whole expression.)
Do this repeatedly until all if expressions have a variable (or t or nil) as a condition.
Continuing our example above:

No Format

(and (not a) b) = (if (if a nil t) a nil)    # expanding out and and not
                = (if a                      # applying transformation above
                      (if nil a nil)
                    (if t a nil))

Now, let's simplify things further.
First, take every if expression, from the outermost to the innermost:

  1. if the expression is of the form (if t X Y), replace it by X, and repeat going into X.
  2. if the expression is of the form (if nil X Y), replace it by Y, and repeat going into Y.
  3. if the expression is of the form (if v X Y), where v is a variable, replace every occurrence of v in X by t and every occurrence of v in Y by nil, and repeat (going into X and Y).

Continuing our example:

No Format

(and (not a) b) = (if (if a nil t) a nil)    # expanding out and and not
                = (if a                      # applying transformation above
                      (if nil a nil)
                    (if t a nil))
                = (if a                      # replacing a by t in THEN clause 
                      (if nil t nil)
                    (if t a nil))
                = (if a                      # replacing a by nil in ELSE clause
                      (if nil t nil)
                    (if t nil nil))
                = (if a                      # (if nil t nil) -> nil
                      nil                 
                    (if t nil nil))
                = (if a nil nil)             # (if t nil nil) -> nil

When you're done all of this, you have an expression with only if expressions and with the property that for any "path" through the conditionals, you encounter every variable only once, in the condition of an if. A Boolean expression is a tautology exactly when every "path" through the conditionals lead to a value that is guaranteed to be non-nil.

If a branch has a return value that is not guaranteed to be non-nil (for instance, it is nil, or it is a variable), you can read off a counter example (that is, an assignment of truth values to variables that makes the Boolean expression false) by looking at the "path" through the conditionals that led to the values that is not guaranteed to be non-nil, setting a variable to t if you ended up going to the THEN branch of the conditional, or to nil if you ended up going to the right branch of the conditional.

Thus, in the above example, we ended up with (if a nil nil); there are two "paths" into this conditional that lead to a value not guaranteed to be non-nil. One of those "path" is obtained by setting a to t, and the other is obtained by setting a to nil. It's easy to check that both of those assignments to a are counterexamples to the initial expression being a tautology.

For a more complex example, consider (implies (or (not a) b) (or a (not b))).
If you work through the above steps, you get the simplified form (if a (if b t t) (if b nil t)). There is one "path" in the conditionals that lead to a value not guaranteed to be non-nil, and that's the "path" that leads to the nil, which is obtained by setting a to nil and setting b to t. And you can check that a=nil,b=t is a counterexample to the initial conjecture.

Decision Procedure for Equivalences

Coming soon