## 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 2 9/15 Propositional Logic II 1.5, 1.7 ps pdf ps(4up) pdf(4up) 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 5 10/6 First-Order Logic: Proof and Deduction 2.4 ps pdf ps(4up) pdf(4up) ps pdf 6 10/13 First-Order Logic: Soundness and Completeness 2.5 ps pdf ps(4up) pdf(4up) ps pdf 7 10/20 First-Order Logic: Compactness and Models 2.6 ps pdf ps(4up) pdf(4up) Midterm  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 10 11/10 Undecidability: Introduction 3.0 - 3.2 ps pdf ps(4up) pdf(4up) ps pdf 11 11/17 Undecidability: Representability 3.3 ps pdf ps(4up) pdf(4up) 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 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)