Proof generation

[Jorge Agra]

Greetings,

tried to find a definition for proof generation from a list of statements/expressions+justifications+dependencies.

mmj2, metamath.exe, yamma, metamath-lamp, all generate valid proof statements, but could not find a spec on the requirements that they implement.

Is a spec available, even if informally?

Best regards.

[Mario Carneiro]

The specification for metamath checking in general is given in the Metamath Book: https://us.metamath.org/downloads/metamath.pdf

The proof blocks are written in "compressed proof format", which is specified in Appendix B of the metamath book. (Although, metamath-exe, mmj2 and metamath-knife generate proofs which are byte identical because they also implement a specific sorting / packing strategy taking advantage of some flexibility in the specification to produce more compact proofs. If you want to implement this you will have to read the code of one of these systems.)

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/e3b5b65e-1c4c-4f88-9ae1-a69e74b0ca0cn%40googlegroups.com.

[Glauco]

Hi jagra,

starting from an uncompressed proof, you can compress it in several different ways, depending on how you order the labels. There's not a spec for how you order the labels.

Yamma's configuration allows you to choose between three ordering algorithms:
fifo

mostReferencedFirst
mostReferencedFirstAndNiceFormatting

it may be fifo is the most "natural": it keeps the order of the uncompressed proof (but it leads to much longer proofs, w.r.t. the other "optimized" options)

by default, yamma uses

mostReferencedFirstAndNiceFormatting

it produces proofs that have the EXACT same LENGTH as those produced by mmj2 (I can't prove it, but I've checked it on the longest proofs in set.mm)

The proofs produced by mmj2 are not exactly the same, because (in my opinion) mmj2 has a small bug in the knapsack algorithm

Since the knapsack is only applied on subgroups of labels which are referred by "numbers" (capital letter strings) of the same length, a different order in these subgroups does not affect the overall length of the compressed proof. Thus, yamma and mmj2 produce proofs of the same length (yamma's proofs could sometimes have a better formatting)

You can find the code for this specific algorithm in this file

https://github.com/glacode/yamma/blob/master/server/src/mmp/proofCompression/MmpSortedByReferenceWithKnapsackLabelMapCreator.ts

IMHO, metamath.exe and mmj2 don't produce the same compressed proofs (I've shown several examples, in the past)

[Mario Carneiro]

On Mon, Feb 12, 2024 at 8:40 AM Glauco <glaform...@gmail.com> wrote:

The proofs produced by mmj2 are not exactly the same, because (in my opinion) mmj2 has a small bug in the knapsack algorithm

 

IMHO, metamath.exe and mmj2 don't produce the same compressed proofs (I've shown several examples, in the past)

I would be interested to hear specifics about these claims, because they are supposed to be the same and I haven't heard any bug reports to the contrary. I also don't understand what knapsack bug you are describing or why it is a matter of opinion whether it is a bug.

 

--
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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f687d4b6-412f-4be0-92b8-4d92dd893277n%40googlegroups.com.

[jagra]

Thanks both for the explanations.

I had it working, but since the generated proofs were in some cases so different from those in set.mm, I was trying to understand why.

One of the things I noticed, and caused the differences I had, was avoiding the use of $p statements in parsing rules. For instance, weq and wceq seem to be similar, but weq is a $p while wceq is a $a, but they seem to be basically equivalent when used in generated proof.

Including weq creates in some cases, several distinct correct parsing alternatives for the same statement, while using just $a rules (wceq instead of weq) does not. Tested (only) with ax8, replacing the original proof with one that contained a proof generated just from $a rules (from base ax8 proof statements), and set.mm was verified without errors.

The proof is bigger and I understand that's a concern always present, but, other than that, do you see any problems with it?

Best regards,

Jorge Agra

[Mario Carneiro]

I think mmj2 only ever uses wceq, because it "parses" formulas and using weq introduces an ambiguity into the resulting grammar. However metamath-exe's MINIMIZE will find shorter proofs using lemmas, and it treats syntax lemmas just like real lemmas, so it will "optimize" the proof to use weq. I think you shouldn't worry much about whether you produce one vs another, IMO having syntax lemmas was a mistake.

--
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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/980d8c60-d073-4784-81c8-11a698612730n%40googlegroups.com.