Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules%

Guillem Godoy and Ashish Tiwari

Presented at CADE 2005, Tallinn, Estonia, July 22-27, 2005. © Springer-Verlag. The final version will appear at the Springer LNCS proceedings site or the Springer LNCS site.

Abstract

We show that termination is decidable for rewrite systems that contain shallow and right-linear rules, collapsing rules, and right-ground rules. This class of rewrite systems is expressive enough to include interesting rules. Our proof uses the fact that this class of rewrite systems is known to be regularity-preserving and hence the reachability and joinability problems are decidable. Decidability of termination is obtained by analyzing the nonterminating derivations.

postscript or pdf. Springer link will appear here soon.

Slides

Slides of the presentation at CADE'05 may be put up here later ...

BibTeX Entry


@inproceedings{GodoyTiwari05:CADE,
	author = "G. Goody and A. Tiwari",
	title = "Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules",
	booktitle = "20th Intl. Conf. on Automated Deduction, CADE",
	EDITOR = "Nieuwenhuis, R.",
	pages = "164--176",
	series = {LNCS},
	volume = 3632,
	PUBLISHER = {Springer},
	MONTH = jul,
	YEAR = 2005
}
Return to the Ashish's home page
Return to the Computer Science Laboratory home page