An algorithm for finding canonical sets of ground rewrite rules in polynomial time

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).

REFERENCES

• 1: Peter B. Andrews, Theorem Proving via General Matings, Journal of the ACM (JACM), v.28 n.2, p.193-214, April 1981 [doi>10.1145/322248.322249]
• 2: L. Bachmair, Proof methods for equational theories, University of Illinois, Department of Computer Science, Urbana, IL, 1987
• 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.
• 4: ~BmEL, W. Tautology testing with a generalized matrix reduction method. Theoret. Comput. ~Sci. 8 (1979), 31-44.
• 5: Wolfgang Bibel, On Matrices with Connections, Journal of the ACM (JACM), v.28 n.4, p.633-645, Oct. 1981 [doi>10.1145/322276.322277]
• 6: ~BmEL, W. Automated Theorem Prot,ing. Friedr. Vieweg & Sohn, Braunschweig, Germany, ~1982.
• 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.
• 8: Nachum Dershowitz, Termination of rewriting, Journal of Symbolic Computation, v.3 n.1-2, p.69-116, Feb./April 1987 [doi>10.1016/S0747-7171(87)80022-6]
• 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.
• 10: Peter J. Downey , Ravi Sethi , Robert Endre Tarjan, Variations on the Common Subexpression Problem, Journal of the ACM (JACM), v.27 n.4, p.758-771, Oct. 1980 [doi>10.1145/322217.322228]
• 11: Jean H. Gallier, Logic for computer science: foundations of automatic theorem proving, Harper & Row Publishers, Inc., New York, NY, 1985
• 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.
• 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.
• 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.
• 15: Jean Gallier , Paliath Narendran , David A. Plaisted , Wayne Snyder, Rigid E-unification: NP-completeness and applications to equational matings, Information and Computation, v.87 n.1-2, p.129-195, July/August 1990 [doi>10.1016/0890-5401(90)90061-L]
• 16: Jean Gallier , Paliath Narendran , Stan Raatz , Wayne Snyder, Theorem proving using equational matings and rigid E-unification, Journal of the ACM (JACM), v.39 n.2, p.377-430, April 1992 [doi>10.1145/128749.128754]
• 17: Gérard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM (JACM), v.27 n.4, p.797-821, Oct. 1980 [doi>10.1145/322217.322230]
• 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.
• 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.
• 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.{
• 21: Dexter Kozen, Complexity of Finitely Presented Algebras, Cornell University, Ithaca, NY, 1976
• 22: Dexter Kozen, Complexity of finitely presented algebras, Proceedings of the ninth annual ACM symposium on Theory of computing, p.164-177, May 04-04, 1977, Boulder, Colorado, United States [doi>10.1145/800105.803406]
• 23: M. S. Krishnamoorthy , P. Narendran, On recursive path ordering, Theoretical Computer Science, v.40 n.2-3, p.323-328, Nov. 1985
• 24: ~LANKFORD, D.S. Canonical inference. Rep. ATP-32. Univ. Texas, Houston, Tex. 1975.
• 25: Greg Nelson , Derek C. Oppen, Fast Decision Procedures Based on Congruence Closure, Journal of the ACM (JACM), v.27 n.2, p.356-364, April 1980 [doi>10.1145/322186.322198]
• 26: F. Otto , C. Squier, The word problem for finitely presented monoids and finite canonical rewriting systems, on Rewriting techniques and applications, p.74-82, May 1987, Bordeaux, France
• 27: ~SNYDER, W. A note on the complexity of simplification ordering. Tech. Rep. BU-8909. ~Boston Univ. Boston, Mass., 1989.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.2 Grammars and Other Rewriting Systems
          Subjects: Decision problems

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Computations on discrete structures
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Functional constructs
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving
      F.4.3 Formal Languages
          Subjects: Classes defined by grammars or automata (e.g., context-free languages, regular sets, recursive sets)

General Terms:
Algorithms, Design, Languages, Theory

Keywords:
completion procedures, congruence closure, equational logic, term rewriting