Alexander writes: > I had a look at Anthony's filtered list (218 entries), and I removed the theorems with the following name patterns (because they are definitive in mathboxes): wl-*, bj-*, rp-*, bnj*, *RP, frege* , axfrege* . Then 103 entries remain. In general, theorems of mathboxes should not be considered.
Yes, I'm afraid the deficiencies in my list aren't likely to be remedied at least until I settle on an mm parser to adopt. Also the rationale I gave for this tool wasn't as a duplicate checker, pleasing though it is that some utility is being found in this regard. However, for what it's worth, I ran alt-mm again last night, the differences in output since the first time I ran it can be found here https://github.com/Antony74/alt-mm/commit/fabcf71e272b131574a3dc95c4d247e22bf1176b Best regards, Antony On Sun, Dec 4, 2022 at 5:11 PM Glauco <[email protected]> wrote: > Thanks, Alexander > > now I'm working on tooling, but as soon as I get back to set.mm with new > proofs, I will certainly look into this list. > > BR > Glauco > > Il giorno domenica 4 dicembre 2022 alle 11:34:26 UTC+1 Alexander van der > Vekens ha scritto: > >> I had a look at Anthony's filtered list (218 entries), and I removed the >> theorems with the following name patterns (because they are definitive in >> mathboxes): wl-*, bj-*, rp-*, bnj*, *RP, frege* , axfrege* . Then 103 >> entries remain. In general, theorems of mathboxes should not be considered. >> >> There are, however, duplicates in the mathboxes (mainly from GS): >> * fdmfifsupp, fidmfisupp (fidmfisupp in GS's mathbox, can be removed) >> * le2addd, leadd12dd (leadd12dd in GS's mathbox, can be removed) >> * fz0ssnn0, fzssnn0 (fzssnn0 in GS's mathbox, can be removed) >> * tendopl2, tendospdi2 (both in NM's mathbox, tendospdi2 could be removed) >> * mapss2, mapssbi (both in GS's mathbox, mapss2 could be removed) >> * fnfvimad, fnfvima2 (both in GS's mathbox, fnfvima2 could be removed) >> * climd, clim2d (both in GS's mathbox, clim2d could be removed) >> * volicorecl, volicore (both in GS's mathbox, volicore could be removed) >> >> Attached my reduced list, containing some comments (including the above >> listed comments). >> >> @Glauco: Maybe you can have a look at this list and find additional >> duplicates. Could you remove these, please? >> >> On Tuesday, August 30, 2022 at 3:55:23 PM UTC+2 [email protected] wrote: >> >>> 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/c6751e4e-98de-4d88-a479-8494716c16a6n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/c6751e4e-98de-4d88-a479-8494716c16a6n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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%2BA3ZN3z4Vpo88DSG4iykkY9Ba_wKmwaxUdQpfar43SWgw%40mail.gmail.com.
