Sorry, I missed one question which could be easily answered: *> I don't see how to create hypothesis statements in the tool*
This is implemented. Each statement is prefixed with an upper case letter either P (provable) or H (hypothesis). Alt-left-click allows to change it. This is demonstrated at 5:49 in this video - https://drive.google.com/file/d/1JCDffUXkb_J-TiA07aNwK9SBKyaukaA3/view - Igor On Sunday, February 12, 2023 at 1:12:24 AM UTC+1 Glauco wrote: > On 2/11/23 07:39, David A. Wheeler wrote: > > > 1) I think one of the "key" missing things is ability to help a user > > to understand why a statement doesn't unify. > > I have only an approximate idea of whether this is easy or hard, but I > will say that even modest improvements here would be helpful. For > example, it may be easier to detect particular cases than every possible > "way" a statement can't unify. One of the more time consuming things > that happens to me when using mmj2 is that a unification which I > expected to happen doesn't, and then I need to look at (sometimes long) > expressions to figure out what parts don't match. > > Hi Igor, > > below I tell what I've come up with, in yamma. > > First, I'll write the short story, then I'll elaborate a bit about the > theory and the challenges. > > The short story: > > yamma has two kinds of diagnostic messages for unification failure. > > > The first kind of message, suggests how to fix the unification error. Two > examples: > > "Unification error: referenced statement is '|- ph' but it was expected to > be '|- ( ps -> ph )'" > > (see > https://github.com/glacode/yamma/blob/b4864171f99f5461255e7ad8bfd2a546a9c4def3/server/src/__test__/MmpParser.test.ts#L329 > > for the full unit test) > > or > > "Unification error: statement is '|- ch' but it was expected to be '|- ( > &W1 <-> &W2 )'" > > (see > https://github.com/glacode/yamma/blob/b4864171f99f5461255e7ad8bfd2a546a9c4def3/server/src/__test__/MmpParser.test.ts#L498 > > for the full unit test) > > The first example is a diagnostic highlighted on the hyp label, > referencing a formula that doesn't match what's expected. > The second example is a diagnostic on the statement itself (the 'main' > formula cannot be unified with what's expected by the step label) > > > The second kind of messages, involves substitution of working vars. > Example: > > 'Working Var unification error: the working var &W2 should be replaced > with the following subformula, containing itself ( &W2 -> ph )' > > (see > https://github.com/glacode/yamma/blob/b4864171f99f5461255e7ad8bfd2a546a9c4def3/server/src/__test__/MmpParser.test.ts#L420 > > for the full unit test) > > > > Now, a bit of 'theory' (as far as I understand it) > > There are two categories of unification: > > 1. single statement > > 2. multiple statements > > With single statement unification, you're trying to find the mgu for both > the logical variables (the theory's variables) and the (possible) working > variables. You could use a Martelli Montanari algorithm on the whole proof, > and it will be clean and "secure", but you'll not get a super-informative > error message. > That's why, for the single statement unification, I've gone for a 'custom' > approach, that allows for some better error message. > > With multiple statement unification, you're trying to find the mgu for all > the working vars in the proof (because logical variables have already been > 'substituted'). > Here, I've gone with the 'pure' Martelli Montanari algorithm. > It can fail either > - with a 'clash fail' error (for metamath, it means two constants don't > match; something like '->' was expected, but you have '<->' ) > or > - with an 'occur check fail' (a working var should be replaced with a > formula strictly containing itself) > > Hope this can give you some ideas. > > -- 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/f20ff644-3907-4906-8a93-3eee2f6ba60dn%40googlegroups.com.
