THE FIRST-ORDER THEORY OF LINEAR ONE-STEP REWRITING IS UNDECIDABLE

The theory of one-step rewriting for a given rewrite system R and sign ature Sigma is the first-order theory of the following structure: its universe consists of all C-ground terms, and its only predicate is the relation ''x rewrites to y in one step by R''. The structure contains no function symbols and no equality. We show that there is no algorit hm deciding the There Exists*For All*-fragment of this theory for an a rbitrary finite, linear and non-erasing term-rewriting system. With th e same technique we prove that the theory of encompassment plus one-st ep rewriting by the rule f(x) --> g(x) and the modal theory of one-ste p rewriting are undecidable. (C) 1998 - Elsevier Science B.V. All righ ts reserved.