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 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).
Complete list of metadatas

Cited literature [1 references]  Display  Hide  Download

http://hal.univ-reunion.fr/hal-01912030
Contributor : Réunion Univ <>
Submitted on : Monday, November 5, 2018 - 9:33:04 AM
Last modification on : Thursday, March 28, 2019 - 11:24:10 AM
Long-term archiving on : Wednesday, February 6, 2019 - 1:42:25 PM

File

1808.05065.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01912030, version 1
  • ARXIV : 1808.05065

Collections

Citation

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

Share

Metrics

Record views

49

Files downloads

68