Announcements

• May 28: Paper on the alexander/magic sets construction is now available. See Bottom UP Model Elimination for postscript version.
• May 23:
  • PS4 is released and due Thursday, May 30.
  • We have a new submission script for PS4! It's located at the same url as the original.
  • Most of the contest is online.
• May 13:
  • PS3 #6.b.8: When we ask for the fastest combination of strategies, we want the fastest combination of strategies that produces the correct results.
  • Tim's office hours on Wednesday, May 15, will be from 1:45-3:45.
• May 9: PS3 #5: "All friends ski together" should read "If two people are friends and one of them skis, then both ski."
• May 8:
  • PS 2 solutions and PS 3 are now online.
    
  • The final for the course looks like it will be on Tuesday, June 11 at 7p.
  • The first deadline for the contest is fast approaching. If you think you might want to participate, send us (cs157-help@cs) an e-mail with the names of 2-3 people who comprise your group (one submission per group please) and a group name. By forming a group, you are not required to participate, but if you fail to do so, you will not be allowed to participate.
• April 25: PS 2 and PS 1 solutions are now online.
• April 23: See changes to Herbrand lecture dealing with the problem that emerged in class. Change #1: The "proof" of the Herbrand theorem has two parts - one for the case where there are object constants and one for the case where there are no object constants. Change #2: The offending example has been modified to include an object constant. Sorry for the confusion.


Archived announcements

Course Information

• Information
• Lecture Schedule (tentative)
• People
• Collaboration Policy
• Homework Submission Policy
• Mailing lists
• Standard Axiom Schemata
• Regrade Policy

Class Notes

• Chapter 1 - Introduction (pdf or (ps)
• Chapter 2 - Propositional Logic (pdf or ps)
• Chapter 3 - Semantic Methods (pdf or ps)
• Chapter 4 - Propositional Proofs (pdf or ps)
• Chapter 5 - Propositional Resolution (pdf or ps)
• Chapter 6 - Relational Logic (pdf or ps)
• Chapter 7 - Herbrand Method (ps and pdf) Old
• Chapter 8 - Relational Proofs (ps and pdf)
• Chapter 9 - Relational Resolution (ps and pdf) Old

Lecture Notes

• Lecture 1 (pdf or ps)
• Lecture 2 (pdf or ps)
• Lecture 3 (pdf or ps)
• Lecture 4 (pdf or ps)
• Lecture 5 (pdf or ps)
• Lecture 6 (pdf or ps)
• Lecture 7 (pdf or ps)
• Lecture 8 (pdf or ps)
• Lecture 9 (pdf or ps)
• Lecture 10 (pdf or ps)
• Lecture 11 (pdf or ps)
• Lecture 12 (pdf or ps)
• Lecture 13 (pdf or ps)
• Lecture 14 (pdf or ps)
• Lecture 15 (pdf or ps)
• Lecture 16 (pdf or ps)
• Lecture 17 (pdf or ps)
• Review (pdf)

Problem Sets

Use this form to submit your solutions. See the homework submission policy for more details.

• Background Test (Solution [more details])
• Problem Set 1 (Solution)
• Problem Set 2 (Solution)
• Problem Set 3 (Solution)
• Problem Set 4 (Solution)

Contest

• Contest rules
• Problem categories

Fun Stuff

• Check out Logica, a simple proof generation system for propositional and relational logic.
• Otter is a very powerful theorem prover that you can use (hint, hint!) to solve problems. Also check out Otter's home page.

Feedback

• To send the cs157 staff anonymous feedback click here.

Stuff from Previous Years

Online Materials from Spring 2001