Detecting Non-Termination of Term Rewriting Systems Using an Unfolding Operator - Université de La Réunion
Conference Papers Year : 2006

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.
Fichier principal
Vignette du fichier
Detecting_non_termination_of_term_rewriting_systems_using_an_unfolding_operator.pdf (212.16 Ko) Télécharger le fichier
Origin Explicit agreement for this submission
Loading...

Dates and versions

hal-01916159 , version 1 (08-11-2018)

Identifiers

  • HAL Id : hal-01916159 , version 1

Cite

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⟩
49 View
150 Download

Share

More