@inproceedings{90e47d36bc93467cb0dc559420c8afe0,

title = "On ground reducibility problem for word rewriting systems with variables",

abstract = "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-linear, the question is decidable for arbitrary (linear or non-linear) w.",

keywords = "Decidability, Pattern languages, Rewriting, String matching",

author = "Gregory Kucherov and Michael Rusinowitch",

year = "1994",

month = apr,

day = "6",

doi = "10.1145/326619.326745",

language = "English",

series = "Proceedings of the ACM Symposium on Applied Computing",

publisher = "Association for Computing Machinery",

pages = "271--276",

booktitle = "1994 ACM Symposium on Applied Computing, SAC 1994",

note = "1994 ACM Symposium on Applied Computing, SAC 1994 ; Conference date: 06-03-1994 Through 08-03-1994",

}