Mon 15 Jun 2026 11:55 - 12:20 at Meadows CD - Session 2
We develop the notion of E-graphs modulo theories to handle well-known cases of combinatorial explosion when running equality saturation for theories including associative and commutative (AC) operators. We connect this to the well-studied word problem, which can be solved for AC with Buchberger’s algorithm; this gives a foundation for integrating fast theory-specific methods into E-graphs.
Mon 15 JunDisplayed time zone: Mountain Time (US & Canada) change
Mon 15 Jun
Displayed time zone: Mountain Time (US & Canada) change
10:40 - 12:20 | |||
10:40 25mTalk | A Semi-Persistent E-Graph with Native AC Canonization and Leapfrog AC Matching. EGRAPHS Remi Delmas Amazon Web Services Pre-print | ||
11:05 25mTalk | Associativity and Commutativity in Equality Saturation EGRAPHS Tarik Rosin Saarland University, Marcel Ullrich Saarland University, Saarland Informatics Campus, Sebastian Hack Saarland University, Saarland Informatics Campus Pre-print | ||
11:30 25mTalk | Augmenting Rewrite Rule Sets via Knuth-Bendix Completion EGRAPHS Michael Schifferer Saarland University, Marcel Ullrich Saarland University, Saarland Informatics Campus, Sebastian Hack Saarland University, Saarland Informatics Campus Pre-print | ||
11:55 25mTalk | E-graphs modulo theoriesRemote EGRAPHS Sofia Brookie Chalmers University of Technology | ||