> For automated Polish notation parsing, I am only aware of [...] Apparently I was mistaken. I meant http://us.metamath.org/downloads/drule.c, which seems is not part of metamath-exe.
Samiro Discher schrieb am Donnerstag, 6. April 2023 um 03:41:00 UTC+2: > 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/7e45e05a-3562-41bb-9717-88dc88354c97n%40googlegroups.com.
