WG211/M26Kammar

From WG 2.11
Revision as of 07:58, 13 October 2026 by Ohad (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

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.