CS157: Computational Logic

Announcements

May 4:
April 23:
- Feel free to post questions to the newsgroup su.class.cs157. The TAs will try to answer questions there regularly. Of course, sending us e-mail is fine as well if need be. General instructions for connecting to newsgroups can be found at http://www.stanford.edu/services/usenet/.
- It would be preferred if you entered your answers for homework 2 in KIF instead of infix notation where possible. A description of the language can be found at http://arrogant.stanford.edu:5000/language? or on one of the normal Logica pages. We will accept infix notation if you must, but KIF is preferred for doing automatic logical equivalence checking.
- A TA has been added for the class: Danny Tarlow. He is also reachable at the e-mail address cs157-ta@cs.stanford.edu.
- Homeworks are being graded incrementally. We will send out an e-mail when they are finished.
April 14:
- Logica went down for a few hours tonight and has been restarted on ports 9000, 9001, 9002, 9003, 9004, and 9005. The homework deadline has been extended by 3 hours to 2:59am.

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.