Announcements

• June 3:
  
  The final exam is scheduled for
  Tuesday, June 8 from 7:00-10:00p.
  It will take place in TCSeq 102 (the same classroom as lecture) and will be closed book.
  
  
• May 26: The due date for PS4 has been extended by 1 day. It is now due Friday at 11:59p. On top of that you may use late days if you like.
• May 19: PS3 has been graded, and handed back. Solutions are now posted.
• May 4:
  • Homework 2 has been graded and handed back.
  • Homework 2 solutions have been posted.
  • Homework 3 will be released Thursday, May 6 and will be due the following Thursday.
• Apr 18:
  • Homework 1 has been graded and handed back.
  • Homework 1 solutions are posted below.
  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)
• Chapter 8 - Relational Proofs (ps and pdf)
• Chapter 9 - Relational Resolution (ps and pdf)
• Information Integration (doc and pdf)

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

Submit your solutions at https://persistent.stanford.edu/start?.

• Background Test (Solution [More Detail])
• Problem Set 1 (Solutions)
• Problem Set 2 (Solutions)
• Problem Set 3 (Solutions)
• Problem Set 4 (Solutions)

• Lisp Tutorial (pdf)
• Overview
• Programming Assignment #1
• Programming Assignment #2
• Programming Assignment #3
• Contest Tips

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. At one time it was available online, but now it looks like it must be downloaded. Here is its home page.

Feedback

• To send the cs157 staff anonymous feedback click here.

Stuff from Previous Years

Online Materials from Spring 2003