Jean Gallier
Paliath Narendran
Abstract
In this paper, it is shown that there is an algorithm that, given by finite set E of ground equations, produces a reduced canonical rewriting system R equivalent to E in polynomial time. This algorithm based on congruence closure performs simplification steps guided by a total simplification ordering on ground terms, and it runs in time O(n3).
- 1 ~ANDREWS, P. Theorem proving via general matings. J. ACM 28, 2 (1981), 193-214. Google Scholar
- 2 ~BACHMAIR, L. Proof methods for equational theories. Ph.D dissertation, Univ. Illinois, ~Urbana-Champaign, Ill., 1987. Google Scholar
- 3 ~BACHMAIR, L., DERSHOWITZ, N., AND PEAISTED, D. Completion without failure. In Resoh~- ~non of Equations in Algebraic Structures, vol. 2. H. A'/t-Kaci and M. Nivat, Eds. Academic ~Press, Orlando, Fla., 1989, pp. 1-30.Google Scholar
- 4 ~BmEL, W. Tautology testing with a generalized matrix reduction method. Theoret. Comput. ~Sci. 8 (1979), 31-44.Google Scholar
- 5 ~BmEL, W. On matrices with connections. J. ACM 28, 4 (Oct. 1981), 633-645. Google Scholar
- 6 ~BmEL, W. Automated Theorem Prot,ing. Friedr. Vieweg & Sohn, Braunschweig, Germany, ~1982.Google Scholar
- 7 ~DAUCHET, M., T1SON, S., HEU{LLARD, T., AND LESCANNE, P. Decidability of the confluence ~of ground term rewriting systems. In Proceedings of the LICS'87 (Ithaca, N.Y.). IEEE, New ~York, 1987, pp. 353-359.Google Scholar
- 8 ~DERSnOWITZ, N. Termination of Rewriting, J. Symb. Comput. 3 (1987), 69-116. Google Scholar
- 9 ~DERSHOWITZ, N. Completion and its applications, In Resolution of Equations in Algebraic ~Structures, vol. 2. H. A'it-Kaci and M. Nivat, Eds. Academic Press, Orlando, Fla., 1989, pp. ~31-85.Google Scholar
- 10 ~DOWNEY, P. J., SETHI, R. AND TARJAN, R. E. Variations on the common subexpression ~problem. J. ACM 27, 4 (Oct. 1980), 758 771. Google Scholar
- 11 ~GALLIER, J. H. Logic for Computer Science: Foundations of Automatic Theorem ProL,ing. ~Harper and Row, New York, 1986. Google Scholar
- 12 ~GALLIER, J. H., RAATZ, S., AND SNYDER, W. Theorem proving using rigid E-unification: ~Equational matings. In Proceedings of the L1CS'87 (Ithaca, N.Y.). IEEE, New York, 1987, pp. ~338-346.Google Scholar
- 13 ~GALLmR, J. H., NARENDRAN, P., PLAISTED, D., AND SNYDER, W. Rigid E-unification is ~NP-complete. In Proceedings of the LICS'88 (Edinburgh, Scotland, July 5-8). IEEE, New ~York, 1988, pp. 218-227.Google Scholar
- 14 ~GALLIER, J. H., RAATZ, S. AND SNYDER, W. Rigid E-unification and its applications to ~equational matings. In ResolWton of Equattons in Algebraic Stnlctures, vol. 1. H. A'it-Kaci and ~M. Nivat, Eds. Academic Press, Orlando, Fla., 1989, pp. 151 216.Google Scholar
- 15 ~GALLIER, J. H., NARENDRAN, P., PLAISTED, D., AND SNYDER, W. Rigid E-unification: ~NP-completeness and applications to theorem proving, bzf. Comput. 87, 1/2 (special issue) ~(1990), pp. 129-195. Google Scholar
- 16 ~GALt.mR, J. H., NARENDRAN, P., RAATZ, S., AND SNYDER, W. Theorem proving using ~equational matings and rigid E-unification. J. ACM 30. 2 (Apr. 1992). 377-429. Google Scholar
- 17 ~HUET, G. Confluent reductions: Abstract properties and applications to term rewriting ~systems. J. ACM 27, 4 (Oct. 1980), 797-821. Google Scholar
- 18 ~HUET, G., AND OPPEN, D.C. Equations and rewrite rules: A survey. In Formal Languages: ~Perspectwes and Open Problems, R. V. Book, Ed. Academic Press, Orlando, Fla., 1982.Google Scholar
- 19 ~KAPUR, D., AND NARENDRAN, P. A finite thue system with decidable word problem and ~without equivalent finite canonical system. Theoret. Compt~t. Sct. 35 (1985), 337-344.Google Scholar
- 20 ~KNUTH, D. n., AND BENDIX, P.B. Simple word problems in univeral algebras. In Cor~Tputa- ~tional Problems in .4bstractAlgebra, J. Leech, Ed. Pergamon Press, New York, 1970.{Google Scholar
- 21 ~KOZEN, D. Complexity of finitely presented algebras. Tech. Rep. TR 76-294. Dept. Comput. ~Sci. Cornell Univ., Ithaca, N.Y., 1976. Google Scholar
- 22 ~ KOZEN, D. Complexity of finitely presented algebras. In Proceedings of the 9th ,4nnual ~Symposium on Theoly of Compzltzng, (Boulder, Colo., May). ACM, New York, 1977, pp. ~64-177. Google Scholar
- 23 ~KRISHNAMOORTHY, M. S., AND NARENDRAN, P. On recursive path ordering. Theoret. Cornput. ~Scl. 40 (1985), 323-328. Google Scholar
- 24 ~LANKFORD, D.S. Canonical inference. Rep. ATP-32. Univ. Texas, Houston, Tex. 1975.Google Scholar
- 25 ~NELSON, G. AND OPPEN, D. C. Fast decision procedures based on congruence closure. J. ~ACM 27, 2 (Apr. 1980), 356-364. Google Scholar
- 26 ~OTTO, F., AND SQUIER, C. The word problem for finitely presented monoids and finite ~pp. 74-82. Google Scholar
- 27 ~SNYDER, W. A note on the complexity of simplification ordering. Tech. Rep. BU-8909. ~Boston Univ. Boston, Mass., 1989.Google Scholar
Index Terms
- An algorithm for finding canonical sets of ground rewrite rules in polynomial time
Recommendations
Congruence closure of compressed terms in polynomial time
FroCoS'11: Proceedings of the 8th international conference on Frontiers of combining systemsThe word-problem for a finite set of equational axioms between ground terms is the question whether for terms s, t the equation s = t is a consequence. We consider this problem under grammar based compression of terms, in particular compression with ...
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 ...
Orienting rewrite rules with the Knuth--Bendix order
RTA 2001We consider two decision problems related to the Knuth-Bendix order (KBO). The first problem is orientability: given a system of rewrite rules R, does there exist an instance of KBO which orients every ground instance of every rewrite rule in R. The ...
Reviews
Franz Winkler
Since every algebra of ground terms admits a total reduction ordering, Knuth-Bendix type completion procedures do not fail on input sets consisting of ground equations, and terminate with a canonical system equivalent to the input set. The new result proven in this paper is that such an equivalent canonical system can be computed in polynomial time depending on the size of the input. The fact that congruence closures of finite sets of ground equations can be computed efficiently is vital for the argument. The authors give a detailed and readable proof of the main result. The examples are helpful for gaining an intuitive understanding of the basic notions and the main algorithm Reduce. The extremely long period between receiving the paper (in 1985) and finally publishing it (in 1993) is frustrating for a community that depends on reasonably fast dissemination of results.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments