0x0f0f0f
commented
3 years ago 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:
- A set of predicates: positive and real
- A syntax to pose facts and queries: Given that x is positive, is x + 1 positive?
- A set of relations between pairs of predicates: x is a natural number implies that x is positive.
- A set of relations between predicates and operators: The addition of positive numbers is positive or the square of a real number is positive
- A solver for satisfiability given the above relations
AIxer
chalst
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.EGraphsandMetatheory.EGraphs.AbstractAnalysisto 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 forMetatheory.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!