Nooo, I meant to say "The algorithm is now implemented". What an unfortunate typo. I shouldn't be sending emails this early.
On Wednesday, October 1, 2025 at 6:53:59 AM UTC+2 Marlo Bruder wrote: > Thanks for confirming that it is just a smart brute force, erveryone! > > The algorithm is not implemented. > > Best regards, > Marlo Bruder > On Tuesday, September 30, 2025 at 10:26:38 PM UTC+2 [email protected] > wrote: > >> > My understanding is that it really is just a smart brute force: the >> worst-case time complexity is something like O((# of theorems) × (# of >> preceding steps) ^ (# of hypotheses per theorem)). That's why 4syl is >> discouraged, since both its hypotheses and conclusion are very broad and >> can potentially match many different steps. In my experience with >> metamath-lamp's unifier, it tends to time out on theorems like syl333anc >> with loads of hypotheses, since there are simply too many possibilities for >> matching. >> >> Yes, that’s correct, in metamath-lamp it is just a smart brute force. I >> need to check, but I feel like the inability to unify syl333anc and similar >> assertions in some cases is not the browser limitation, it is rather not >> enough optimized implementation. >> >> Maybe this will be useful: >> >> 1. In this comment >> >> <https://github.com/expln/metamath-lamp/issues/77#issuecomment-1577804381> >> Mario summarized his implementation of the unification algorithm in MM1. >> 2. This comment >> >> <https://github.com/expln/metamath-lamp/issues/77#issuecomment-1608487072> >> contains a few interesting examples of unification. >> >> >> - >> Igor >> >> -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/fc763f03-6a8f-47a7-af44-dc037b43b599n%40googlegroups.com.
