We survey the state of the art in automated deduction through a collection of useful algorithms and semi-algorithms. Topics include propositional satisfiability, ground decision procedures for equality and inequality, combination methods, quantifier elimination, rewriting, and proof search. The emphasis is on simple and unified theoretical foundations, efficient implementation, and novel applications. Our presentation includes recent research results and complements the contents of the Fall Quarter Logic Seminars. A basic background in logic and computation is adequate. The course should be of interest to graduate students in logic, computer science, and philosophy.
Date | Lecturer | Topic |
Wed Sep 24 |
Shankar |
Course Overview ( ps, ps.gz, pdf) |
Mon Sep 29 |
Shankar |
Decidability and Decision Procedures ( ps, ps.gz, pdf) |
Wed Oct 1 |
de Moura |
Propositional Satisfiability: Truth Table, Tableau, Resolution ( ps, ps.gz, pdf) |
Mon Oct 6 |
de Moura |
Propositional Satisfiability: Davis-Putnam, Stalmarck ( ps, ps.gz, pdf) |
Wed Oct 8 |
de Moura |
Propositional Satisfiability: BDDs ( ps, ps.gz, pdf) |
Mon Oct 13 |
Tiwari |
Equality: Variables, Union-Find, Ackermann, Congruence Closure ( ps, ps.gz, pdf) |
Wed Oct 15 |
Tiwari |
Equality: Finite Instantiation, Ground Completion ( ps, ps.gz, pdf) |
Mon Oct 20 |
Tiwari |
Equality: Congruence closure, Basic superposition ( ps, ps.gz, pdf) |
Wed Oct 22 |
Ruess |
Equality Decision Procedures ( ps, ps.gz, pdf) |
Mon Oct 27 |
Ruess |
Equality Decision Procedures ( ps, ps.gz, pdf) |
Wed Oct 29 |
Shankar |
Summary ( ps, ps.gz, pdf) |
Mon Nov 3 |
Shankar |
Combination Methods: Nelson-Oppen ( ps, ps.gz, pdf) |
Wed Nov 5 |
Shankar |
Combination Methods: Shostak ( ps, ps.gz, pdf) |
Mon Nov 10 |
Shankar |
Arithmetic Inequalities ( ps, ps.gz, pdf) |
Wed Nov 12 |
Shankar |
Arithmetic Inequalities ( ps, ps.gz, pdf) |
Mon Nov 17 |
Tiwari |
Commutative Semigroups and Algebraically Closed Fields ( ps, ps.gz, pdf) |
Wed Nov 19 |
Tiwari |
Quantifier Elimination for Real Closed Fields ( ps, ps.gz, pdf) |
Mon Nov 24 |
Ruess |
Presburger Arithmetic and S1S ( ps, ps.gz, pdf) |
Mon Dec 1 |
de Moura |
Bounded Model Checking ( ps, ps.gz, pdf) |
Wed Dec 3 |
Tiwari |
Qualitative Abstraction ( ps, ps.gz, pdf) |