Abstract : In this paper, we present an approach to non-termination of term rewriting systems inspired by a technique that was designed in the context of logic programming. Our method is based on a classical unfolding operation together with semi-unification and is independent of a particular reduction strategy. We also describe a technique to reduce the explosion of rules caused by the unfolding process. The analyser that we have implemented is able to solve most of the non-terminating examples in the Termination Problem Data Base.
https://hal.univ-reunion.fr/hal-01916159 Contributor : Réunion UnivConnect in order to contact the contributor Submitted on : Thursday, November 8, 2018 - 11:56:17 AM Last modification on : Tuesday, October 19, 2021 - 5:56:07 PM Long-term archiving on: : Saturday, February 9, 2019 - 2:18:46 PM
Etienne Payet. Detecting Non-Termination of Term Rewriting Systems Using an Unfolding Operator. 16th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'06), Jul 2006, Venise, Italy. pp.194-209. ⟨hal-01916159⟩