Omelets Need Onions: E-graphs Modulo Theories via Bottom-up E-matching

Philip Zucker

REVIEW 3 major objections 4 minor 37 references

Omelets Need Onions: E-graphs Modulo Theories via Bottom-up E-matching

T0 review · 3 major / 4 minor · reviewed 2026-08-16 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Bottom-up e-matching with semantic e-ids makes e-graphs modulo theories a practical, nearly free extension of the standard equality-saturation engine.

desk verdict A readable, honest synthesis arguing bottom-up e-matching plus semantic e-ids can make e-graphs modulo theories nearly free—but the key soundness question (what happens when a canonizer changes an e-class's canonical value) is left unaddressed. read the letter →

arxiv 2504.14340 v1 pith:EGZEZEKN submitted 2025-04-19 cs.PL

Philip Zucker This is my paper · ORCID

classification cs.PL

keywords e-graphse-matchingequalitysaturationtermrewritingmodulotheoriessemantice-idsunion-findcanonizercongruenceclosureSMT

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper argues that two ingredients—bottom-up e-matching and semantic e-ids—turn e-graphs modulo theories into a pragmatic technique rather than a research project. Bottom-up e-matching scans the pool of already-known e-classes, grounding pattern variables through ordinary hash-cons lookups, so it needs no ability to enumerate subterms of a term. Semantic e-ids replace plain integer class identifiers with structured values from a theory-specific domain, such as linear combinations, polynomials quotiented by an ideal, multisets, or group orbits. If the recipe works, an existing e-graph engine can gain specialized theories by supplying a small canonizer interface, and equality saturation can reason about arithmetic and algebraic identities with the same generic machinery.

What carries the argument

The two load-bearing mechanisms are bottom-up e-matching and semantic e-ids. Bottom-up e-matching is a query strategy that iterates over e-classes in the term bank to ground pattern variables, replacing each variable by a candidate e-id and constructing the instantiated pattern by a lookup; its complexity is roughly $O(E^v d \log N)$ in e-class count $E$, variables $v$, pattern depth $d$, and nodes $N$, versus top-down's exponential-in-depth cost. Semantic e-ids are structured values—vectors, polynomials, multisets, group elements, primitive constants, or even terms—used directly as e-class identifiers, with a theory-specific canonizer supplying the union-find interface. The e-node tables and congruence closure remain the generic glue that relates different sorts and theories.

What would settle it

Build an e-graph with a linear-arithmetic canonizer in the proposed interface and run a saturation where an asserted equality like $4x+5y=13z+2w$ is followed by a rewrite whose pattern has a variable occurring under a non-canonical subterm; if the e-node table misses a congruence that the unspecialized e-graph would find, or if canonization changes a key during rebuilding and loses a match, the nearly-free claim fails. More directly, exhibit a finite ground theory and a pattern where seeding the term bank with all subterms still leaves bottom-up matching unable to find a substitution that top-down matching finds.

Watch

Extended reading notes

Core claim

The discovery the paper is trying to establish is that the standard e-graph, viewed as a model of a set of ground equalities, can have its uninterpreted value domain replaced by a structured semantic domain without abandoning congruence closure. Each theory contributes a canonizer—a generalized union-find that implements create, eq, fresh, canon, and assert_eq—and the canonizer's output serves as the e-id. Bottom-up e-matching then proceeds in the same direction as term insertion, reusing the e-node tables and canonizers that already exist, and it can find matches even for theories where top-down e-matching would need to enumerate infinitely many or unrepresentable subterms. The paper claims that in this setting bottom-up e-matching is strictly more powerful than top-down e-matching, because seeding the term bank with subterms lets bottom-up matching reproduce every top-down match while remaining meaningful when top-down is not.

Load-bearing premise

The whole approach rests on the assumption that any theory-specific canonizer can be dropped into the generic union-find interface without breaking congruence closure, matching, or extraction—specifically, that canonical structured values remain usable as hash-consed e-node keys.

Editorial extensions

If this is right

An equality-saturation engine can be extended to linear arithmetic by plugging in a Gaussian-elimination canonizer, without changing the rewriting loop.
Polynomial identities such as $\sin(x)^2 + \cos(x)^2 = 1$ become usable as matching facts when e-ids are elements of a polynomial quotient ring modulo a Gröbner basis.
For deep patterns with few variables, bottom-up matching avoids the exponential factor top-down pays per pattern depth.
Theories whose completion does not terminate, such as string rewriting, can still be used by stopping completion early and relying on the e-graph's self-healing behavior.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

If the central claim holds, the practical bottleneck of e-graph rewriting shifts from matching algorithms to the quality of the term bank and the cost of canonization, which the paper's complexity sketch leaves out.
A natural testable extension is to combine several semantic domains at once—say multisets for AC symbols and polynomials for arithmetic—and check whether cross-theory equalities still propagate correctly through the e-node tables.
The semantic-e-id view may also change extraction: if an e-class is a canonical vector or polynomial, extracting a readable term requires a theory-specific inverse translation, which the paper does not address.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

This is a position paper by Philip Zucker arguing that two ingredients—bottom-up e-matching and semantic e-ids—make e-graphs modulo theories (EMT) nearly free. The conceptual case is plausible and the writing is refreshingly clear, but the central mechanism has a real gap the author doesn't confront.

What's good: the paper crystallizes a nice observation. Bottom-up e-matching proceeds in the same direction as term insertion, so it reuses existing lookup and canonization infrastructure, whereas top-down matching requires expanding e-classes to e-nodes, which is awkward or impossible once e-ids are semantic values. The examples of theory-specific union-finds (linear arithmetic, Gröbner bases, multisets, group actions) are useful and the limitations (e.g., non-terminating completion) are acknowledged honestly. For a paper with no implementation, it does a good job of explaining why the approach should be practical.

Where it's soft: the stress-test concern is real and lands. Section 3 presents a generalized union-find API (create, eq, fresh, canon, assert_eq) and says e-ids are structured values, but it never specifies whether e-node tables are keyed by stable handles or by mutable canonical values. If x+y and z are asserted equal, the canonical representative of that class can become a new value that neither x+y nor z had. An e-node stored under the old canonical child (e.g., f(x+y) keyed by vector v1) won't be found by a later lookup with the new canonical child (f(z) keyed by v2)—or it will be duplicated, breaking congruence. The paper's claim that EMT comes "nearly for free" depends exactly on this. No invariant or re-keying procedure is given. This isn't a performance issue; it's a correctness question about the title claim.

Also, the paper leans heavily on the author's own blog posts for load-bearing claims (ground completion as union-find, semantic e-ids). Those are unpublished and not peer-reviewed, which is fine for intuition but not enough for verification. A prototype or a formal treatment of congruence closure over structured e-ids would address both gaps.

Bottom line: it's a good design argument worth engaging with. A serious referee should see it, but the referee should push hard on the re-keying question and request either a prototype or a formal invariant. If that can be fixed, this could become a useful reference for practitioners.

Referee Report

3 major / 4 minor

Summary. This paper proposes a pragmatic recipe for e-graphs modulo theories (EMT) based on two ideas: bottom-up e-matching and semantic e-ids. In bottom-up e-matching, one scans all e-classes or variables, constructs a fully ground pattern by hash-cons lookups, and asserts equality with the right-hand side, rather than expanding patterns top-down from e-class roots. Semantic e-ids replace integer e-class identifiers with theory-specific structured values (vectors, polynomials, multisets, etc.), and the union-find is replaced by a generic canonizer supporting create, eq, fresh, canon, and assert_eq. The paper argues that this combination gives EMT 'nearly for free' because it reuses existing lookups and canonizers, and that bottom-up e-matching is more powerful than top-down in the presence of theories. The manuscript is a short position/tool paper: it contains code sketches and a catalogue of candidate theory-specific union-finds, but no implementation, no benchmarks, and no formal proofs.

Significance. If the central claims are correct, this would be a valuable and inexpensive recipe for users of e-graphs who need built-in theories such as linear arithmetic, polynomials, multisets, or group actions. The paper is explicit about the proposed five-method interface and gives concrete examples, which makes the intended design easy to reproduce. It also states clearly that the asymptotic comparison in Section 2 is rough, which is appropriate. The main contribution, however, is not yet established: the soundness of using semantic e-ids as keys in e-node tables is not proved, and the complexity argument omits match enumeration and canonization costs. The manuscript relies heavily on the author's unpublished blog posts for several load-bearing claims, which limits verifiability. The ideas are plausible and worth pursuing, but the paper does not yet provide enough formal or experimental support for its 'nearly for free' assertion.

major comments (3)

[Section 3 (Generalized Union Finds and Semantic E-ids)] The manuscript uses semantic e-ids both as values and as keys for e-node tables, but it never states an invariant separating stable handles from canonical values. In an ordinary e-graph, e-class ids are stable handles and e-node tables are keyed by those ids, so congruence is preserved after unions. If an e-id is a semantic value, then a new ground equation can change the canonical representative of a class (for example, asserting x+y = z may change the canonical vector for that class to a new vector that neither original term had). In that case, an e-node stored under the old canonical child is no longer found by the Section 2 lookup `lhs = foo[bar[X],Y]`, or it is duplicated. The paper gives no re-keying or rebuilding procedure, and no theorem stating whether the e-node table and congruence closure remain sound and complete. This is load-bearing for the 'nearly for free' claim; the manuscript's own 'self-healing character' comment in Section 3.2 suggests the author is aware of incompleteness but does not formalize what invariant is preserved.
[Section 2 (Bottom Up E-Matching Plays Nicer With Theories)] The asymptotic comparison O(E (N/E)^d) for top-down versus O(E^V d ln N) for bottom-up is marked as rough, but it omits two quantities that are essential to the matching problem: the number of matches produced and the cost of theory-specific canonization during the hash-cons lookup. Bottom-up scans a Cartesian product of variable assignments and is exponential in the number of pattern variables (E^V), while top-down's depth factor d depends on the branching structure of the e-graph; both are also at least linear in the output size. Consequently, the examples of 'bad' patterns do not by themselves establish the claim that 'bottom-up e-matching is more powerful than top-down e-matching' in the presence of theories. A precise problem statement (what counts as one match, whether all matches or only witnesses are required) and a comparison that includes match enumeration and canonizer cost are needed.
[Section 3.2 and references [27]–[36]] Several load-bearing claims are supported mainly by the author's own unpublished blog posts. In particular, the characterization of union-find as ground completion is credited to [32], the multiset canonizer to [36], and the linear/Gröbner canonizers to [34]. The text states that various theories 'are guaranteed to be completable to canonizers,' but it does not give proofs or cite peer-reviewed sources for termination and confluence of the relevant completion procedures. Because the entire EMT scheme presupposes that the canonizer is a well-defined function that respects the asserted equalities, the manuscript should either provide proofs, point to published treatments, or explicitly present these cases as conjectured. As written, a reader cannot verify the central claim from the manuscript alone.

minor comments (4)

[Title] In the arXiv text, the title appears as 'via Bo/t_tom-up E-Matching'; this looks like a typo for 'Bottom-up' and should be corrected.
[Section 4] The phrase 'might reaosnably go' contains a typo; it should be 'might reasonably go'.
[Section 2] The Python snippets use comments and indentation in a way that is hard to parse in the rendered text. Providing a single runnable listing with explicit `continue` statements would make the idiom clearer.
[Section 3] The paper uses 'union find' both for the standard integer parent-pointer data structure and for the generalized theory-specific canonizer; a short table or glossary distinguishing the two would reduce confusion.

Circularity Check

0 steps flagged · score 2.0 of 10

No significant circularity; only minor, non-load-bearing self-citations to the author's blog posts, which illustrate rather than force the central claim.

full rationale

The paper makes no fitted predictions and contains no derivation that reduces to its own inputs. Its central claims are the pragmatic effectiveness of bottom-up e-matching and the use of semantic e-ids as a generalized union-find interface. Those claims are supported by argumentation, code sketches, and references to standard material, not by a fitted parameter or by a theorem whose conclusion is assumed in its premises. The author does cite his own blog posts (e.g., [30], [32], [34], [36]) for key concepts such as bottom-up e-matching, union-find as ground completion, Gauss/Groebner e-graphs, and multiset rewriting. These self-citations are numerous and disclosed, and they are used as pointers to prior exposition rather than as externally verified proof. However, under the review rules self-citation is not circularity unless it is load-bearing and unverified while the argument reduces to it. Here the underlying mathematical content is independently known: ground Knuth-Bendix completion terminates for atomic equations, Gaussian elimination canonizes linear systems, Groebner bases canonize polynomial ideals, and multiset/AC rewriting is a standard topic in term rewriting (see [1], [17]). The paper's 'nearly for free' claim is an engineering assertion about implementation complexity, not a result derived from a self-citation chain. The main weakness, that the paper does not prove congruence closure and hash-consing remain sound when e-ids are structured semantic values, is a correctness risk rather than a circularity. Therefore the circularity score is low, reflecting only the prevalence of minor self-citations.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The paper contributes a conceptual synthesis, so the ledger is mostly standard background from term rewriting and SMT. The main unpaid assumptions are that theory-specific canonizers can be plugged into the generic union-find interface without breaking congruence closure, and that the complexity heuristics in Section 2 are representative.

assumptions (5)

domain assumption Standard e-graphs implement congruence closure over ground terms, and e-classes / e-nodes can be represented with a union-find data structure.
Assumed throughout; the paper builds on the egg paper [25] and standard e-graph literature.
domain assumption Ground atomic equational completion (Knuth-Bendix completion) always terminates and yields a canonical union-find.
Used in Section 3.1 to justify the view that a union-find is a canonizer; cited to the author's own talk [32] rather than an external proof.
domain assumption The e-graph can be modeled as a partial-function minimal model, with e-ids as values and e-node tables as partial functions.
Section 3 uses this model to justify semantic e-ids; it is a standard e-graph semantics but not proven in the paper.
domain assumption All listed theories (linear equations, Grobner bases, ground multisets, group actions, constructors, Boolean clauses, strings) admit canonizers supporting assert_eq and canon with reasonable efficiency.
Section 3.2 lists these as examples; the paper acknowledges some, such as string rewriting, may not terminate.
ad hoc to paper The asymptotic cost of top-down e-matching is O(E (N/E)^d) and of bottom-up is O(E^V d ln(N)).
Stated in Section 2 without derivation; it is a heuristic that ignores the actual number of matches and variable constraints.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Omelets Need Onions: E-graphs Modulo Theories via Bottom-up E-matching." pith.science (2026). https://pith.science/paper/EGZEZEKN

@misc{pith2026250414340,
  author       = {Pith},
  title        = {Pith review of: Omelets Need Onions: E-graphs Modulo Theories via Bottom-up E-matching},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/EGZEZEKN}},
  note         = {Machine review of arXiv:2504.14340}
}

