A weakly monotonic, logically constrained, HORPO-variant
Fuente:
arXiv
Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866911933954785280 |
|---|---|
| author | Kop, Cynthia |
| author_facet | Kop, Cynthia |
| contents | In this short paper, we present a simple variant of the recursive path ordering, specified for Logically Constrained Simply Typed Rewriting Systems (LCSTRSs). This is a method for curried systems, without lambda but with partially applied function symbols, which can deal with logical constraints. As it is designed for use in the dependency pair framework, it is defined as reduction pair, allowing weak monotonicity. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_18493 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | A weakly monotonic, logically constrained, HORPO-variant Kop, Cynthia Logic in Computer Science In this short paper, we present a simple variant of the recursive path ordering, specified for Logically Constrained Simply Typed Rewriting Systems (LCSTRSs). This is a method for curried systems, without lambda but with partially applied function symbols, which can deal with logical constraints. As it is designed for use in the dependency pair framework, it is defined as reduction pair, allowing weak monotonicity. |
| title | A weakly monotonic, logically constrained, HORPO-variant |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2406.18493 |