CS 81: Computability and Logic

Course Staff and Consulting Hours

Prof. Robert Keller , keller [AT] cs.hmc.edu, 1253 Olin MTW 2:45-4:00

For quickest response, contact all of us by e-mailing cs81help [AT] cs.hmc.edu. Tutoring is held in the Platt Campus Center Livingroom, near the whiteboards. Professors' office hours are held in their respective offices.

Grading

Homework	50%
Midterm	20%
Final	25%
Participation (attendance, asking questions, coming to office hours, etc.)	5%

Textbooks

Michael Huth and Mark Ryan, Logic in Computer Science, Second Edition (Paperback), Cambridge University Press (2004), ISBN-10: 052154310X, ISBN-13: 978-0521543101 (link includes errata) (preview)

Michael Sipser, Introduction to the Theory of Computation, Third Edition (Hardcover), Course Technology (February 15, 2005), ISBN-10: 0534950973, ISBN-13: 978-0534950972
Errata

LaTex Formatting Packages

Assignments

Selected Lecture Slides

Other Items of Interest

Logic Portal on Wikipedia
Special Issue of Formal Proof, Notices of the American Mathematical Society
Natural Deduction Prover in Prolog, based on the completeness theorem proof
Sequent Calculus Prover in Prolog
Predicate Calculus Truth Evaluator for Finite Domains
Otter 3.3 (command-line version)
Original Otter manual
Otter examples
Inference Rules Used in Otter
Prover9
Prover9 Manual
Otter-λ (web, and other)
- Modus Ponens Example | Transitivity Example
- Monoid Example 1 | Monoid Example 2 | Monoid Example 3
- Group Example 1
- Equivalence Relation Example 1
- Universally-valid Example 1 | Universally-valid Example 2 | Universally-valid Example 3 | Universally-valid Example 4
- Missile Example
- Mushrooms Example
- Grandfather Example (answer predicate)
- Pegs puzzle
- Pegs puzzle, recording version
- Son of BirdBrain II (More theorem proving examples)