CSU 290   Spring 2009   Section 2 (16h35)
Logic and Computation

PLEASE SEE THE OFFICIAL COURSE WEB PAGE for general course information such as homeworks, TAs, office hours, etc. This page is specifically for Section 2 information, mostly lecture notes. There is also an RSS feed specifically for section 2 announcements, that will also include all the main announcements from the official course web page.

Announcements  

Sun, 19 Apr 2009: I've moved my office hours tomorrow to 13h00-15h00, as I have a conference call at 15h00 that I need to take.

Thu, 16 Apr 2009: I've gotten the final grades for homework 6, and I'm finishing to correct that little grading errors that have made their ways into blackboard. I will be tabulating the grades and sending you all a report later tonight. So check your email, and you'll be able to determine whether you need to take the final or not. (You can probably figure it out already, but this may save you some time.)

Wed, 15 Apr 2009: First off, added an addendum to the first-order logic lecture notes giving two informal proofs of the theorems we proved in gory details. And I added the lecture notes for informal proofs by induction, the last lecture of the course.

Fri, 10 Apr 2009: Final exam information from the Registrar's Office: 04/23/2009 1:00 PM CS U290 LOGIC COMP 50 DG R.PUCELLA. So Thursday, April 23, 13h00. DG 50 is Dodge Hall 50, I believe.

Wed, 08 Apr 2009: Lecture notes for this afternoon's lecture on first-order logic are up. I also uploaded a PDF version of Monday's phantom lecture on binary search trees.

Wed, 08 Apr 2009: Sample solutions for homework 6 are available. Note that there are many ways to formalize some of the statements.

Tue, 07 Apr 2009: I want to apologize again for the last minute cancel of Monday's lecture. I would have talked about binary search trees. There's a couple of other things I want to talk about tomorrow and next Monday, so I won't actually cover that material, but I just made available to executable lecture notes for the lecture, that you can run interactively in ACL2s. For your edification, if you will, and they provide an example of a nontrivial ADT specification.

Tue, 07 Apr 2009: After a chat with Richard Zelinsky, I've decided to slightly modify the lecture notes on observational equivalence (and the corresponding bit in the lecture on binary trees), to make clear the notion of an invariant. Really what we define is an equivalence between representations, and we prove that that equivalence is an invariant of th eoperations. Hopefully, things are a bit clearer now.

Fri, 03 Apr 2009: Last update of the day, promised. Posted lecture notes on binary trees. We're now up-to-date with respect to lecture notes. Monday, binary search trees.

Fri, 03 Apr 2009: In case you did not notice, we have added the code unix.list for homework 6 in the assignments page.

Fri, 03 Apr 2009: The lecture notes on interfaces and specifications and on ADTs have been posted. I'll post the remaining notes (on binary trees) later tonight.

Fri, 03 Apr 2009: Homework 6 is available from the assignments page, due at midnight, Tue April 7. Also, midterm 6, originally scheduled for Wed April 8, has been moved to Thu April 9.

Thu, 02 Apr 2009: Posted lecture notes on observational equivalence are up. Lectures 24 & 25 will go up tomorrow morning - they're on my office computer.

Tue, 24 Mar 2009: Solutions to homework 5 are available, again using the "alternative" proof notation that I described at the end of the lecture 14. And, of course, a reminder that tomorrow (Wednesday) is the fifth midterm, covering generalization, proving in ACL2, and rewriting.

Mon, 23 Mar 2009: Posted lecture notes on rewriting. Today's lecture ended up being a review of generalization, and looking at problems 1(b), 2(c), and 4 on the last homework.

Thu, 19 Mar 2009: I just wanted to remind you that homework 5 is available from the assignments page, and that you only have to do the first 5 questions. You do not have to do question 6, although feel free to try, you should know everything needed to complete it anyways.

Thu, 19 Mar 2009: Posted lecture notes for the two lectures on ACL2 earlier this week. Lecture notes on rewriting coming up soon.

Thu, 12 Mar 2009: Lectures notes for today's lecture on generalization are up.

Mon, 09 Mar 2009: Lectures notes for today's lecture on the review using rev are up. There's a bit at the beginning and a bit at the end that I never got to but is useful, so please read it. Also, solutions to homework 4 have been posted on the homeworks page of the main web site. Again, the solutions use the "alternative" proof notation that I described at the end of the lecture 14.

