Name
Abstract | ||
|---|---|---|
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 |
Year | DOI | Venue |
|---|---|---|
1980 | 10.1145/322217.322228 | J. ACM |
Keywords | Field | DocType |
Common Subexpression Problem,uniform word problem,decision procedure,relational database,expression equiva- lence,congruence closure,lossless join,unification,theory of equality,graph algorithm,common subexpresslon | Discrete mathematics,Computer science,Arithmetic | Journal |
Volume | Issue | ISSN |
27 | 4 | 0004-5411 |
Citations | PageRank | References |
193 | 78.51 | 21 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Peter J. Downey | 1 | 436 | 172.07 |
| Ravi Sethi | 2 | 2281 | 1029.21 |
| Robert Endre Tarjan | 3 | 25160 | 6384.61 |