Home

Welcome to the GtMetamath wiki! Perhaps we could look briefly at what implementations currently exist?

metamath-exe: https://github.com/metamath/metamath-exe/blob/master/src/mmunif.c

mmj2: (see also /doc/StepUnifier.html) https://github.com/digama0/mmj2/blob/master/src/mmj/pa/ProofUnifier.java

metamath-knife: I don't think this has a proof assistant yet, and formula.rs (comes up in searches but) is part of the verifier?

mm0-rs: https://github.com/digama0/mm0/blob/master/mm0-rs/src/elab/refine.rs#L692-L772

It's MM0 not metamath, but it basically represents what I would do for a metamath unification algorithm, with the slight extension that it supports unfolding definitions as well. You can just ignore the cases that call self.unfold (and the returned conversion proof) for mmj2-style unification.