Harvey Mudd College

Computer Science 81

Fall 2007

• General information and outline
• Slides from the Spring 2005 offering of CS 81
• Slides from the Fall 2003 offering of CS 81

• Midterm Solutions
• Assignment 1 Solutions
• Assignment 2 Solutions
• Assignment 3 Solutions
• Assignment 4 Solutions
• Assignment 5
• Assignment 6
• JAPE Proof Editor
• JAPE Quantifier Proof Examples
• Hints for Using JAPE for Natural Deduction
• Prenex rules justified using JAPE
• JAPE Natural Deduction Manual (Richard Bornat)
• Otter-λ
• Original Otter manual
• 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
• Son of BirdBrain II (More theorem proving examples)

• Logic for Computer Science, by Jean Gallier (reference book for resolution, etc.)
• Hoare Logic
• wikipedia page
• Hoare Logic in JAPE (incomplete notes)
• Hoare's original paper (CACM, Oct. 1969)

• Structural Induction
• wikipedia article
• ACL2 (Theorem prover based on structural induction)
• Application to languages
• Application to languages, with on-line exercises

• Meta-Logic
• Soundness and Completeness (slides)
• Constructive Completeness (write-up)

• Lambda Calculus
• Lecture Slides
• Wikipedia article
• Introduction to Lambda Calculus (Henk Barendregt and Erik Barendsen)
• The impact of the lambda calculus on logic and computer science (by Henk Barendregt, in Bulletin of Symbolic Logic)

• Other Links of interest
• Introduction to Natural Deduction (Daniel Clemente Laboreo)
• Natural Deduction (wikipedia)
• Peano Arithmetic (wikipedia)
• List of First-Order Theories

• Schedule Part II