Metatheory.jl should be able to, analogously to the chase, perform equality saturation. It also has its own version of optimal term extraction. Automating the the process of encoding Catlab theories as Metatheory rewrite systems would allow us to compare our own functionality.
Metatheory.jl should be able to, analogously to the chase, perform equality saturation. It also has its own version of optimal term extraction. Automating the the process of encoding Catlab theories as Metatheory rewrite systems would allow us to compare our own functionality.