Deciding Fundamental Properties of Right-(Ground or Variable) Rewrite Systems by Rewrite Closure

Guillem Godoy and Ashish Tiwari

Presented at IJCAR 2004, Cork, Ireland, July 6--8 2004, © Springer-Verlag.

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 $\cl{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.

gzipped postscript or postscript.

Slides

First version of the slides of the presentation at IJCAR'04 are available here in postscript format.

BibTeX Entry


@inproceedings{GodoyTiwari04:IJCAR,
	TITLE = {Deciding Fundamental Properties of Right-(Ground or Variable)
Rewrite Systems by Rewrite Closure},
	AUTHOR = {Godoy, G. and Tiwari, A.},
	BOOKTITLE = {Intl. Joint Conf. on Automated Deduction, IJCAR},
	EDITOR = "Basin, D. and Rusinowitch, M.",
	PAGES = {91--106},
	PUBLISHER = {Springer},
	SERIES = {LNAI},
	VOLUME = "3097
	MONTH = jul,
	YEAR = 2004
}
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page