Child pages
  • CSU 290 (Spring 2008)
Skip to end of metadata
Go to start of metadata

You are viewing an old version of this page. View the current version.

Compare with Current View Page History

« Previous Version 7 Next »

This is the resource page for Section 2 of Logic and Computation, CSU 290 (Spring 2008). Welcome.

The purpose of this page is to simply complete the lectures, partly to keep us in sync with the other section, partly because there is only so much time and much interesting things to discuss.

These notes are meant to supplement the lectures, the readings and the lecture notes (available on the course web site) and not replace them.

Feel free to comment at the bottom of the page if you have any questions or anything is unclear. (Select "Add Comment" under "Add Content" down below.) I will generally merge your comments and questions into the main text when I get to them.

What you should do right now: Make sure you are logged into the wiki. (Select "Log In" under "Your Account" below if not, use you CCIS credentials to log in.) Look at the bottom of the page, under "Other Features", top right icon is an envelope. Press that button. That will register you as watching this page. Basically, every time the page changes, you get an email saying so. Keeps you from having to check the page regularly.

February 15: Formal proof for ~(t=nil)

Here is a complete formal proof for ~(t=nil) using the axioms I gave in class. (This is the proof that I started on Monday, but ran out of time 5 steps into the proof.)

You should be able to understand all the steps in that proof, if not be able to come up with the proof yourself. We will not ask you to come up with these kind of formal proofs in this course. Instead, we will use the more informal "chain of equals" or "chain of relations" approach I presented in class.

In the proof below, I write ~A for "not A" and A & B for "A and B".

1. ~(equal (car (cons x y) x) x) = nil        [ axiom for equal/car/cons 
2. ~(equal (car (cons a b) a) a) = nil)       [ instantiation of 1 with x->a, y->b 

Okay, so 2 is something we will use later on. Let's remember it.

3. ~(x = y) => (equal x y) = nil              [ axiom for equal 
4. ~(car (cons a b)) = a =>
         (equal (car (cons a b)) a) = nil     [ instantiation of 3 with x->(car (cons a b)), y->a 
5. ~(~(car (cons a b)) = a)                   [ by MT applied to 4 and 2 
6. ~(~A) => A                                 [ tautology of Boolean logic 
7. ~(~(car (cons a b)) = a) =>
      (car (cons a b)) = a                    [ instantiation of 6 with A->(car (cons a b)) 
8. (car (cons a b)) = a                       [ by MP applied to 7 and 5 
9. x=y => (equal x y) = y                     [ axiom for equal 
10. (car (cons a b)) = a =>
        (equal (car (cons a b)) a) = t        [ instantiation of 9 with x->(car (cons a b)),y->a 
11. (equal (car (cons a b)) a) = t            [ by MP applied to 10 and 8

Excellent. So now we can see that 2 and 11 together essentially give us that t /= nil.
We just have to work some to get that to come out of the proof.

12. (A & B => C) => (A & ~C => ~B)            [ tautology of Boolean logic (check it!) 
13. ((equal (car (cons a b)) a) = t
      & t = nil => 
          (equal (car (cons a b)) a) = nil))  [ instantiation of 12 with 
     => ((equal (car (cons a b)) a) = t       [  A->(equal (car (cons a b)) a) = t
        & ~(equal (car (cons a b)) a) = nil)) [  B->(t=nil)
             => ~(t = nil))                   [  C->(equal (car (cons a b)) a) = nil 
14. x = y & y = z => x = z                    [ axiom of transitivity 
15. (equal (car (cons a b)) a) = t            [ instantiation of 14 with 
     & t = nil =>                             [   x->(equal (car (cons a b)) a)
         (equal (car (cons a b)) a) = nil     [   y->t  and z->nil
16. (equal (car (cons a b)) a) = t            [ by MP applied to 13 and 15
    & ~(equal (car (cons a b)) a) = nil
          => ~(t = nil)

And we are just about done. We have both antecedents of the implication in 16.

17. ~(t=nil)                                  [ by MP applied to 16, 11, and 2

February 20: Review of Proving Theorems

Here is what we have seen until now as far as proving theorems are concerned.

We reviewed Boolean logic and the concept of a tautology of Boolean logic. Recall that a tautology is just a Boolean formula that is always true, irrespectively of the truth values you give to the Boolean variables in the formula.

We shall take Boolean (aka propositional) reasoning for granted.

We introduced the ACL2 logic, as essentially Boolean logic augmented with the ability to reason about basic formulas of the form EXP1 = EXP2, where EXP1 and EXP2 are ACL2 expressions.

The ACL2 logic is defined formally using the following axioms and rules of inferences:

  • Every tautology of Boolean logic is an axiom
  • x = x (reflexivity)
  • x = y => y = x (symmetry)
  • x = y /\ y = z => x = z (transitivity)
  • x1 = y1 /\ ... /\ xn = yn => (f x1 ... xn) = (f y1 ... yn) for every function symbol f of arity n
  • From F derive F/s (where F is an arbitrary formula, and s is a substitution of ACL2 expressions for free variables in F)
  • From F and F => G derive G (modus ponens)

We also have axioms corresponding to the different primitives of the language. The basic ones are:

  • x = y => (equal x y) = t
  • x /= y => (equal x y) = nil (where /= represents "not equal to")
  • x = nil => (if x y z) = z
  • x /= nil => (if x y z) = x
  • (car (cons x y)) = x
  • (cdr (cons x y)) = y
  • consp (cons x y) = t
  • consp (nil) = nil
  • (integerp x) = t => (consp x)=nil

Additionally, we can take as axioms the basic properties of arithmetic that you have seen in high school and discrete maths. Thus, when proving theorems, you will be free to perform standard simplification of arithmetic.

A formal proof of F is a sequence of formulas such that every formula in the sequence is either an axiom or derived from previous formulas using an inference rule, and such that the last formula of the sequence is F itself.

I gave you a formal proof of t /= nil above. We shall not write a lot of formal proof, and you certainly will not have to write any of them.

Instead, we shall use some proof techniques to prove formulas that have a certain form. These techniques do not work for all formulas, but they work for enough of them to be interesting.

If the formula you want to prove is of the form EXP1 = EXP2, then one technique is to use a sequence of equalities to equate EXP1 and EXP2:


where all the equalities are justified using the axioms or the inference rules above. By transitivity of =, this clearly shows that EXP1 = EXP2.

Alternatively, it is sometimes easier to simplify both EXP1 and EXP2 into a common expression EXP3.



Again, it should be pretty clear that this proves that EXP1 = EXP2. (By transitivity of = once again.)

If the formula you want to prove is of the form HYPS => EXP1 = EXP2, where HYPS is some hypotheses (formulas), then you can use a variant of the above, that is, prove that EXP1 = EXP2 using a sequence of equalities (or simplify EXP1 and EXP2 to the same expression EXP3), except that when you derive the equalities you can in addition to the axioms and inference rules use the hypotheses in HYPS to help you.

  • No labels