Thu, 26 Feb 2009: Lecture notes for today's lecture on induction for other data types than lists. Have a good and safe break, and see you all back in March.

Wed, 25 Feb 2009: Lecture notes for today's lecture on induction are up. I did not proofread carefully, so there may be typos. Let me know if you find any.

Wed, 25 Feb 2009: Here is the formula that I wanted you to think about at the end of class today, the one I blanked on. Try to come up with the proof obligations for the following formula: (true-listp x) => (= (app x nil) x). In particular, try to "massage" the formula corresponding to the inductive step into a form you can actually prove. Then, prove both proof obligations, since that's a good exercise.

Mon, 23 Feb 2009: Lecture notes for today's lecture on termination and the definitional principle are up. I added some proving exercises at the beginning of the lecture, two of which I gave in class, two I did not. Do then, it's good practice, and they're not difficult.

Sat, 21 Feb 2009: Homework 4 is out, due at the end of Spring Break, March 7th. (You can do the first two questions now, for the rest, we will cover the material early next week.)

Thu, 19 Feb 2009: Lecture notes for today's lecture on case analysis are up.

Wed, 18 Feb 2009: Here are the solutions to the midterm questions, in case you were curious, along with a quick postmortem of how overall you all did, and the main problems encountered. We'll talk about it some tomorrow.

Tue, 17 Feb 2009: Sorry, it appears I messed up the link to the solutions file, unless you happened to click on the link from the announcements page. It's fixed now.

Tue, 17 Feb 2009: I've added the solution to questions 6 and 7 to the solution file. Again, make sure you understand what's going on.

Tue, 17 Feb 2009: Sorry, I forgot to finish the solutions, questions 6 and 7 have not been "converted". Hey, it's probably a good exercise to do so, if you have not done so already :). I'll try to plop them up by the end of the afternoon.

Tue, 17 Feb 2009: First off, I was away for the weekend, and while I expected to have email access, I turned out to be wrong. So if you have sent me email over the weekend, I should get to it today. If you had a question about the homework, I hope you thought of emailing the friendly TAs (such as your lab TA, always a good start). Anyways, solutions to homework 3 have been posted on the homeworks page of the main web site. Note that the solutions use the "alternative" proof notation that I described at the end of the lecture notes for last Thursday. (What, you didn't read them? Shame... shame...) Anyways, here are the solutions to homework 3 using the proof structure I gave in class. Make sure you understand what's going on.

Mon, 16 Feb 2009: Sorry to appear fickle, but something came up and coming in will be harder than expected. So I will not be in this afternoon. To compensate, I will be holding office hours tomorrow (Tuesday), 14h00-17h00. I will be in my office, just drop by if you have questions.

Sun, 15 Feb 2009: I will hold my office hours tomorrow as usual, 14h00-16h00, even though it's Presidents Day. I know, I have no life...

Thu, 12 Feb 2009: Lecture notes for the lecture on definitions and proving equality formulas and on proving conditional equality formulas have been posted. They reflect what I have talked about in class, especially the second lecture. I have also added some remarks at the end of the second lecture that you should read, especially if you have some time before the lab tomorrow.

Tue, 10 Feb 2009: Oops, forgot to mention this: the solutions to homework 2 are available on the homeworks page, if you're curious.

Tue, 10 Feb 2009: Here are the lecture notes for tomorrow's lecture, and also Thursday's really, since it's a bit long. If you read it through, you can do the homework. (You may need to disregard the page that reviews one way of doing proofs - we're doing things differently this week; and you also want to convert formulas in the homework from the ACL2 notation to the logical notation we've been using in class - pretty straightforward. I'll review all of this tomorrow.) Off to bed now.

Tue, 10 Feb 2009: Homework 3 is out. Note that you haven't seen the theory for it yet, that will be tomorrow. Actually, I will try to write up the notes for tomorrow today and post them tonight, so that if you want you can start on the homework tomorrow after having read the notes prior to the lecture. (Does that make sense?) Also, be aware that the syntax of the logic used in the homework 3 slightly different from the one I used in class. (One of the downsides of getting sick over the weekend is that I couldn't interact with the homework production as much.) I will probably give you all a version of the homework adapted to our section. A director's cut, if you will (or Section-2 cut?). The homework content will of course be the same - it's just the presentation of the formulas will be slightly different, in a way that will be obvious in retrospect.

