Deciding the confluence of ordered term rewrite systems

ABSTRACT

replace me

REFERENCES

• 1: Bachmair, L. 1988. Proof by consistency in equational theories. In Proceedings of the Third Annual Symposium on Logic in Computer Science (Edinburgh, Scotland, July 5--8). IEEE Computer Society, Los Alamitos, CA, 228--233.
• 2: Leo Bachmair , Nachum Dershowitz, Equational inference, canonical proofs, and proof orderings, Journal of the ACM (JACM), v.41 n.2, p.236-276, March 1994 [doi>10.1145/174652.174655]
• 3: Bachmair, L., Dershowitz, N., and Hsiang, J. 1986. Orderings for equational proofs. In First IEEE Symposium on Logic in Computer Science, Cambridge, MA, June 16--18). IEEE Computer Society Press, Los Alamitos, CA, 346--357.
• 4: Bachmair, L., Dershowitz, N., and Plaisted, D. 1989. Completion whitout failure. In Resolution of Equations in Algebraic Structures, Volume 2: Rewriting Techniques, H. Aït-Kaci and M. Nivat, Ed. Academic Press, New York, chapter 1, 1--30.
• 5: Comon, H. 1990. Solving symbolic ordering constraints. Internat. J. Foundat. Comput. Sci. 1, 4, 387--411.
• 6: Hubert Comon , Ralf Treinen, The first-order theory of lexicographic path orderings is undecidable, Theoretical Computer Science, v.176 n.1-2, p.67-87, April 20, 1997 [doi>10.1016/S0304-3975(96)00049-7]
• 7: M. Dauchet, Simulation of turing machines by a left-linear rewrite rule, Proceedings of the 3rd international conference on Rewriting Techniques and Applications, p.109-120, January 1989
• 8: Dershowitz, N. 1982. Orderings for term-rewriting systems. Theoret. Comput. Sci. 17, 3, 279--301.
• 9: 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]
• 10: Nachum Dershowitz , Jean-Pierre Jouannaud , Jan Willem Klop, More Problems in Rewriting, Proceedings of the 5th International Conference on Rewriting Techniques and Applications, p.468-487, June 16-18, 1993
• 11: Nachum Dershowitz , Zohar Manna, Proving termination with multiset orderings, Communications of the ACM, v.22 n.8, p.465-476, Aug. 1979 [doi>10.1145/359138.359142]
• 12: Dershowitz, N. and Plaisted, D. 2001. Rewriting. In Handbook of Automated Reasoning, J. A. Robinson and A. Voronkov, Eds. Elsevier Science Publishers, Amsterdam, The Netherlands, and MIT Press, Cambridge, MA, 535--610.
• 13: Ganzinger, H., Nieuwenhuis, R., and Nivela, P. 2001. The Saturate System, 2001. Software and documentation available at http://www.mpi-sb.mpg.de/SATURATE/Saturate.html.
• 14: J. Hsiang , M. Rusinowitch, On word problems in equational theories, 14th International Colloquium on Automata, languages and programming, p.54-71, July 1987, Karlsruhe, Germany
• 15: Jouannaud, J.-P. and Kounalis, E. 1986. Automatic proofs by induction in equational theories without constructors. In Proceedings, Symposium on Logic in Computer Science (Cambridge, MA, June 16--18). IEEE Computer Society, Los Alamitos, CA, 358--366.
• 16: Deepak Kapur , David R. Musser, Proof by consistency, Artificial Intelligence, v.31 n.2, p.125-157, Feb. 1987 [doi>10.1016/0004-3702(87)90017-8]
• 17: Deepak Kapur , Paliath Narendran , Friedrich Otto, On ground-confluence of term rewriting systems, Information and Computation, v.86 n.1, p.14-31, May 1990 [doi>10.1016/0890-5401(90)90023-B]
• 18: D Kapur , P Narendran , G Sivakumar, A path ordering for proving termination of term rewriting systems, Proc. of the international joint conference on theory and practice of software development (TAPSOFT) Berlin, March 25-29, 1985 on Mathematical foundations of software development, Vol. 1: Colloquium on trees in algebra and programming (CAAP'85), p.173-187, April 1985, Berlin, Germany
• 19: Kirchner, C., Kirchner, H., and Rusinowitch, M. 1990. Deduction with symbolic constraints. Rev. Française d'Intelligence Artific. 4, 3, 9--52.
• 20: Knuth, D. E. and Bendix, P. B. 1970. Simple word problems in universal algebras. In Computational Problems in Abstract Algebra, J. Leech, Ed., Pergamon Press, Oxford, U.K., 263--297.
• 21: Pierre Lescanne, On the recursive decomposition ordering with lexicographical status and other related orderings, Journal of Automated Reasoning, v.6 n.1, p.39-49, Mar. 1990 [doi>10.1007/BF00302640]
• 22: Ursula Martin , Tobias Nipkow, Ordered rewriting and confluence, Proceedings of the tenth international conference on Automated deduction, p.366-380, July 1990, Kaiserslautern, Germany
• 23: Marvin Lee Minsky, Computation: Finite and Infinite Machines, Prentice-Hall, Inc., Upper Saddle River, NJ, 1967
• 24: Robert Nieuwenhuis, Simple LPO constraint solving methods, Information Processing Letters, v.47 n.2, p.65-69, Aug. 20, 1993 [doi>10.1016/0020-0190(93)90226-Y]
• 25: Robert Nieuwenhuis , Albert Rubio, Theorem proving with ordering and equality constrained clauses, Journal of Symbolic Computation, v.19 n.4, p.321-351, April 1995 [doi>10.1006/jsco.1995.1020]
• 26: Nieuwenhuis, R. and Rubio, A. In press. Paramodulation-based theorem proving. In Handbook of Automated Reasoning, J. A. Robinson and A. Voronkov, Eds. Elsevier Science Publishers, Amsterdam, The Netherlands, vol. 1, chap. 7. and MIT Press, Cambridge, MA.
• 27: Pilar Nivela , Robert Nieuwenhuis, Saturation of First-Order (Constrained) Clauses with the Saturate System, Proceedings of the 5th International Conference on Rewriting Techniques and Applications, p.436-440, June 16-18, 1993
• 28: Gerald E. Peterson, Complete sets of reductions with constraints, Proceedings of the tenth international conference on Automated deduction, p.381-395, July 1990, Kaiserslautern, Germany
• 29: Plaisted, D. A. 1985. Semantic confluence tests and completion methods. Inform. Contr. 65, 2/3 (May/June), 182--215.

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.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving

General Terms:
Theory, Verification

Keywords:
Rewrite systems, confluence, ordered rewriting, path orderings