Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2405.17109 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910921125789696 |
|---|---|
| author | Niederhauser, Johannes Hirokawa, Nao Middeldorp, Aart |
| author_facet | Niederhauser, Johannes Hirokawa, Nao Middeldorp, Aart |
| contents | We revisit completion modulo equational theories for left-linear term rewrite systems where unification modulo the theory is avoided and the normal rewrite relation can be used in order to decide validity questions. To that end, we give a new correctness proof for finite runs and establish a simulation result between the two inference systems known from the literature. Given a concrete reduction order, novel canonicity results show that the resulting complete systems are unique up to the representation of their rules' right-hand sides. Furthermore, we show how left-linear AC completion can be simulated by general AC completion. In particular, this result allows us to switch from the former to the latter at any point during a completion process. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_17109 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Left-Linear Completion with AC Axioms Niederhauser, Johannes Hirokawa, Nao Middeldorp, Aart Logic in Computer Science We revisit completion modulo equational theories for left-linear term rewrite systems where unification modulo the theory is avoided and the normal rewrite relation can be used in order to decide validity questions. To that end, we give a new correctness proof for finite runs and establish a simulation result between the two inference systems known from the literature. Given a concrete reduction order, novel canonicity results show that the resulting complete systems are unique up to the representation of their rules' right-hand sides. Furthermore, we show how left-linear AC completion can be simulated by general AC completion. In particular, this result allows us to switch from the former to the latter at any point during a completion process. |
| title | Left-Linear Completion with AC Axioms |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2405.17109 |