> 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/dfc08701-76de-424e-900e-f3b663b556a3n%40googlegroups.com.
