[Back]

G. Salzer, S Limet:
"Proving Properties of Term Rewrite Systems via Logic Programs";
in: "Rewriting Techniques and Applications: 15th International Conference, RTA 2004, Aachen, Germany, June 3-5, 2004", V van Oostrom (ed.); Springer, LNCS 3091, 2004, ISBN: 3-540-22153-0, 170 - 184.

We present a general translation of term rewrite systems (TRS) to logic programs such that basic rewriting derivations become logic deductions. Certain TRS result in so-called cs-programs, which were originally studied in the context of constraint systems and tree tuple languages. By applying decidability and computability results of cs-programs we obtain new classes of TRS that have nice properties like decidability of unification, regular sets of descendants or finite representations of R-unifiers. Our findings generalize former results in the field of term rewriting.

http://aleph.ub.tuwien.ac.at/F?base=tuw01&func=find-c&ccl_term=AC04968655