Syllabus

Week Date Topic Reading Lectures Homework Homework Solutions
1 9/8 Propositional Logic I 1.0 - 1.4 ps pdf ps(4up) pdf(4up)
Review sheet: ps pdf
ps pdf ps pdf
2 9/15 Propositional Logic II 1.5, 1.7 ps pdf ps(4up) pdf(4up) ps pdf ps pdf
3 9/22 Propositional Logic: Applications 1.7
Abstract DPLL (pp. 1-9)
ps pdf ps(4up) pdf(4up) None  
4 9/29 First-Order Logic: Syntax and Semantics 2.0 - 2.3 ps pdf ps(4up) pdf(4up) ps pdf ps pdf
5 10/6 First-Order Logic: Proof and Deduction 2.4 ps pdf ps(4up) pdf(4up) ps pdf ps pdf
6 10/13 First-Order Logic: Soundness and Completeness 2.5 ps pdf ps(4up) pdf(4up) ps pdf ps pdf
7 10/20 First-Order Logic: Compactness and Models 2.6 ps pdf ps(4up) pdf(4up) Midterm  ps pdf ps pdf
8 10/27 First-Order Logic: Theories 2.6
Combining Decision Procedures
Fast Decision Procedures Based on Congruence Closure
Variations on the Common Subexpression Problem
PhD thesis
ps pdf ps(4up) pdf(4up) None  
9 11/3 First-Order Logic: Applications A New Correctness Proof of the Nelson-Oppen Combination Procedure
Unions of Non-Disjoint Theories and Combinations of Satisfiability Procedures
Abstract DPLL and Abstract DPLL Modulo Theories
Run-Time Validation of Speculative Optimizations using CVC
ps pdf ps(4up) pdf(4up)
More: ps pdf ps(4up) pdf(4up)
ps pdf
Extra practice problem: ps pdf
ps pdf
10 11/10 Undecidability: Introduction 3.0 - 3.2 ps pdf ps(4up) pdf(4up) ps pdf ps pdf
11 11/17 Undecidability: Representability 3.3 ps pdf ps(4up) pdf(4up) ps pdf ps pdf
12 11/24 Undecidability: Godel's Incompleteness Theorem 3.4-3.7 ps pdf ps(4up) pdf(4up) None  
13 12/1 Second-Order Logic, Resolution, Many-Sorted Logic 4.1, 4.2, 4.3
Resolution
ps pdf ps(4up) pdf(4up) ps pdf ps pdf
14 12/8 Temporal Logic and Model Checking E. Clarke, O. Grumberg, D. Peled. Model Checking. MIT Press, 1999, chapters 3, 4.
Binary Decision Diagrams (pp. 1-9)
ps pdf ps(4up) pdf(4up)    

Final Exam: ps pdf