theorem importation

[majidaldo]

would it be possible to slurp in some library of theorems to use? for example, https://github.com/bzhan/holpy/tree/main/library , or from Lean.

[brandonwillard]

There are a few "encoding" questions to answer in order to do that, but it's absolutely the kind of thing to which I would like to apply miniKanren.

[majidaldo]

MathML?

[brandonwillard]

If we could form miniKanren relations from MathML, that would be pretty cool.

[majidaldo]

i've been thinking about this a lot: what would the minikanren form look like? does it have to be ast-like, or can it be triples like MathML-content ? (they're probably equivalent).

from there, how would you implement sequent calculus?

i mean figuring out these two would basically be the 'killer app' for minikanren in python land.

[brandonwillard]

i've been thinking about this a lot: what would the minikanren form look like? does it have to be ast-like, or can it be triples like MathML-content ? (they're probably equivalent).

Depends on the type of information, but, for something like Gradshteyn and Ryzhik identities, etuples would probably suffice.

We really need to implement more relations that can make use of MathML-encoded information.

from there, how would you implement sequent calculus?

The relational typing example in #34 implements some of the elements needed in an implementation of the Sequent Calculus. I would need to look through the miniKanren literature to find all the necessary parts, though, but I'm sure most of them are there. This would be a good thing to ask the miniKanren community at large (e.g. here).

i mean figuring out these two would basically be the 'killer app' for minikanren in python land.

Yeah, fully implementing the Sequent Calculus would be pretty great.
Efficient and flexible relational search is also a necessary next step in this work, and likely a big component of a usable implementation of the aforementioned. Something like #64 seems promising.