We consider quantifier free formulae of a first order theory without funcctions and with predicates x rewrites to y in one step with given rewrite ssytems.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 veryf restricted classes of rewriting systems (e.g. linear,shallow and convergent in [STTT98]).Decidability of the positive existential fragment has been shown in [NPR97].
展开▼
