CS 81: Computability and Logic
Fall 2012

Course Staff

• Prof. Chris Stone
• Eric Autry
• Jack Ma
• Audrey Musselman-Brown
• Stephanie Porter
• John Sarracino
• David Scott
• Rebecca Thomas
• Garrett Wong

• Introduction; Structural Induction
• Natural Deduction for Propositional Logic
• Truth Tables; Intro to Predicate Calculus
• Hoare Logic
• Linear and Temporal Logic
• Strings and Languages
• State Machines
• Regular Languages
• Regular Expressions
• Closure Properties; Nonregular Languages
• Context-Free Grammars
• Parsing and PDAs
• Parsing Concluded; Turing Machines
• Uncomputability
• Uncomputability Dialog Worksheet
• Computation Histories, PCP, and the Recursion Theorem
• Conclusion: Beyond (and back to) Turing Machines

Handouts

• Syllabus
• Worksheet: Natural Deduction and Predicate Calculus
• Worksheet: Models and Predicate Calculus
• Worksheet: Tableau Proofs
• Worksheet: Countability

Homework Assignments

• Assignment 11: Bringing CS 81 to a Logical Conclusion
  • Due in class Wednesday, December 12
  • My LaTeX Source
  • Sample solution on Sakai.
  
  
• Assignment 10: Decidable, Semidecidable, and Undecidable
  • Due in class Wednesday, December 5
  • My LaTeX Source
  • Sample solution on Sakai.
  
  
• Assignment 9: Regular, Nonregular, and Context-Free
  • Due in class Wednesday, November 21.
  • My LaTeX Source
  • Sample solution on Sakai.
  
  
• Assignment 8: Regular Languages
  • Due in class Wednesday, November 14.
  • My LaTeX Source
  • Sample solution on Sakai.
  
  
• Assignment 7: Induction and State Machines
  • Due in class Wednesday, November 7.
  • My LaTeX Source
  • Sample solution on Sakai.
  
  
• Assignment 6: Temporal Logic and Cardinality
  • Due in class Wednesday, October 31.
  • My LaTeX source
  • Sample solution on Sakai.
  
  
• Assignment 5: Proving Programs Correct
  • Due October 10
  • Sample solution on Sakai.
  • My (Terrible) LaTeX source
  
  
• Assignment 4:
  • Sample solution on Sakai
  • My LaTeX source
  • My sample solutions use the TikZ package for typesetting tableau proofs, but I don't claim this is necessarily the best approach; see also the section of LaTeX for Logicians. (Legible handwriting is perfectly acceptable.)
  
  
• Assignment 3:
  • Sample solution on Sakai.
  • My LaTeX source
  
  
• Assignment 2:
  • A one-sheet summary of the Natural Deduction rules
  • Sample solution on Sakai.
  • My LaTeX source (again, won't typeset without my personal macros)
  • Two sets of LaTeX macros for proof boxes
  • boxproof.sty: The proof-with-boxes package that I've used (possibly the same as one of the above.)
  
  
• Assignment 1:
  • See the paper handout for MIU rules
  • My LaTeX source (won't typeset without my personal macros, but parts might be reusable)
  • Sample solution on Sakai.