A New Result about the Decidability of the Existential One-Step Rewriting Theory
Sébastien Limet, Pierre Réty · 1998
. 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 ffl-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. 1 Introduction Given a signature \\Sigma , the theory of one-step rewriting for a finite rewrite system is the first order theory over the universe of ground \\Sigma -terms that uses the only predicate symbol !, where x ! y means x rewrites into y by one step. It has been shown undecidable in [11]. Sharper undecidability results have been obtained for some subclasses of rewrite systems, about the 9 8 -fragment [10, 8] and the 9 8 9 -fragment [12]. It has been shown decidable for the positive existential fragment [9], in the case of unary signatures [3], in the case ...