WG211/M26Kammar: Difference between revisions
From WG 2.11
Jump to navigationJump to search
Created page with "'''Modular construction of sound-and-complete simplifiers for varieties of semi-rings''' ''Ohad Kammar'', joint work with ''Amaury Mazoyer''" |
No edit summary |
||
| Line 2: | Line 2: | ||
''Ohad Kammar'', joint work with ''Amaury Mazoyer'' | ''Ohad Kammar'', joint work with ''Amaury Mazoyer'' | ||
We characterise the free models of a distributive combination of | |||
finitary algebraic theories in terms of free models for each combined | |||
theory, under suitable assumptions proposed by [https://doi.org/10.4230/LIPIcs.LICS.2026.45 Fuji etal. (2026)]. This characterisation leads to dozens of | |||
sound-and-complete algebraic simplifiers performant enough for | |||
rote-proof synthesis. | |||
Latest revision as of 07:58, 13 October 2026
Modular construction of sound-and-complete simplifiers for varieties of semi-rings
Ohad Kammar, joint work with Amaury Mazoyer
We characterise the free models of a distributive combination of finitary algebraic theories in terms of free models for each combined theory, under suitable assumptions proposed by Fuji etal. (2026). This characterisation leads to dozens of sound-and-complete algebraic simplifiers performant enough for rote-proof synthesis.