Mon, 09 Feb 2009: Today's lecture on the ACL2 logic (equalities and function symbols) is available. The lecture was very much drinking from the fire hose, for which I somewhat apologize. But hey, it's done now, and the terms have been defined. Some things to note about the notes, which I did not have time to say in class, or plain forgot: (1) How do you determine the truth of a formula when it has an ACL2 expression in it? Same as what we saw in the "Propositional Logic in ACL2" lecture, any non-NIL value is true, NIL is false. (2) I forgot the most important point of equational proofs: if F has an equational proof, then F is valid. That is why equational proofs are interesting. (3) While every theorem is valid, it is not true that every valid formulas has an equational proof. This is essentially the content of Godel's incompleteness theorem. (4) I decided to make the Rule of Modus Ponens an actual rule, and not a derived rule. It is actually possible to remove it from the system, but not in the setup I gave. Sorry for having thought otherwise. We'll add more rules as time goes on, when they come in handy. Off to bed now, head's spinning.

Tue, 03 Feb 2009: Some lecture notes from the first section of the course, taught by Prof. Manolios, have been posted. Feel free to have a look. They are doing doing things a bit differently than we are in the first section, but you may benefit from the different exposition and the contrast.

Mon, 02 Feb 2009: Lecture notes for today, on extending propositional logic to deal with equality. I changed a little bit the presentation I made in class, for clarity, and I think it is now more understandable. I never got to the last proof, though. The lecture notes also give the quiz (which will not be graded thanks to Anna's inspired coin-toss call), and I recommend everyone takes a stab at it again if they did not get it the first time. That's what the midterm will be like. The midterm will cover propositional logic (validity, satisfiability, truth tables, equational proofs). Basically what we did last week, up to and including Thursday. Today's material is therefore not on the midterm. In class, I also handed out a sheet with a list of basic propositional validities that you can take as given in your proofs. And as I stated in class, for this midterm, when asked for an equational proof, I will ask you to do it somewhat pedantically: perform at most one substitution at each step, and write down the substitution you are using. Like in the notes, that should be your model. We want to have as much data as possible when grading, and it's hard to tell what you are thinking sometimes when we do not see the steps you go through in details. We'll relax on this point after the midterm.

Mon, 02 Feb 2009: Corrected lecture notes for lecture 8 on propositional logic; I stupidly messed up the de Morgan duals. It shoud be all better now.

Sat, 31 Jan 2009: The lecture of lists and cons structures, the last lecture on "programming ACL2", is now available.

Sat, 31 Jan 2009: On the off-chance some of you believe that what we're doing in class with our equational proofs is useless for non-class work, I was sitting down to finish up a research paper this morning with a colleague, and she made a statement that essentially amounted to the validity of the following propositional logic formula: (x => ~y) <=> (x => ~(x => y)), where I use => for implication, <=> for equivalence, and ~ for negation. I wasn't completely convinced, so I hammered out an equational proof, and presto, validity established. Try it out, it's not a hard one.

Fri, 30 Jan 2009: Slowly working my way up the stack - I've posted the lecture notes for the first six lectures. Only the lecture on deconstructing lists left, and I'm up to date.

Thu, 29 Jan 2009: Lecture notes for today's lecture on propositional logic in ACL2 are available. I haven't proofread them yet, so there may be typos, be warned.

Wed, 28 Jan 2009: Lecture notes for today's lecture on equational proofs are available. Please do the exercise, it's good practice. I also very slightly modified the lecture notes on propositional logic, restating the Principle of Substitution to match the one gave in class.

Tue, 27 Jan 2009: Lecture notes for yesterday on propositional logic are available. Please have look, partly because I put in more exercises than I discussed in class, in case you want to drill a bit on validity. I will pick up some of the stuff at the end, on if-then-else, tomorrow. Lecture notes for the first seven lecture on programming in ACL2 are coming along, and should be up later this week.

Mon, 26 Jan 2009: Prof. Pucella has changed his office hours to Mondays from 14h00-16h00.

Sun, 25 Jan 2009: Homework 2 is available from the course web page.

Schedule Outline and Lecture Notes

This schedule is subject to change without warning. Readings will be assigned to supplement lectures, and posted here.