This course covers fundamental concepts, techniques and algorithms in computer-aided reasoning. The topics covered include propositional logic, variants of the DPLL algorithm for satisfiability checking, first-order logic, unification, tableaux, resolution, Horn clauses, congruence closure, rewriting, Knuth-Bendix completion, decision procedures, Satisfiability Modulo Theories, recursion, induction, termination, Presburger arithmetic, quantifier elimination and interactive theorem proving. The course is project-based and students will develop and implement a reasoning engine in a sequence of assignments, over the course of the semester. The course will also cover how to formalize and reason about computational systems using a modern interactive theorem prover.

The prerequisites for this course are CS2800 and CS4800 or permission of the instructor. The course will be project-based so you will need a strong programming background and a solid understanding of algorithms. You also need to understand logic at the level of CS2800.