The mmsolitaire project (https://us.metamath.org/mmsolitaire/mms.html)
might be relevant to you. (In case you are looking for a minimal proof
database and didn't find this yet:
https://us.metamath.org/mmsolitaire/pmproofs.txt)
There is a version linked that supports manual input on higher axioms and
definitions (https://catsarefluffy.github.io/mmsjs/unify.html). The axioms
used there might not be up to date.
For automated Polish notation parsing, I am only aware of
https://github.com/metamath/metamath-exe and
https://github.com/xamidi/pmGenerator.
Both only support the propositional axioms ax-1, ..., ax-3 (thus far — I
wrote the latter tool and might implement custom axioms in the future).
But I am not aware of any publicly available converter from (all
unconditional) proofs of set.mm to PN or RPN.
I'm curious as well, though, so I'd appreciate if you let me know in case
you find something.
However, once you have an unfolded proof, the algorithm to generate its
condensed detachment proof (in Polish notation) is rather simple, something
like this:
string DRuleParser::condensedDetachmentString(const DlProof* proof) {
auto recurse = [&](unsigned pos, stringstream& ss, const auto& me) -> void {
const DlProofReason& reason = proof->reasonAt(pos);
switch (reason.type) {
case DlProofReasonType::ModusPonens:
ss << "D";
me(reason.metadata[1], ss, me);
me(reason.metadata[0], ss, me);
break;
case DlProofReasonType::Axiom: {
unsigned axiomNumber = reason.metadata[0];
if (axiomNumber < 1 || axiomNumber > 3)
throw logic_error("DRuleParser::condensedDetachmentString(): Unimplemented
axiom number " + to_string(axiomNumber) + " for (" + proof->name() + ").");
switch (axiomNumber) {
case 1:
ss << "1";
break;
case 2:
ss << "2";
break;
case 3:
ss << "3";
break;
}
break;
}
case DlProofReasonType::Alias:
me(reason.metadata[0], ss, me);
break;
case DlProofReasonType::Necessitation:
throw logic_error("DRuleParser::condensedDetachmentString(): Unimplemented
reason type 'Necessitation' for (" + proof->name() + ").");
case DlProofReasonType::Premise:
throw logic_error("DRuleParser::condensedDetachmentString(): Unimplemented
reason type 'Premise' for (" + proof->name() + "). You shall not pass a
conditional proof.");
case DlProofReasonType::Reference:
throw logic_error("DRuleParser::condensedDetachmentString(): Unimplemented
reason type 'Reference' for (" + proof->name() + "). You shall not pass a
retracted proof.");
default:
throw logic_error("DRuleParser::condensedDetachmentString(): Unknown reason
type for (" + proof->name() + ").");
}
};
stringstream ss;
unsigned startPos = proof->length();
if (startPos == 0)
return "";
recurse(startPos, ss, recurse);
return ss.str();
}
The above C++ example works for propositional proofs (ax-1, ..., ax-3) only.
Note that there are some seriously long proofs in set.mm (which aims not to
minimize proofs, but to minimize the overall size of the database).
Here are some that I queried (with an unpublished tool) over only the
propositional proofs of set.mm (version 0.198). The fourth column is the
unfolded proof length.
411. ax2 7 146802383
>\phi\imply(\psi\imply\chi)\imply(\phi\imply\psi\imply(\phi\imply\chi))
1083. merco1lem14 11 102457811
>\phi\imply\psi\imply\psi\imply\chi\imply(\phi\imply\chi)
1084. merco1lem15 3 136706393
>\phi\imply\psi\imply(\phi\imply(\chi\imply\psi))
1085. merco1lem16 5 144363881
>\phi\imply(\psi\imply\chi)\imply\tau\imply(\phi\imply\chi\imply\tau)
1086. merco1lem17 24 223234495
>\phi\imply\psi\imply\phi\imply\chi\imply\tau\imply(\phi\imply\chi\imply\tau)
1087. merco1lem18 19 476274051
>\phi\imply(\psi\imply\chi)\imply(\psi\imply\phi\imply(\psi\imply\chi))
1285. nic-luk1 23 682656735
>\phi\imply\psi\imply(\psi\imply\chi\imply(\phi\imply\chi))
1286. nic-luk2 11 297742468 >\not\phi\imply\phi\imply\phi
1287. nic-luk3 10 359490068 >\phi\imply(\not\phi\imply\psi)
1647. retbwax1 29 1770374047
>\phi\imply\psi\imply(\psi\imply\chi\imply(\phi\imply\chi))
So, for example, the D-proof of https://us.metamath.org/mpeuni/retbwax1.html
alone would be 1770374047 bytes, i.e. approx 1.64 GiB.
— Samiro Discher
[email protected] schrieb am Donnerstag, 6. April 2023 um 02:29:25
UTC+2:
> I am wondering if there is a way to display full RPN proof of an assertion
> in set.mm without relying on any previously proved theorems. I would like
> instead to include the proofs of the used theorems in the final RPN, which
> would only reference the axioms.
>
> --Guga
>
--
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/444ca4bf-71c9-4460-bea2-e01ec44ffdecn%40googlegroups.com.
