Today I released version 1.2.1 <https://github.com/xamidi/pmGenerator/releases/tag/1.2.1>, which comes with several improvements and some new features to assist with proof minimization. Their utilization led to significant improvements <https://github.com/xamidi/pmGenerator/discussions/2#hall-of-fame> in pmGenerator's and Metamath's corresponding challenges [results <https://github.com/xamidi/pmGenerator/discussions/2#challenge-proofs>; pm.txt <https://gist.github.com/xamidi/288ce12d61d317483602f6ad6215038a>] , and has great potential <https://github.com/xamidi/pmGenerator/discussions/3#1-current-algorithm> for tackling these kinds of problems in general.
[email protected] schrieb am Montag, 4. März 2024 um 11:59:57 UTC+1: > I have just released pmGenerator 1.2 > <https://github.com/xamidi/pmGenerator/releases/tag/1.2.0>, which is > capable of building and iterating condensed detachment proofs for > user-definable sets of axioms. The only rules of inference currently > supported, however, are *modus ponens* and *necessitation*. The latter > allows to explore proof systems in modal logic, such as S5. > Consequently, the tool can now assist in research exploring any Hilbert > systems with modus ponens and/or necessitation, not limited to classical > logic. > > Metamath's propositional axioms > <https://us.metamath.org/mpeuni/mmset.html#scaxioms> are still the > default. > Different systems (e.g. Łukasiewicz' first system: > {L1:(p→q)→((q→r)→(p→r)), L2:(¬p→p)→p, L3:p→(¬p→q)}) can now be addressed as > simple as > $ ./pmGenerator -c -n -s CCpqCCqrCpr,CCNppp,CpCNpq [do whatever with L1-L3 > as axioms] > using formulas in Polish notation (here: "normal" Polish notation via '-n > '). > Necessitation can be enabled by '-N <consequtive limit>', e.g. > $ ./pmGenerator -c -n -N -1 -s > CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp > addresses a full axiomatization of S5 in terms of {¬,→,□}, which extends > on our default axioms. > > > But what I mostly worked on are quality of life features to find, display > and handle these proofs, for example to convert them into formula-based or > abstract summary representations, and to actually find meaningful proofs, > such as these: s5proofs.txt > <https://xamidi.github.io/pmGenerator/data/s5proofs.txt> (abstract proof > summary: s5.txt <https://xamidi.github.io/pmGenerator/data/s5.txt>) > > For illustration, I created an abstract proof summary of the whole > pmproofs.txt <https://us.metamath.org/mmsolitaire/pmproofs.txt> database > of Metamath's mmsolitaire <https://us.metamath.org/mmsolitaire/mms.html> > project, and documented on how this can be done: pmproofs-summary.txt (online > version <https://pastebin.com/NjTx1E7c>) > Comments excluded it is only 12059 bytes in size, and with pmGenerator's > new features it could probably be used as a resource to further tackle > Metamath's "shortest known proofs" challenge. > > I left that challenge behind for almost a year now. Instead I created a > new proof minimization challenge that concerns minimal single axioms and > includes even some proofs that are yet to be found! > You may have a look <https://github.com/xamidi/pmGenerator/discussions/2>. > > > As usual, if you find any bugs, please report them to my issue tracker > <https://github.com/xamidi/pmGenerator/issues>. (Not a single bug has > been reported so far!) > I would be happy to receive some feedback. > > — Samiro Discher > > -- 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/ead173a6-f028-4416-b03e-2ab8edcda024n%40googlegroups.com.
