Harvey Mudd College

CS 81: Computability and Logic
Spring 2013

Course Staff and Consulting Hours

Name	How to Contact	Hours (Platt Living Room, unless noted otherwise)
Prof. Robert Keller	keller [AT] cs.hmc.edu	MTW 2:45-4:00, 1253 Olin
Rohitashwa Bagaria	rbagaria [AT] hmc.edu	Sun. 7-8 pm
Sam Gray	sam_gray [AT] hmc.Edu	Sun. 8-9 pm
Ben Johnson	bjohnson [AT] g.hmc.edu	Tue. 7-8 pm
Jeffrey Hemphill	jeffrey_hemphill [AT] hmc.edu	Tue. 8-9 pm
Kevin Vigue	kevinvigue [AT] gmail.com>	Wed. 7-8 pm
Jake Low	jake_low AT hmc.edu	Wed. 8-9
Meg O'Keefe	margaret_okeefe AT hmc.edu	Thu. 7-8 pm
Jason Wang	jason_wang [AT] hmc.edu	Thu. 10-11 pm

For quickest response, please use our piazza site. Tutoring is held in the Platt Campus Center Livingroom, near the whiteboards.

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 (July, 2012), ISBN-10: 0534950973, ISBN-13: 978-0534950972
Errata

Assignments

Assignment 1
Assignment 2
Assignment 3
Assignment 4
Assignment 5
Assignment 6
Notes on Conversion to Clausal Form
Resolution Problems, for Practice
Assignment 7
Assignment 8
Assignment 9
Assignment 10
Non-Assignment 11
Below the line are assignments from the previous time I (co-)taught this course. They are not necessarily the ones that will be used this time.
Assignment 7
Assignment 8
Assignment 9
Assignment 10
Assignment 11

Selected Lecture Slides

Introduction, Propositional Natural Deduction
Semantics, Soundness, Completeness
Tableau Proofs
Sequent Calculus
Predicate Logic
Blocks World Logic
Predicate Tableaux
Program Logic (Part 2, Mostly JAPE stuff)
Resolution
Computability 1st Week Outline
Background on Logic Circuits (notes from HMC CS 42)
Strings, Machines, and Languages
pflap.pro (Prolog Finite Language and Automata Package)
Abstract States of a Language
Grammars and Languages
Pushdown Automata
CYK & Parsing
Effective Computability
Uncomputability
Below the line are slides of Prof. Stone, from the previous time we co-taught this course. They are not necessarily the ones that will be used this time, but you can read them for extra viewpoints.
Structural Induction
Theories
Constructive Logic
Other Logics
Strings and Languages
Regular Languages
NFA to Regexp, Regular Expressions
Closure Properties, Myhill-Nerode, Pumping Lemma
Context-Free Grammars
Parsing and PDAs
CKY, Intro to Turing Machines
From TMs to Decidability
Undecidability and Reductions
TM Histories, PCP, Recursion Theorem
Other Models of Computation, Decidability of Logical Theories, Incompleteness

Other Items of Interest

LaTex Formatting Packages for proof boxes and more
- Set from Alan Davidson, HMC '06
- Set from Huth & Ryan (includes trees)
- Set from Paul Taylor
- bussproofs.sty
- LaTeX for Logicians
- GasTeX for Graph and Automata Drawing (JasTeX, GUI for producing GasTeX)
- ProofCheck: Proof Checker for LaTeX Proofs (video, from ProofCheck.org)
JAPE Distribution (Just Another Proof Editor)
JAPE Natural Deduction Manual
Logitext Interactive Sequent Calculus
Tree Proof Generator
Sequent Calculus Prover
ProofWeb
Proof assistant Wikipedia page
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)
Database of Mechanized Reasoning Systems
JFLAP (Java Formal Languages and Automata Package)
Proof of the Four-Color Theorem
2-state 3-symbol universal (?) Turing machine