Class Logs and Required Readings
The cited references can be found in the Readings section.
| Date | Topics | Readings |
|---|---|---|
| 01/18 |
Course introduction and motivation.
Introduction to propositional logic. Satisfiability and related notions: validity and entailment. Decidability of propositional satisfiability. |
- [Bar04a]
- [Por01] (suggested) |
| 01/20 | Introduction to first-order logic. Syntax and semantics. | [Bar04a] |
| 01/25 | More on first-order logic. Satisfiability and related notions: validity and entailment. | [Bar04a] |
| 01/27 |
Basic notions of computability and decidability.
Undecidability of validity/satisfiability in first order logic.
Theories. validity/satisfiability modulo theories. |
[Bar04a] |
| 02/01 | First order logic with equality vs. first order logic withour equality. Embeddings of models and preservation properties. Normal models. Proof that the class of normal models is not elementary. | [TinEq1] |
| 02/03 |
The axioms of equality: the first order theory of equality.
Example of a non-normal model for this theory.
Reducibilty of the validity/satisfiability problem in normal models
to the validity/satisfiability problem in models of the theory of equality.
Deciding the validity of quantifier formulas modulo the theory of equality. Congruence closure over labeled directed graphs. |
[TinEq1] |
| 02/09 |
A basic congruence closure algorithm.
Discussion of the algorithm, its correctness and time complexity.
Using the CC algorithm to decide the satisfiability of
quantifier-free sets of equalities and disequalities.
Reducing the satisfiability of arbitrary quantifier free formulas to the above problem.
A faster CC algorithm. Discussion of the new algorithm. |
[TinEq1] |
| 02/10 | Introduction to rewriting. Reasoning about term equivalence by rewriting. Why congruence closure will not do. Rewriting as a simplification/normalization process. The rewriting relation on terms. Abstract reduction relations. Basic notation and definitions. | [TinRew1] |
| 02/15 | More on rewriting. Various notions of confluence and how they are related. Canonical forms. Using canonical rewrite systems to decide term equivalence. | [TinRew1] |
| 02/17 | Reduction orderings. Use of reduction ordering on terms to prove the termination of rewrite systems. A simple reduction ordering. More sophisticated reduction ordering: LPOs. Properties of LPOs. Example of using LPOs to check the termination of a rewrite system. | [TinRew1] |
| 02/22 |
Checking for convergence of terminating rewrite systems.
Critical pairs.
Coompletion and interreduction.
An abstract congruence closure procedure for equalities over constants. The rewriting approach. |
[TinRew1] and
[Tiw04a] |
| 02/24 | An abstract congruence closure procedure for equalities over ground terms. The derivation rules. Proof of soundness and termination. Proof that the rewrite system produced by the ACC algorithm from a system E of ground equalities is canonical and decides the equivalence modulo E of ground terms. | [Tiw04a] |
| 03/01 | Guest lecture by Albert Oliveras on efficient congruence closure algorithms and their extensions. | [Oli04a] |
| 03/03 | Guest lecture by Albert Oliveras on proof producing congruence closure algorithms. | [Oli04b] |
| 03/08 | Class replaced by colloquium talk by Rob Johnson. | |
| 03/10 |
Congruence closure modulo ACU.
Rules and examples.
Termination, soundness and completeness arguments.
Definition of Shostak theory. Convexity, canonizers, solvers. Examples. |
[Tiw-04b]
[Tin-Sho] |
| 03/15 | Springbreak. | |
| 03/17 | Springbreak. | |
| 03/22 | Review of Shostak theories. The Shostak decision procedure: a simplified version. The Shostak procedure as Gaussian elimination for Shostak theories. Termination of the procedure. Proof of soundness and completeness. | [Tin-Sho] |
| 03/24 | Quantifier elimination in first order theories. Uses of QE. Obtaining decision procedures for full first-order theories by means of QE. A QE procedure for the theory of dense linear orderings without endpoints. | [Tin-QE] |
| 03/29 | Correctness of the QE procedure for the theory of dense linear orderings without endpoints. | [Tin-QE] |
| 03/31 | Cooper's QE procedure for Presburger arithmetic. | [Tin-QE] |
| 04/05 | More on Cooper's QE procedure for Presburger arithmetic. | [Tin-QE] |
| 04/07 | Various theories of algebraic structure: groups, rings, fields. A QE method for the theories of algebraically closed fields. | [Bar04c] |
| 04/12 | More on quantifier elimination for the theory of algebraically closed fields. Correctness proof. | [Bar04c] |
| 04/14 | A specialized algorithm for the simultaneous elimination of quantifiers for closed existential formulas in the theory of algebraically closed fields. Polynomial rings over a field. Ideals in a ring. Generating set of an ideal. Groebner bases for polymomial rings. | [Bar04d] |
| 04/19 | Computing Groebner bases. A term rewriting view. Examples and exercises. |
[Bar04d] and
[Tiw04b] |