A new result about the decidability of the existential one-step rewriting theory

摘要

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~2).The procedure is defined by means of tree-tuple synchronized grammars.