BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-77-646
       ENTRY:: June 28, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Fast decision algorithms based on congruence closure
        TYPE:: Technical Report
      AUTHOR:: Nelson, Charles Gregory
      AUTHOR:: Oppen, Derek C.
        DATE:: February 1978
       PAGES:: 14
    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.
       NOTES:: [Adminitrivia V1/Prg/19950628]
         END:: STAN//CS-TR-77-646