Guided Unfoldings for Finding Loops in Standard Term Rewriting
Abstract
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.
Origin | Files produced by the author(s) |
---|
![]()
Has part hal-01912030 Preprint Etienne Payet. Guided Unfoldings for Finding Loops in Standard Term Rewriting. 2018. ⟨hal-01912030⟩