CMPT-701: Computability and Logic (Spring 2011)

• Notes pp1-17: Propositional Calculus
  
• Notes pp18-30: Predicate Calculus
  
• Notes pp31-38: Completeness of system LK for Predicate Calculus
  
• Notes pp39-53: Herbrand Theorem, Equality and Compactness
  
• Notes pp54-70: Computability Theory
  
• Notes pp71-82: Recursive and Recursively Enumerable Sets
  
• Notes pp83-95: Incompleteness and Undecidability
  
• Notes pp96-108: Peano Arithmetic
  
• Notes pp109-112: Godel's Incompleteness Theorems
  

• Arithmetical Relations (messy!)
• Tarski's Theorem
• Theories of Arithmetic
• RA Representation Theorem
• Main Theorem (Every consistent extension of RA is undecidable)
• Godel's Incompleteness Theorems

Assignments, etc.:
TBA

References:
- Herbert Enderton, A Mathematical Introduction to Logic, 2nd Ed'n. (Simiar coverage to this course, but using a different kind of proof system.)
- Michael Sipser, Introduction to the Theory of Computation (For Computability)
- A SAT Solver Primer, by David Mitchell (Section 2 describes the relationship between Resolution proofs and backtracking search=traversal of semantic tree)
- E. Mendelson, An Introduction to Mathematical Logic

Further Reading:
- And Logic Begat Computer Science: When Giants Roamed the Earth Abstract of a talk on Logic and CS by Moshe Vardi.
- Martin Davis Engines of Logic
- Handbook of Proof Theory, Chapters I and II by Sam Buss
- Buss, Kechris, Pillay and Shore, The Prospects for Mathematical Logic in the Twenty-first Century