Journal of the ACM · 1980 · 350 citations · 11 references
ComputingComputer ScienceAlgorithmsComputational LinguisticsNatural Language ProcessingFrequency AnalysisSource DescriptionCommon Subexpression Elimination
Let G be a directed graph such that for each vertex v in G, the successors of v are ordered Let C be any equivalence relation on the vertices of G. The congruence closure C* of C is the finest equivalence relation containing C and such that any two vertices having corresponding successors equivalent under C* are themselves equivalent under C* Efficient algorithms are described for computing congruence closures in the general case and in the following two special cases. 0) G under C* is acyclic, and (it) G is acychc and C identifies a single pair of vertices. The use of these algorithms to test expression eqmvalence (a problem central to program verification) and to test losslessness of joins in relational databases is described
11
Fast Decision Procedures Based on Congruence Closure
Greg Nelson, Derek C. Oppen · Journal of the ACM · 1980 · 509 citations · Full text
Mike Paterson, Mark N. Wegman · Journal of Computer and System Sciences · 1978 · 280 citations
Robert E. Tarjan, Andrew Chi-Chih Yao · Communications of the ACM · 1979 · 207 citations · Full text