Guided Unfoldings for Finding Loops in Standard Term Rewriting

TL;DR

This paper introduces a guided unfolding technique for detecting loops in standard term rewriting, improving efficiency and success rate by using position-guided depth-first computation, implemented in the NTI tool.

Contribution

It presents a novel guided unfolding method that enhances loop detection in term rewriting by incorporating position guidance and depth-first computation, outperforming previous breadth-first approaches.

Findings

Faster loop detection times

Higher success rate in proofs

Effective in various rewrite systems

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).