**
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