Hello everyone, I'm currently in the process of creating a mmj2 style proof assistant and I had another question. So far my unifier is able to:
1. Fill in step refs if the assertion and hypotheses are given 2. Unify the assertion and hypotheses if the step ref is given Now I noticed that yammas unifier is able to do the following: When given the following mmp file: h1::test.2 |- ( ps -> ch ) h2::test.1 |- ps qed:: |- ch The unifier is able to do the following: h1::test.1 |- ( ps -> ch ) h2::test.2 |- ps qed:2,1:ax-mp |- ch As you can see, despite the fact that the qed step previously had no hypotheses or step ref, the unifier was able to fill in both at the same time. Now my question is: How is this possible in a short period of time? Wouldn't the proof assistant have to look at every theorem in the database, and then try a whole lot of possible combinations of previous lines and hypotheses? That sounds like it would take forever. There are obviously some optimizations to be done (like when one hypothesis does not match a line, don't try it again), but even then my intuition tells me that it would still take practically forever, since multiple hypotheses could match multiple lines and each combination would have to be tried. Is there a smarter, faster way (than what is essentially a smart brute force) of achieving this that I am overlooking? Best regards, Marlo Bruder -- 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/ddc0991a-7f2d-4f50-92f4-e504e4f038c9n%40googlegroups.com.
