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