Enhancement proposal: use Metatheory.jl

[0x0f0f0f]

Me and @philzook58 worked on an EGraph implementation in pure Julia: https://github.com/0x0f0f0f/Metatheory.jl
It may be really interesting to write a backend for Julog using Metatheory.EGraphs and Metatheory.EGraphs.AbstractAnalysis to see if it simplifies the Julog codebase and outperforms the original implementation.
You may want to take a read at this paper https://dl.acm.org/doi/pdf/10.1145/3434304
Using Julog the other way, as an analysis for Metatheory.jl (applying rewrite rules only when a goal can be solved) would prove fundamental and useful for a symbolic mathematics/theorem proving framework in pure Julia.
Thanks for your package btw!

[0x0f0f0f]

Check this out! From "Mathematically Informed Linear Algebra Codes Through
Term Rewriting" http://people.cs.uchicago.edu/~mrocklin/storage/dissertation.pdf

Later work in this dissertation will require inference over mathematical terms. We discuss this
element of SymPy now in preparation. We often want to test whether algebraic statements
are true or not in a general case. For example,
Given that x is a natural number and that y is real, is x + y positive?
To create a system capable of posing and answering these questions we need the following
components:

1. A set of predicates: positive and real
2. A syntax to pose facts and queries: Given that x is positive, is x + 1 positive?
3. A set of relations between pairs of predicates: x is a natural number implies that x is positive.
4. A set of relations between predicates and operators: The addition of positive numbers is positive or the square of a real number is positive
5. A solver for satisfiability given the above relations

[AIxer]

sounds great and expect!

[AIxer]

It may be really interesting to write a backend for Julog using Metatheory.EGraphs and Metatheory.EGraphs.AbstractAnalysis to see if it simplifies the Julog codebase and outperforms the original implementation.

any suggestions of HowTo?
In fact, I want to use Metatheory.jl to functional replace prolog 😄 , and there are many rules written in prolog, could I directly rewrite them in Metatheory.jl way and achieve the same result with good performance?

[0x0f0f0f]

@philzook58 made a cool equality-aware prolog. we may start from there
https://www.philipzucker.com/egglog-checkpoint/
https://www.philipzucker.com/egglog2-monic/

[chalst]

I don't have an intuition as to how to get decent performance from an LP language using e-graphs, but it occurs to me that a decent implementation of this is likely to put us in a very good place to implement constraints.