read the original abstract

E-graphs are a data structure for equational reasoning and optimization over ground terms. One of the benefits of e-graph rewriting is that it can declaratively handle useful but difficult to orient identities like associativity and commutativity (AC) in a generic way. However, using these generic mechanisms is more computationally expensive than using bespoke routines on terms containing sets, multi-sets, linear expressions, polynomials, and binders. A natural question arises: How can one combine the generic capabilities of e-graph rewriting with these specialized theories. This paper discusses a pragmatic approach to this e-graphs modulo theories (EMT) question using two key ideas: bottom-up e-matching and semantic e-ids.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

37 extracted references · 27 canonical work pages

[32]

Philip Zucker. 2024. EGraphs as Ground Completion Talk and EGRAPHS 2024 notes. https://www.philipzucker.com/egraph2024_talk_ done/

work page 2024
[36]

Philip Zucker. 2024. Towards an AC Egraph: Groebner, an d Ground Multiset Rewriting. https://www.philipzucker.com/multiset_rw/

work page 2024
[34]

Philip Zucker. 2024. Gauss and Groebner Egraphs: Intri nsic Linear and Polyno- mial Equations. https://www.philipzucker.com/linear_g robner_egraph/

work page 2024
[1]

Franz Baader and Tobias Nipkow. 1998. Term rewriting and all that . Cambridge University Press, USA

