An algorithm for finding canonical sets of ground rewrite rules in polynomial time
- 2 January 1993
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 40 (1) , 1-16
- https://doi.org/10.1145/138027.138032
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(n 3 ) .Keywords
This publication has 12 references indexed in Scilit:
- Theorem proving using equational matings and rigid E -unificationJournal of the ACM, 1992
- Rigid E-unification: NP-completeness and applications to equational matingsInformation and Computation, 1990
- Termination of rewritingJournal of Symbolic Computation, 1987
- A finite thue system with decidable word problem and without equivalent finite canonical systemTheoretical Computer Science, 1985
- On Matrices with ConnectionsJournal of the ACM, 1981
- Theorem Proving via General MatingsJournal of the ACM, 1981
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting SystemsJournal of the ACM, 1980
- Variations on the Common Subexpression ProblemJournal of the ACM, 1980
- Fast Decision Procedures Based on Congruence ClosureJournal of the ACM, 1980
- Tautology testing with a generalized matrix reduction methodTheoretical Computer Science, 1979