Deciding Confluence of Certain Term Rewriting Systems
in Polynomial Time
Ashish Tiwari
To appear in
LICS 2002,
which is being held as part of
FLoC 2002,
Copenhagen, Denmark, July 20--Aug 1, 2002.
Abstract
We present a polynomial time algorithm for deciding confluence of
ground term rewrite systems. We generalize the decision procedure
to get a polynomial time algorithm, assuming that the maximum arity
of a symbol in the signature is a constant, for deciding confluence
of rewrite systems where each rule contains a shallow linear term
on one side and a ground term on the other. The existence of a
polynomial time algorithm for deciding confluence of ground rewrite
systems was open for a long time and was independently solved only
recently by Comon, Godoy, and Nieuwenhuis [FoCS 2001]. Our decision
procedure is based on the concepts of abstract congruence closure
and abstract rewrite closure, which have been described by Bachmair
and Tiwari [CADE 2000] and Tiwari [FSTTCS 2001], respectively.
pdf
See also
the journal version of this paper (co-authored with Godoy and Nieuwenhuis):
click here.
Slides
pdf
BibTeX Entry
@inproceedings{Tiwari02:FLoC,
TITLE = {Deciding Confluence of Certain Term Rewriting Systems in Polynomial Time},
AUTHOR = {A. Tiwari},
BOOKTITLE = {{IEEE} Symposium on Logic in Computer Science, LICS 2002},
EDITOR = {Gordon Plotkin},
PAGES = {447--456},
PUBLISHER = {IEEE Society},
MONTH = July,
YEAR = 2002
}
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page