Harvey Mudd College
Computer Science 81
Spring 2007
Sample Final
(
solutions
)
General information and outline
Slides from the Spring 2005 offering of CS 81
Slides from the Fall 2003 offering of CS 81
LaTeX proof box macros (2 sets)
JAPE Proof Editor
Conjunctive Normal Form and Truth Table calculator
Assignment 1
(
Solutions
)
Notes on derivatives of regular expressions
Notes on abstract states, etc.
PFLAP version 2
(
Test
,
Output
)
Grammars in Prolog example
Assignment 2
(
Solutions
)
Assignment 2 problems in TeX
Assignment 3
(
Solutions
)
Assignment 4
(
Solutions
)
Notes on converting to a 1-state PDA
Assignment 5
(
Solutions
)
Augmented CYK Algorithm in Python
(
Output
)
Grammar for assignment 5 problem 5 in Prolog DCG notation
(
Output
)
Assignment 6
(
Solutions
)
Notes on Proposition Logic
Notes on Soundness and Completeness for Proposition Logic
Constructive Completeness Proof for Proposition Logic
Assignment 7
(
Solutions
)
Sample Mid-Term Exam
(
Solutions
)
Mid-Term Exam Solutions
Notes on Predicate Logic
Assignment 8
(
Solutions
)
Notes on Conversion to Clausal Form
Assignment 9
(
Solutions
)
Assignment 10
(
Solutions
)
Assignment 11
(
Solutions
)
Implementation of the van Dalen partial recursive function language
(
sample output
)
(
View only if not interested in this part of the extra credit: version with Predecessor
)
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)
Other Links of interest
Introduction to Natural Deduction
(Daniel Clemente Laboreo) (The rules are slightly different than van Dalen's, but the examples still could be helpful.)
Natural Deduction
(wikipedia)
Peano Arithmetic
(wikipedia)
List of First-Order Theories
ACL2
(Theorem prover based on structural induction)
Computability and Recursion
(Robert I. Soare)
Gödel's Theorem
Translation of Gödel's paper
Notes on Gödel's Theorem
Gödel's Theorem and Around
(Karlis Podnieks)
Popular Impact
(Torkel Franzen)
Logic Factasia
Theorems for Sale