I agree; I think implementing compressed proof reading is worth the effort,
particularly because of the exponential speedup over uncompressed proofs
(in the worst case). The scheme is pretty simple to work with. Be sure to
read appendix C of the metamath book, which lays it all out clearly.
On
I found proof decompression to be easier to implement than I thought it
would be. The hardest part was just understanding how it works.
On Tuesday, December 3, 2019 at 3:32:07 PM UTC+1, Marko Grdinic wrote:
>
> Well, at any rate as I've been working on this for 9 days now I'll stop
> here. I do
On Tue, 3 Dec 2019 06:32:07 -0800 (PST), Marko Grdinic wrote:
> Well, at any rate as I've been working on this for 9 days now I'll stop
> here. I do not feel like going those last few extra miles just to implement
> proof decompression and test it thoroughly on the big library. I am not
> sure
Yeah, it works fine on demo0.mm. I did some examples by hand to make sure
that disjointment constraints are verified properly as well.
Dana utorak, 3. prosinca 2019. u 16:18:22 UTC+1, korisnik Antony Bartlett
napisao je:
>
> Uncompressing the entire set.mm database was last discussed here
>
>
Uncompressing the entire set.mm database was last discussed here
https://groups.google.com/forum/#!msg/metamath/Hey2L9f1ULk/vXMWVcI5DwAJ
Can your verifier check demo0.mm yet? (
https://github.com/david-a-wheeler/metamath-test/blob/master/demo0.mm)
Best regards,
Antony
On Tue, Dec
Well, at any rate as I've been working on this for 9 days now I'll stop
here. I do not feel like going those last few extra miles just to implement
proof decompression and test it thoroughly on the big library. I am not
sure how stringent the criteria for inclusion on that list of verifiers in
Sorry about this, as soon as I posted I realized that I had completely
forgotten about compressed proofs.
--
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
