Release of pmGenerator 1.2: User-definable systems, and proof minimization challenges
100 views
Skip to first unread message
samiro.d...@rwth-aachen.de
Mar 4, 2024, 5:59:57 AMMar 4
to Metamath
I have just released pmGenerator 1.2, 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 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 (abstract proof summary: s5.txt)
For illustration, I created an abstract proof summary of the whole pmproofs.txt database of Metamath's mmsolitaire project, and documented on how this can be done: pmproofs-summary.txt (online version)
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.
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 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 (abstract proof summary: s5.txt)
For illustration, I created an abstract proof summary of the whole pmproofs.txt database of Metamath's mmsolitaire project, and documented on how this can be done: pmproofs-summary.txt (online version)
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.
As usual, if you find any bugs, please report them to my issue tracker. (Not a single bug has been reported so far!)
I would be happy to receive some feedback.
— Samiro Discher
Reply all
Reply to author
Forward
0 new messages