A New Result about the Decidability of the Existential One-step
Rewriting Theory

Sebastien Limet and Pierre Rety

Abstract:
We give a decision procedure for the whole existential fragment of
one-step rewriting first-order theory, in the case where rewrite systems
are linear, non left-left-overlapping (i.e. without critical pairs), and
non epsilon-left-right-overlapping (i.e. no left-hand-side overlaps
on top with the right-hand-side of the same rewrite rule).
The procedure is defined by means of tree-tuple synchronized grammars.