Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2309.12112 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929584289611776 |
|---|---|
| author | Schöpf, Jonas Middeldorp, Aart |
| author_facet | Schöpf, Jonas Middeldorp, Aart |
| contents | Numerous confluence criteria for plain term rewrite systems are known. For logically constrained rewrite system, an attractive extension of term rewriting in which rules are equipped with logical constraints, much less is known. In this paper we extend the strongly-closed and (almost) parallel-closed critical pair criteria of Huet and Toyama to the logically constrained setting. We discuss the challenges for automation and present crest, a new tool for logically constrained rewriting in which the confluence criteria are implemented, together with experimental data. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2309_12112 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Confluence Criteria for Logically Constrained Rewrite Systems (Full Version) Schöpf, Jonas Middeldorp, Aart Logic in Computer Science Numerous confluence criteria for plain term rewrite systems are known. For logically constrained rewrite system, an attractive extension of term rewriting in which rules are equipped with logical constraints, much less is known. In this paper we extend the strongly-closed and (almost) parallel-closed critical pair criteria of Huet and Toyama to the logically constrained setting. We discuss the challenges for automation and present crest, a new tool for logically constrained rewriting in which the confluence criteria are implemented, together with experimental data. |
| title | Confluence Criteria for Logically Constrained Rewrite Systems (Full Version) |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2309.12112 |