HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Detecting Non-Termination of Term Rewriting Systems Using an Unfolding Operator

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [24 references]  Display  Hide  Download

Contributor : Réunion Univ Connect 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


Explicit agreement for this submission


  • HAL Id : hal-01916159, version 1



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⟩



Record views


Files downloads