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 13h0015h00, 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 firstorder
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 firstorder
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 uptodate 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: (truelistp 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),
14h0017h00. 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, 14h0016h00, 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 Section2 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 nonNIL 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 cointoss 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 offchance some of you believe that what we're doing in class
with our equational proofs is useless for nonclass 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 ifthenelse, 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
14h0016h00.
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.
Jan 5
 Introduction 
 Lecture notes 
Jan 7 
Review of 211, demo of ACL2s 
(See Jan 5 for lecture notes) 
Jan 8 
Introduction to ACL2 
(See Jan 5 for lecture notes) 
Jan 12 
Recursion and Termination (1) 
(See Jan 5 for lecture notes) 
Jan 14 
Recursion and Termination (2) 
(See Jan 5 for lecture notes) 
Jan 15 
Recursion with Accumulators 
(See Jan 5 for lecture notes) 
Jan 19 
Martin Luther King's Day  no classes 

Jan 21 
Midterm 1 

Jan 22 
Lists and Cons Structures 
 Lecture notes 
Jan 26 
Propositional logic 
 Lecture notes 
Jan 28 
Equational Proofs 
 Lecture notes 
Jan 29 
Propositional logic in ACL2 
 Lecture notes 
Feb 2 
Reasoning about equality 
 Lecture notes
 Bank of propositional validities 
Feb 4 
Midterm 2 

Feb 5 
Cancelled 

Feb 9 
Reasoning about Equality and
Function Symbols 
 Lecture notes 
Feb 11 
Definitions and Proving Equality Formulas 
 Lecture notes 
Feb 12 
Proving Conditional Equality Formulas 
 Lecture notes 
Feb 16 
President's Day  no classes 

Feb 18 
Midterm 3 

Feb 19 
Case analysis 
 Lecture notes 
Feb 23 
The definitional principle 
 Lecture
notes 
Feb 25 
Induction 
 Lecture notes 
Feb 26 
Induction for general data definitions 
 Lecture notes

Mar 2 
Spring break  no classes 

Mar 4 
Spring break  no classes 

Mar 5 
Spring break  no classes 

Mar 9 
Review using rev 
 Lecture notes 
Mar 11 
Midterm 4 

Mar 12 
Generalization 
 Lecture notes 
Mar 16 
Using ACL2 
 Lecture notes 
Mar 18 
More on using ACL2 
 Lecture notes 
Mar 19 
Rewriting in ACL2 
 Lecture notes 
Mar 23 
Review 

Mar 25 
Midterm 5 

Mar 26 
Specifications and interfaces 
 Lecture notes 
Mar 30 
Abstract data types 
 Lecture notes 
Apr 1 
Observational equivalence 
 Lecture notes 
Apr 2 
Binary trees 
 Lecture notes 
Apr 6 
Binary search trees 
 Lecture notes
 Code 
Apr 8 
Firstorder logic 
 Lecture notes 
Apr 9 
Midterm 6 

Apr 13 
Inductive proofs 
 Lecture notes 
