> That's the piece of MMJ I'd be after first if it was me. OK. Thanks for this clue! :)
> (you can un-unify a regular proof by removing all the tokens who's > expressions don't start with |- ??? un-unify?? > but I don't know how you put them back in. > It's important because having to specify all the symbols used in a proof > would be really pedantic). ? in a metamath verifier unification is trivial because: ( Mandatory hypotheses must be pushed on the proof stack in the order in which they appear. In addition, each variable must have its type specified with a $f hypothesis before it is used and that each $f hypothesis have the restricted syntax of a typecode (a constant) followed by a variable. The typecode in the $f hypothesis must match the first symbol of the corresponding RPN stack entry (which will also be a constant), so the only possible match for the variable in the $f hypothesis is the sequence of symbols in the stack entry after the initial constant. ) to discover new proofs is non-trivial because ... ... Godel... etc. P != NP ......? The general algorithm for unification described in the literature is somewhat complex. In the Proof Assistant, a more general unification algorithm is used. DOES MMJ use the same algo? HOW does MMJ do it? What is the best (description of the) algorithm? ? GtMM currently has some tricks/features. eg, you can work forwards and backwards. forwards = starting with the essential hypoths and moving from left right . backwards = starting with the chain we want to make and moving right to left. suppose we guess at the last machine we'll use, then GtMM can show us what chain(s) that machine would need for its inputs chains are strings of blobs. blobs are metamath variables. triangular blobs are variables that can be 'mapped' to other chains. square blobs cannot be mapped. unification = doing the mapping? / finding it |- = provable / starting chain / essential hypoths GtMM just ignores floating hypoths???? chain we need to make to complete the level always shown top-center in Gtmm essential hypoths = chains given to start with, they are used as input for the machines. shown in top left of gtmm. machines you can use (= things we've already proved) are shown on the right of the screen. click on a machine to add it to the workspace pane. workspace pane is always in the center of gtmm screen. 4.3.1 The Concept of Unification During the course of verifying a proof, when Metamath encounters an assertion label, it associates the mandatory hypotheses of the assertion with the top entries of the RPN stack. Metamath then determines what substitutions it must make to the variables in the assertion’s mandatory hypotheses in order for these hypotheses to become identical to their corresponding stack entries. This process is called unification. (We also informally use the term “unification” to refer to a set of substitutions that results from the process, as in “two unifications are possible.”) After the substitutions are made, the hypotheses are said to be unified. If no such substitutions are possible, Metamath will consider the proof incorrect and notify you with an error message. While a proof is being developed, sometimes not enough information is available to determine a unique unification. In this case Metamath will ask you to pick the correct one. How is MetamathZero different? -- 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 on the web visit https://groups.google.com/d/msgid/metamath/CANS9R92BwuD3h%2BNEmNB2uGNa7g%3Dk5HJkf5L4r9L3f3j4GRFgFQ%40mail.gmail.com.
