Deciding fundamental properties of right-(ground or variable) rewrite systems by rewrite closure

10Citations
Citations of this article
1Readers
Mendeley users who have this article in their library.
Get full text

Abstract

Right-(ground or variable) rewrite systems (RGV systems for short) are term rewrite systems where all right hand sides of rules are restricted to be either ground or a variable. We define a minimal rewrite extension R̄ of the rewrite relation induced by a RGV system R. This extension admits a rewrite closure presentation, which can be effectively constructed from R. The rewrite closure is ' used to obtain decidability of the reachability, joinability, termination, and confluence properties of the RGV system R. We also show that the word problem and the unification problem are decidable for confluent RGV systems. We analyze the time complexity of the obtained procedures; for shallow RGV systems, termination and confluence are exponential, which is the best possible result since all these problems are EXPTIME-hard for shallow RGV systems.

Cite

CITATION STYLE

APA

Godoy, G., & Tiwari, A. (2004). Deciding fundamental properties of right-(ground or variable) rewrite systems by rewrite closure. In Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science) (Vol. 3097, pp. 91–106). Springer Verlag. https://doi.org/10.1007/978-3-540-25984-8_5

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free