On ground reducibility problem for word rewriting systems with variables
Grégory Kucherov, Michaël Rusinowitch · 1994
Given a word rewriting system with variables R and a word with variables w, the question we are interested in is whether all the instances of w obtained by substituting its variables by non-empty words are reducible by R.This property is known as ground reducibility and is the core of the inductive completion methods that have been designed for proving theorems in the initial model of equational specifications.We prove the problem to be generally undecidable even for a very simple word w, namely axa where a is a letter and x a variable.When R is left-hnear, the question is decidable for arbitrary (linear or non-linear) w.