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
355 stars 46 forks source link

Compare with twee #200

Open 0x0f0f0f opened 4 months ago

0x0f0f0f commented 4 months ago

https://github.com/nick8325/twee https://nick8325.github.io/twee/ https://www.tptp.org/ (problem sets).

twee is based on knuth bendix. in our knuth bendix test EqSat already outperformed knuth bendix.

After we have #111 we should compare MT and Twee