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.
CITATION STYLE
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
Mendeley helps you to discover research relevant for your work.