search

JuliaSymbolics / Metatheory.jl

Makes Julia reason with equations. General purpose metaprogramming, symbolic computation and algebraic equational reasoning library for the Julia programming language: E-Graphs & equality saturation, term rewriting and more.
https://juliasymbolics.github.io/Metatheory.jl/dev/
MIT License
350 stars 44 forks source link

Proof production algorithm #111

Open vitrun opened 2 years ago

vitrun commented 2 years ago

Is it possible to extract the steps needed to produce the final answer? for example. (a*2)/2 -step1-> a*(2/2) -step2-> a

rule of step1: (x*y)/z --> x*(y/z) rule of step2: x/x --> 1

0x0f0f0f commented 2 years ago

Not yet. We're planning to do so Egg rust library has it https://docs.rs/egg/0.7.1/egg/tutorials/_03_explanations/index.html

0x0f0f0f commented 2 years ago

See this for later implementation https://www.cs.upc.edu/~roberto/papers/rta05.pdf cc @Wilkenfeld

adrianleh commented 3 weeks ago

Linking #223 #226 here