Email Gateway (Mar 22 2026 at 19:39): Email Gateway (Mar 22 2026 at 19:39):From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
I’m happy to announce a new AFP entry:
Sorted Rewriting
by Akihisa Yamada
Abstract:
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.
https://www.isa-afp.org/entries/Sorted_Rewriting.html
Enjoy,
René
Last updated: Apr 12 2026 at 02:50 UTC