Course Readings
Course Notes
| [Tin-Eq1] |
Equality
(1/1
4/1)
|
| [Tin-Rew1] |
Rewriting
(1/1
4/1)
|
| [Tin-Sho] |
Satisfiability modulo Shostak Theories
(1/1
4/1)
|
| [Tin-QE] |
Quantifier Elimination
(1/1
4/1)
|
Articles
| [Por01] |
Automated Reasoning
by Frederic Portoraro. In Edward N. Zalta editor The Stanford Encyclopedia of Philosophy. Fall 2001 Edition.
|
Books and Additional Course Notes
| [Bar04a] |
Overview and background
by C. Barrett. Lecture notes, New York University, 2004.
|
| [Bar04b] |
Decision Procedures for Equality I
by C. Barrett. Lecture notes, New York University, 2004.
|
| [Bar04c] |
Quantifier elimination for algebraically closed fields
by C. Barrett. Lecture notes, New York University, 2004.
|
| [Bar04d] |
Grobner Bases
by C. Barrett. Lecture notes, New York University, 2004.
|
| [Gan04] |
DPLL(T): Fast Decision Procedures.
by H. Ganzinger et al. CAV'04 presentation. July 2004.
|
| [Har04] |
Introduction to Logic and Automated Theorem Proving
by J. Harrison, Book draft, April 2004.
|
| [Nie05] |
Abstract DPLL and Abstract DPLL Modulo Theories.
by R. Nieuwenhuis et al. LPAR'04 presentation. March 2005.
|
| [Ohl97] |
Introductory Logic Course Notes
by H. J. Ohlbach. Lecture Notes, Imperial College, London, 1997 (see also related slides).
|
| [Oli04a] |
Lecture Notes on Congruence Closure and its Extensions.
by A. Oliveras, February 2005.
|
| [Oli04b] |
Lecture Notes on Proof Producing Congruence Closure.
by A. Oliveras, February 2005.
|
| [Tin04] |
DPLL-based checkers for satisfiability modulo (multiple) theories.
by C. Tinelli. CMU presentation. Octorber 2004.
|
| [Tiw04a] |
Lecture Notes on Abstract Congruence Closure.
by A. Tiwari, Summer School on Combination of Decision Procedures, August 2004.
|
| [Tiw04b] |
Lecture Notes on AC Abstract Congruence Closure.
by A. Tiwari, Summer School on Combination of Decision Procedures, August 2004.
|
Last Updated: May 3, 2005