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 modify it by guiding the unfolding process, using disagreement pairs in rewrite rules. This results in a partial computation of the unfoldings, whereas the original technique consists of a thorough computation followed by a mechanism for eliminating some rules. We have implemented this new approach in our tool NTI and conducted successful experiments on a large set of term rewrite systems.
Domaines
Logique en informatique [cs.LO]Origine | Fichiers produits par l'(les) auteur(s) |
---|