Greg Nelson
Abstract
The notion of the congruence closure of a relation on a graph is defined and several algorithms for computing it are surveyed. A simple proof is given that the congruence closure algorithm provides a decision procedure for the quantifier-free theory of equality. A decision procedure is then given for the quantifier-free theory of LISP list structure based on the congruence closure algorithm. Both decision procedures determine the satisfiability of a conjunction of literals of length n in average time O(n log n) using the fastest known congruence closure algorithm. It is also shown 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. The decision procedures have been implemented in the authors' simplifier for the Stanford Pascal Verifier.
- 1 ACKERMANN, W Solvable Cases of the Dectston Problem North-Holland, Amsterdam, 1954Google Scholar
- 2 Ago, A V, HOPCROFT, J E, AND ULLMANN, J D The Design and Analysts of Computer Algorithms Addison-Wesley, Reading, Mass 1974 Google Scholar
- 3 DOWNEY, P. J, SETHI, R, AND TARJAN, R E. Var,auons on the common subexpresslon problem To appear m J. A CM. Google Scholar
- 4 Kozt~N, D. Complexity of finitely represented algebras. Proc. 9th Annual ACM Symp. on Theory of Comptg., Boulder, Colo., May 1977, pp. 164-177. Google Scholar
- 5 NELSON, C G., AND OPP~N, D. C Fast decision procedures based on UNION and'FIND. Proc E,ghteenth Annual Symp on Foundauons of Comptr. Sct, Providence, R I., 1977 (This is an earher verston of the present paper.)Google Scholar
- 6 NELSON, C G., AND OPPEN, D. C Stmphfieation by cooperating dec,slon procedures To be pubhshedGoogle Scholar
- 7 OPPEN, D C. Reasoning about recurstvely defined data structures Proc 5th ACM Syrup on Principles of Programming Lanl~uages, Tucson, Anz, January 1978, pp 151-157 Google Scholar
- 8 SHOSTAK, R An algorithm for reasomng about equahty Comm ACM 21, 7 (July 1978), 583-585 Google Scholar
- 9 TARJAN, R. E Efftctency of a good but not linear set umon algortthm J ACM 22, 2 (April 1975), 2t5-225 Google Scholar
Index Terms
- Fast Decision Procedures Based on Congruence Closure
Recommendations
Abstract Congruence Closure
We describe the concept of an abstract congruence closure and provide equational inference rules for its construction. The length of any maximal derivation using these inference rules for constructing an abstract congruence closure is at most quadratic ...
Factor Congruence Lifting Property
In previous work, we have introduced and studied a lifting property in congruence---distributive universal algebras which we have defined based on the Boolean congruences of such algebras, and which we have called the Congruence Boolean Lifting ...
Comments