Guided Unfoldings for Finding Loops in Standard Term Rewriting
Programming Languages
2018-11-09 v2 Logic in Computer Science
Abstract
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).
Cite
@article{arxiv.1808.05065,
title = {Guided Unfoldings for Finding Loops in Standard Term Rewriting},
author = {Etienne Payet},
journal= {arXiv preprint arXiv:1808.05065},
year = {2018}
}
Comments
Pre-proceedings paper presented at the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2018), Frankfurt am Main, Germany, 4-6 September 2018 (arXiv:1808.03326)