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.
Domains
Computer Science [cs]
Fichier principal
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...