Report Number: CS-TR-77-646
Institution: Stanford University, Department of Computer Science
Title: Fast decision algorithms based on congruence closure
Author: Nelson, Charles Gregory
Author: Oppen, Derek C.
Date: February 1978
Abstract: We define the notion of the 'congruence closure' of a relation on a graph and give a simple algorithm for computing it. We then give decision procedures for the quantifier-free theory of equality and the quantifier-free theory of LISP list structure, both based on this algorithm. The procedures are fast enough to be practical in mechanical theorem proving: each procedure determines the satisfiability of a conjunction of length n of literals in time O($n^2$). We also show that if the axiomatization of the theory of list structure is changed slightly, the problem of determining the satisfiability of a conjunction of literals becomes NP-complete. We have implemented the decision procedures in our simplifier for the Stanford Pascal Verifier.
http://i.stanford.edu/pub/cstr/reports/cs/tr/77/646/CS-TR-77-646.pdf