Abstract
We show that the termination of ground term-rewriting systems is decidable in polynomial time. This result is extended to ground rational term-rewriting systems. We apply this result to show that the problem of determining whether there exists a simplification ordering over a possibly extended signature, satisfying a set of stict inequalities between terms, is decidable in polynomial time. As a simple consequence, it is decidable in polynomial time whether there exists a simplification ordering which shows that a ground term rewriting system terminates.
This research was partially supported by the National Science Foundation under grant CCR-9108904
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
G. Alexander and D. Plaisted. Proving equality theorems with hyper-linking. In Proceedings of the 11th International Conference on Automated Deduction, pages 706–710, 1992. system abstract.
H. Comon. Solving inequations in term algebras. In Proceedings of 5th IEEE Symposium on Logic in Computer Science, pages 62–69, 1990.
G. Huet and D. Lankford. On the uniform halting problem for term rewriting systems. Technical Report Rapport Laboria 283, IRIA, Le Chesnay, France, 1978.
Jean-Pierre Jouannaud and Claude Kirchner. Solving equations in abstract algebras: A rule-based survey of unification. In J.-L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT Press, Cambridge, MA, 1991. To appear.
Jean-Pierre Jouannaud and Mitsuhiro Okada. Satisfiability of systems of ordinal notations with the subterm property is decidable. In Proceedings of the Eighteenth EATCS Colloquium on Automata, Languages and Programming, Madrid, Spain, July 1991. Vol. 510 in Lecture Notes in Computer Science, Springer, Berlin.
C. Kirchner, H. Kirchner, and M. Rusinowitch. Deduction with symbolic constraints. Revue Francaise d'Intelligence Artificielle, 4(3):9–52, 1990.
S. Kamin and J.-J. Levy. Two generalizations of the recursive path ordering. Unpublished, February 1980.
J.B. Kruskal. Well-quasi-ordering, the tree theorem, and vazsonyi's conjecture. Transactions of the American Mathematical Society, 95:210–225, 1960.
R. Nieuwenhuis and A. Rubio. Theorem proving with ordering constrained clauses. In Proceedings of the 11th International Conference on Automated Deduction, pages 477–491, July 1992.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Plaisted, D.A. (1993). Polynomial time termination and constraint satisfaction tests. In: Kirchner, C. (eds) Rewriting Techniques and Applications. RTA 1993. Lecture Notes in Computer Science, vol 690. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-21551-7_30
Download citation
DOI: https://doi.org/10.1007/978-3-662-21551-7_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56868-1
Online ISBN: 978-3-662-21551-7
eBook Packages: Springer Book Archive