Sorted Rewriting, Conditional Rewriting, and Logically Constrained Rewriting (Q7361328)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Sorted_Rewriting
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Sorted Rewriting, Conditional Rewriting, and Logically Constrained Rewriting |
AFP entry Sorted_Rewriting |
Statements
11 March 2026
0 references
Akihisa Yamada
0 references
Sorted Rewriting, Conditional Rewriting, and Logically Constrained Rewriting (English)
0 references
This entry provides various materials for sorted term rewrite systems (sorted TRSs), (sorted) conditional TRSs (CTRSs), and logically constrained TRSs (LCTRSs). For (C)TRSs we formalize the fundamental result that the rewrite steps induced by a (C)TRS is the least rewrite relation that models the (C)TRS. For LCTRSs we simply formulate logics as sorted algebras with the bool sort and logical symbols which are interpreted as expected. This allows us to define rewrite steps of LCTRSs as rewrite steps of an (infinite) TRS.
0 references
