Week | Date | Topic | Notes | Useful Readings | Homework |

1 | 9/8 | Overview and Background | notes | Review Harrison Ch. 1, also sections 2.1-2.6; Hickey's Introduction to Objective Caml; Harrison appendix 2 | Suggested exercises Solutions |

2 | 9/15 | Propositional Logic | slides | Harrison chapter 2 | Homework 1, due 9/29 |

3 | 9/22 | Theorem Proving Techniques for First-Order Logic I | slides; OCaml examples; Replacement makefile; init_no_fol.ml | Harrison sections 3.1-3.8 | |

4 | 9/29 | Theorem Proving Techniques for First-Order Logic II | slides; unif_example.ml | ||

5 | 10/6 | Decision Procedures for Equality I | slides; union_find.ml Replacement makefile; init.ml; init_no_fol.ml; make.ml | Downey-Sethi-Tarjan (DST), "Variations on the CSE Problem"; Nieuwenhuis and Oliveras, "Fast CC and extensions"; Hickey chapter 7 (on reference cells); Harrison sections 4.1-4.4 | Homework 2, due 10/20; hw2.ml |

6 | 10/13 | Decision Procedures for Equality II | slides | Harrison sections 4.5-4.7 | |

7 | 10/20 | Decidable Fragments of First Order Logic | slides | ||

8 | 10/27 | Presburger Arithmetic | slides | ||

9 | 11/3 | Algebraically Closed Fields | slides; handout | ||

10 | 11/10 | Finish algebraically closed fields, Intro to Gröbner Bases | slides | project, due 12/15 (short presentation on 12/8) | |

11 | 11/17 | Gröbner Bases | slides | ||

12 | 11/24 | No class (Happy Thanksgiving) | |||

13 | 12/1 | Real Closed Fields, Geometry Theorem Proving | Project: Deciding array formulas (Liana Hadarean) slides from lecture | ||

14 | 12/8 | Project Presentations; Theory combination | slides from lecture | ||

15 | 12/15 | No class (classes meet on a Monday schedule, per academic calendar) |