Confluence of Logically Constrained Rewrite Systems Revisited
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866914851697197056 |
|---|---|
| author | Schöpf, Jonas Mitterwallner, Fabian Middeldorp, Aart |
| author_facet | Schöpf, Jonas Mitterwallner, Fabian Middeldorp, Aart |
| contents | We show that (local) confluence of terminating locally constrained rewrite systems is undecidable, even when the underlying theory is decidable. Several confluence criteria for logically constrained rewrite systems are known. These were obtained by replaying existing proofs for plain term rewrite systems in a constrained setting, involving a non-trivial effort. We present a simple transformation from logically constrained rewrite systems to term rewrite systems such that critical pairs of the latter correspond to constrained critical pairs of the former. The usefulness of the transformation is illustrated by lifting the advanced confluence results based on (almost) development closed critical pairs as well as on parallel critical pairs to the constrained setting. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_13552 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Confluence of Logically Constrained Rewrite Systems Revisited Schöpf, Jonas Mitterwallner, Fabian Middeldorp, Aart Logic in Computer Science We show that (local) confluence of terminating locally constrained rewrite systems is undecidable, even when the underlying theory is decidable. Several confluence criteria for logically constrained rewrite systems are known. These were obtained by replaying existing proofs for plain term rewrite systems in a constrained setting, involving a non-trivial effort. We present a simple transformation from logically constrained rewrite systems to term rewrite systems such that critical pairs of the latter correspond to constrained critical pairs of the former. The usefulness of the transformation is illustrated by lifting the advanced confluence results based on (almost) development closed critical pairs as well as on parallel critical pairs to the constrained setting. |
| title | Confluence of Logically Constrained Rewrite Systems Revisited |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2402.13552 |