Harvey Mudd College
Computer Science 81
Fall 2006
Leon Henkin
(April 19, 1921 - November 1, 2006)
General information and outline
Office Hours
LaTeX proof box macros (2 sets)
Assignment 1
(
sample solutions
)
Assignment 2
(
sample solutions
)
Notes on state equivalence and minimization
Assignment 3
(
sample solutions
)
Assignment 4
(
sample solutions
)
Assignment 5
(
sample solutions
)
PDA Simulator in Prolog
Conversion to 1-state PDA
Simulation comparison
Assignment 6
(
sample solutions
)
Assignment 6: PDA Conversion Solution
Assignment 7
(
sample solutions
)
Assignment 8 and mid-term exam info
(
sample solutions
)
Sample exam problems
(
some solutions
)
Mid-Term Exam solutions
Examples from "active" proof of the propositional Completeness Theorem
Input (formulas)
Output (proofs)
Assignment 9
(
sample solutions
)
Assignment 10
(
sample solutions
)
Virtual Assignment 11
Final Exam Solutions
Links of interest
JAPE
(proof editor)
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
Automated Theorem Proving and Reasoning
Otter-λ
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)
Turing-machine Simulation Example
(showing the first-order predicate calculus is undecidable)
Otter-λ
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)
Note on Effective Computability
Gödel's Theorem
Notes on Gödel's Theorem
Gödel's Theorem and Around
(Karlis Podnieks)
Popular Impact
(Torkel Franzen)
Theorems for Sale