Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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 [11 references]  Display  Hide  Download

https://hal.univ-reunion.fr/hal-01912030
Contributor : Réunion Univ <>
Submitted on : Monday, November 5, 2018 - 9:33:04 AM
Last modification on : Monday, September 2, 2019 - 9:41:20 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

92

Files downloads

140