Announcements

• Dec. 10: -Sutin will hold office hours tomorrow (Wednesday) from 10am-noon at Bytes Cafe (in the Packard Building).
  -Walter's office hours today have been shifted to 3:45pm-5:00pm in the Gates basement TA office.
  -An even newer version of the PS #4 solutions has been posted with more explanation for #5.
  -There was a mistake is the PS #4 solutions on 4a. A new corrected version has been posted.
  


• Dec. 9: -Solutions to PS #4 have been posted. You can find it in doc, pdf, and html format.
  -All problem sets have been graded and returned now. For PS #3, here are the stats: mean - 89.95, median - 93, standard deviation - 11.66. For PS #4, here are the stats (out of 90): mean - 83.71, median - 85, standard deviation - 5.54. For PS #4, here are the stats (out of 100): mean - 93.01, median - 94.44, standard deviation - 6.06.
  -The following information is for SITN students only. For remote students, arrangements are made by SITN with the students' local proctors as to whether SITN faxes or sends hardcopy by overnight mail to the proctor. Students make arrangements with their proctor to set aside 3 hours for the exam. The proctor collects and sends the original exams back to SITN. You have a 24 hour window to take the exam, but if any of you have serious conflicts with this, we will try to work something out.
  


• Dec. 7: -Solutions to PS #3 have been posted. You can find it in doc, pdf, and html format. PS #4 solutions should follow soon.
  -The final exam will be closed book/closed notes.
  -The final exam will be on THURSDAY, DECEMBER 12, from 3:30pm-6:30pm. It will be in our normal classroom (for those of you who haven't yet had the pleasure of coming to a lecture, that would be McCullough 115). The final is designed to take two hours or less, but you will have the full three hours to take the exam. If you were approved to take the alternate exam, you should have received an e-mail with all the details.
  -The TA's will be having a couple office hours next week. Walter will have office hours at his normally scheduled time on Tuesday at 2:30-4:30 in the Gates basement. Sutin will announce her office hours in the near future.
  -Do not combine multiple steps on the final. For example, do not say "resolving premises 3, 4, 5, 8, and 10, we will get the empty clause." You must write out each step. In this example, you would need 4 statements to represent this resolution. Massive points will be taken off for combining steps.
  -The solutions to PS 3 and PS 4 will be posted in the next day or two and all remaining problem sets will be graded and returned as well.
  -The contest results are as follows (to get extra credit amount, divide by 5):
  CS157 Staff -- 81.556
  CS221-Tas -- 78.996
  chmod 666 -- 69.608
  A2V -- 69.243
  Inspector Gadget -- 59.242
  Cigol -- 58.693
  Constant Time -- 58.184
  Team Comp Stomp -- 55.11
  Resomania -- 49.840
  Champions -- 49.301
  Bear Ninja Cowboy -- 48.333
  Mister Spock's Posse -- 37.473
  Resolutionaries -- 32.541
  Blue Sky -- 29.306
  Optimizer -- 12.054
  


• Dec. 3: -A few clarifications from the review session today:
  1. There was a bit of confusion in the explanation of Restriction Strategies. Check the lecture #12 slides for clarification.
  2. For semi-ordered resolution, you may do reduction on any one literal in the first chain, but the second chain has to have reduction done on the first literal in the chain.
  3. Set of Support resolution is complete for most cases, but not for when the goal is the empty set.
  4. For Epilog, you do not negate the goal statement, but just add a "?" to the end of it (this is, in effect, a negation).
  -The slides from the review session have been posted.
  

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) Old
• Chapter 6 - Relational Logic (pdf or ps) Old
• Chapter 7 - Herbrand Method (ps and pdf) Old
• Chapter 8 - Relational Proofs (ps and pdf) Old
• 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) Old
• Lecture 9 (pdf or ps) Old
• Lecture 10 (pdf or ps) Old
• Lecture 11 (pdf or ps) Old
• Lecture 12 (pdf or ps) Old
• Lecture 13 (pdf or ps) Old
• Lecture 14 (pdf or ps) Old
• 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: doc | pdf   FAQ and Changes (Solution doc | pdf | html)
• Problem Set 2: doc | pdf | html   FAQ and Changes (Solution doc | pdf | html)
• Problem Set 3: doc | pdf | html   FAQ and Changes (Solution doc | pdf | html)
• Problem Set 4: doc | pdf | html   FAQ and Changes (Solution doc | pdf | html)

CS157 Online

Check out http://www.stanford.edu/~tjruwase/projects/cs157/ for an online version of CS157 that's currently in the works. Check it out and send any comments (good or bad) to the the guy in charge of it.

Contest

• Contest rules
• Problem categories

Fun Stuff

• Check out Logica, a simple proof generation system for propositional and relational logic. Other versions: Sound:2000, Persistent:2000.
• 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 2002