Guided Unfoldings for Finding Loops in Standard Term Rewriting - Université de La Réunion
Pré-Publication, Document De Travail Année : 2018

Guided Unfoldings for Finding Loops in Standard Term Rewriting

Résumé

In this paper, we reconsider the unfolding-based technique that we have introduced previously for detecting loops in standard term rewriting. We improve it by guiding the unfolding process, using distinguished positions in the rewrite rules. This results in a depth-first computation of the unfoldings, whereas the original technique was breadth-first. We have implemented this new approach in our tool NTI and compared it to the previous one on a bunch of rewrite systems. The results we get are promising (better times, more successful proofs).
Fichier principal
Vignette du fichier
1808.05065.pdf (189.36 Ko) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01912030 , version 1 (05-11-2018)

Identifiants

Citer

Etienne Payet. Guided Unfoldings for Finding Loops in Standard Term Rewriting. 2018. ⟨hal-01912030⟩

Relations

70 Consultations
122 Téléchargements

Altmetric

Partager

More