Basic Rewriting via Logic Programming, with an Application to the Reachability Problem
Sébastien Limet, Gernot Salzer · HAL (Le Centre pour la Communication Scientifique Directe) · 2006
We present a general translation of term rewrite systems to logic programs such that basic rewriting derivations become logic deductions. Certain rewrite systems result in so-called cs-programs, which were originally studied in the context of constraint systems and tree tuple languages. By applying results of cs-programs we obtain new classes of rewrite systems that preserve recognizability (i.e. systems with the property that the terms reachable from a regular set of terms by rewriting form again a regular set). Our findings generalize previous results in the field of term rewriting and can be useful for reachability problems originating for example from the verification of infinite state systems.