Deciding the satisfiability of quantifier free formulae on one-step rewriting

Abstract

We consider quantifier free formulae of a first order theory without functions and with predicates x rewrites to y in one step with given rewrite systems. Variables are interpreted in the set of finite trees. The full theory is undecidable [Tre96] and recent results [STT97], [Mar97], [Vor97] have strengthened the undecidability result to formulae with small prefixes (∃∗∀∗) and very restricted classes of rewriting systems (e.g. linear, shallow and convergent in [STTT98]). Decidability of the positive existential fragment has been shown in [NPR97]. We give a decision procedure for positive and negative existential formulae in the case when the rewrite systems are quasi-shallow, that is all variables in the rewrite rules occur at depth one. Our result extends to formulae with equalities and memberships relations of the form x ∈ L where L is a recognizable set of terms.