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 metadatas

Cited literature [24 references]  Display  Hide  Download

http://hal.univ-reunion.fr/hal-01916159
Contributor : Réunion Univ <>
Submitted on : Thursday, November 8, 2018 - 11:56:17 AM
Last modification on : Thursday, March 28, 2019 - 11:24:11 AM
Long-term archiving on : Saturday, February 9, 2019 - 2:18:46 PM

File

Detecting_non_termination_of_t...
Explicit agreement for this submission

Identifiers

  • HAL Id : hal-01916159, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

42

Files downloads

68