work page 1998
[2]

Franz Baader, Wayne Snyder, Paliath Narendran, Manfred Schmidt-Schauss, and Klaus Schulz. 2001. Chapter 8 - Uniﬁcation Theory. In Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.). North-Holland, Amster- dam, 445–533. doi:10.1016/B978-044450813-3/50010-2

doi:10.1016/b978-044450813-3/50010-2 2001
[3]

Sylvain Conchon, Évelyne Contejean, and Mohamed Iguern elala. 2012. Canon- ized Rewriting and Ground AC Completion Modulo Shostak Theo ries : Design and Implementation. Logical Methods in Computer Science 8, 3 (Sept. 2012), 1–29. doi:10.2168/LMCS-8(3:16)2012 Selected Papers of the Conference Tools and Algo- rithms for the Construction and Analysis of Syst...

work page doi:10.2168/lmcs-8(3:16)2012 2012
[4]

Cox, John Little, and Donal O’Shea

David A. Cox, John Little, and Donal O’Shea. 2015. Gröbner Bases . Springer International Publishing, Cham, 49–119. doi:10.1007/978 -3-319-16721-3_2

doi:10.1007/978 2015
[5]

Leonardo de Moura and Nikolaj Bjørner. 2007. Eﬃcient E-M atching for SMT Solvers. In Automated Deduction – CADE-21 , Frank Pfenning (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 183–198

work page 2007

Show all 37 references

[6]

Steven Eker. 2003. Associative-Commutative Rewriting on Large Terms. In Rewriting Techniques and Applications , Robert Nieuwenhuis (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 14–29

2003
[7]

Michael Färber. 2023. Terms for Eﬃcient Proof Checking a nd Parsing. In Pro- ceedings of the 12th ACM SIGPLAN International Conference onCertiﬁed Programs and Proofs (Boston, MA, USA) (CPP 2023). Association for Computing Machinery, New York, NY, USA, 135–147. doi:10.1145/3573...

2023
[8]

Jean-Christophe Filliâtre and Sylvain Conchon. 2006. T ype-safe modular hash- consing. In Proceedings of the 2006 Workshop on ML (Portland, Oregon, USA) (ML ’06) . Association for Computing Machinery, New York, NY, USA, 12 –19. doi:10.1145/1159876.1159880

2006
[9]

Thom Frühwirth. 2009. Union-ﬁnd algorithm . Cambridge University Press, 256–280. Conference’17, July 2017, Washington, DC, USA Philip Zucker

2009
[10]

Harald Ganzinger. 2002. Shostak Light. In Proceedings of the 18th International Conference on Automated Deduction (CADE-18) . Springer-Verlag, Berlin, Heidel- berg, 332–346

2002
[11]

Yeting Ge and Leonardo de Moura. 2009. Complete Instant iation for Quanti- ﬁed Formulas in Satisﬁabiliby Modulo Theories. In Computer Aided Veriﬁcation, Ahmed Bouajjani and Oded Maler (Eds.). Springer Berlin Heidelberg, Berlin, Hei- delberg, 306–320

2009
[12]

Joxan Jaﬀar and Michael J. Maher. 1994. Constraint logi c program- ming: a survey. The Journal of Logic Programming 19-20 (1994), 503–581. doi:10.1016/0743-1066(94)90033-7 Special Issue: Ten Yea rs of Logic Program- ming

1994 doi
[13]

Thomas Koehler, Phil Trinder, and Michel Steuwer. 2022 . Sketch-Guided Equal- ity Saturation: Scaling Equality Saturation to Complex Opt imizations of Func- tional Programs. arXiv:2111.13040 [cs.PL] https://arxiv .org/abs/2111.13040

2022 arXiv
[14]

Cynthia Kop and Naoki Nishida. 2013. Term Rewriting wit h Logical Constraints. In Frontiers of Combining Systems , Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt (Eds.). Springer Berlin Heidelberg, Berl in, Heidelberg, 343– 358

2013
[15]

Laura Kovács and Andrei Voronkov. 2013. First-Order Th eorem Proving and Vampire. In Computer Aided Veriﬁcation , Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1 –35

2013
[16]

Matthieu Lemerre and Dorian Lesbre. 2024. Labeled Unio n-Find for Constraint Factorization. In Proceedings of the 10th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains (NSAD 2024) . Pasadena, United States. HAL Id: cea-04996700

2024
[17]

CLAUDE MARCHÉ. 1996. Normalized Rewriting: an Alterna tive to Rewriting modulo a Set of Equations. Journal of Symbolic Computation 21, 3 (1996), 253–

1996
[18]

Mateusz Paprocki. [n. d.]. Gröbner bases and their appl ications. https://mattpap.github.io/masters-thesis/html/src/groebner.html
[19]

Rudi Schneider, Marcus Rossel, Amir Shaikhha, Andres G oens, Thomas Koehler, and Michel Steuwer. [n. d.]. Slotted E-Graphs. In To Appear at PLDI 2025

2025
[20]

Stephan Schulz, Simon Cruanes, and Petar Vukmirović. 2 019. Faster, Higher, Stronger: E 2.3. In Proc. of the 27th CADE, Natal, Brasil (LNAI, 11716) , Pascal Fontaine (Ed.). Springer, 495–507
[21]

Eytan Singher and Shachar Itzhaky. 2023. Colored E-Gra ph: Equality Reasoning with Conditions. arXiv:2305.19203 [cs.PL]

2023 arXiv
[22]

Sturmfels

B. Sturmfels. 1996. Grobner Bases and Convex Polytopes. American Mathematical Society. https://books.google.com/books?id=K-bxBwAAQ BAJ

1996
[23]

Remy Wang. 2025. Completeness of Equational Proofs wit h Equality Saturation. https://remy.wang/blog/birkhoﬀ.html

2025
[24]

Yisu Remy Wang, Max Willsey, and Dan Suciu. 2023. Free Jo in: Unify- ing Worst-Case Optimal and Traditional Joins. arXiv:2301. 10841 [cs.DB] https://arxiv.org/abs/2301.10841

2023 arXiv
[25]

Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tat- lock, and Pavel Panchekha. 2021. egg: Fast and extensible eq uality satura- tion. Proc. ACM Program. Lang. 5, POPL, Article 23 (jan 2021), 29 pages. doi:10.1145/3434304

2021 doi
[26]

Yihong Zhang, Yisu Remy Wang, Max Willsey, and Zachary T atlock. 2022. Re- lational E-Matching. arXiv:2108.02290 [cs.DB] https://a rxiv.org/abs/2108.02290

2022 arXiv
[27]

Philip Zucker. 2022. Groupoid Annotated Union Finds. https://www.philipzucker.com/union-ﬁnd-groupoid/

2022
[28]

Philip Zucker. 2023. Relational AC Matching. https://www.philipzucker.com/relational-ac-matching/

2023
[29]

Philip Zucker. 2024. Acyclic Egraphs and Smart Constru ctors. https://www.philipzucker.com/smart_constructor_aegraph/

2024
[30]

Philip Zucker. 2024. Bottom Up Egraph Ematching Plays N icer with Theories (AC, etc). https://www.philipzucker.com/bottom_up/

2024
[31]

Philip Zucker. 2024. Co-Egraphs: Streams, Uniﬁcation , PEGs, Rational Lambdas. https://www.philipzucker.com/coegraph/

2024
[33]

Philip Zucker. 2024. An External Z3 Egraph for Egraphs M odulo Theories. https://www.philipzucker.com/ext_z3_egraph/

2024
[35]

Philip Zucker. 2024. Hashing Modulo Theories. https://www.philipzucker.com/hashing-modulo/

2024
[288]

doi:10.1006/jsco.1996.0011

1996

Pith tools

Reviewed August 16, 2026 · model on record in the stance chip above.

[1] [32]

Philip Zucker. 2024. EGraphs as Ground Completion Talk and EGRAPHS 2024 notes. https://www.philipzucker.com/egraph2024_talk_ done/

work page 2024

[2] [36]

Philip Zucker. 2024. Towards an AC Egraph: Groebner, an d Ground Multiset Rewriting. https://www.philipzucker.com/multiset_rw/

work page 2024

[3] [34]

Philip Zucker. 2024. Gauss and Groebner Egraphs: Intri nsic Linear and Polyno- mial Equations. https://www.philipzucker.com/linear_g robner_egraph/

work page 2024

[4] [1]

Franz Baader and Tobias Nipkow. 1998. Term rewriting and all that . Cambridge University Press, USA

work page 1998

[5] [2]

Franz Baader, Wayne Snyder, Paliath Narendran, Manfred Schmidt-Schauss, and Klaus Schulz. 2001. Chapter 8 - Uniﬁcation Theory. In Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.). North-Holland, Amster- dam, 445–533. doi:10.1016/B978-044450813-3/50010-2

doi:10.1016/b978-044450813-3/50010-2 2001

[6] [3]

Sylvain Conchon, Évelyne Contejean, and Mohamed Iguern elala. 2012. Canon- ized Rewriting and Ground AC Completion Modulo Shostak Theo ries : Design and Implementation. Logical Methods in Computer Science 8, 3 (Sept. 2012), 1–29. doi:10.2168/LMCS-8(3:16)2012 Selected Papers of the Conference Tools and Algo- rithms for the Construction and Analysis of Syst...

work page doi:10.2168/lmcs-8(3:16)2012 2012

[7] [4]

Cox, John Little, and Donal O’Shea

David A. Cox, John Little, and Donal O’Shea. 2015. Gröbner Bases . Springer International Publishing, Cham, 49–119. doi:10.1007/978 -3-319-16721-3_2

doi:10.1007/978 2015

[8] [5]

Leonardo de Moura and Nikolaj Bjørner. 2007. Eﬃcient E-M atching for SMT Solvers. In Automated Deduction – CADE-21 , Frank Pfenning (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 183–198

work page 2007