Skip to Main content Skip to Navigation
New interface
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