Child pages
  • CSU 290 (Spring 2008)

Versions Compared


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


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.)


And that's it, we cannot lump things any further. And we've exhausted all of our equations in the hypotheses. So the lumps above represent all the different things that can be proved equal to each other. Our conjecture asks whether the three equations imply that (f (g a)) = b; in other words, do the three equations ensure that (f (g a)) and b are lumped together by the above procedure? It is easy to see that yes, they are. Therefore, the algorithm (and ACL2s) will report that the conjecture is true.


April 21: Study Guide

As requested by a few students, here is a quick study guide for the final. (There is nothing here that has not been said already in class.) As we mentioned in class, the final will be a cross-section of all the tests we have had during the semester. Roughly, there should be one question per exam.

So what did those tests cover?

Test 1:

  1. the basics of the ACL2 programming language
  2. total functions,
  3. the use of the design recipe to develop functions

Test 2:

  1. lists and true lists
  2. quotation
  3. design recipe for recursive functions over true lists

Test 3:

  1. Boolean logic
  2. proving theorems using equational reasoning
  3. falsifying conjectures

Test 4:

  1. the induction principle (give proof obligations)
  2. proving proof obligations

Test 5:

  1. more difficult inductions (idenfitication of lemmas)
  2. generalization
  3. using different substitutions in the inductive proof obligation

Test 6:

  1. The ACL2s theorem prover and the waterfall model
  2. rewriting
  3. understanding proof reports, including identifying interesting checkpoints
  4. decision procedures for Boolean logic and congruence closure