Tentative Syllabus

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 LogicslidesHarrison chapter 2Homework 1, due 9/29
3 9/22 Theorem Proving Techniques for First-Order Logic Islides;
OCaml examples;
Replacement makefile;
init_no_fol.ml
Harrison sections 3.1-3.8
4 9/29 Theorem Proving Techniques for First-Order Logic IIslides;
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 IIslidesHarrison sections 4.5-4.7
7 10/20 Decidable Fragments of First Order Logicslides
8 10/27 Presburger Arithmeticslides
9 11/3 Algebraically Closed Fieldsslides;
handout
10 11/10 Finish algebraically closed fields, Intro to Gröbner Bases slidesproject, 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)