On Tue, Aug 30, 2022 at 12:10 AM Benoit <[email protected]> wrote: > That's a nice work.
Thanks :-) > As for the big list, it would be interesting to have it. Please find the original unfiltered alt-mm output here https://github.com/Antony74/alt-mm/blob/1cef09bc1976bd673d10ae76bdc872ff476b2fa1/set-mm-output.txt And with the label filtering suggested by David here https://github.com/Antony74/alt-mm/blob/master/set-mm-output.txt I don't know why I didn't think of committing the output to the git repository before. If I make further improvements I should be able to keep that output file in sync. Note: you wrote on the first line of your first post "proofs that are > identical", but the proofs can differ: what you mean is that the statements > are identical (more precisely, as you wrote later: the $f, $d, $e and $p > statements of the associated frame). > I think it's the bit where I said axioms, definitions, and proofs were assertions, that I went wrong. A proof does contain an assertion but it contains more than just that. We're only concerned here with the assertion part. The concept of an assertion is just something I've picked up from the checkmm source code, sorry if it's not proper terminology. > And probably not up to variable renaming ? No. Savask has got further with this question than me by considering which sets of variables can be used interchangeably. Sounds like a challenging problem to resolve programmatically (though easily guessed when looking at an .mm file). After solving that I would probably just re-assign variables alphabetically in order of appearance - imposing a consistent ordering makes a test for equality trivial - except I think that falls apart here because the hypotheses in which variables may appear are themselves unordered. Best regards, Antony -- 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/CAJ48g%2BBiMwbMA_GUD8LZPoq5%3Dvy%2Ba9kLQ0qObNSop8J%2BhiQxvw%40mail.gmail.com.
