[opentheory-users] Scalable LCF-style proof translation

[Joe Leslie-Hurd]

Hi Ramana,

I'm still not convinced that the proof format in Cezary & Alex's paper is
more concise than OpenTheory, here is where the discussion ended last time:

On Wed, Jul 31, 2013 at 2:49 PM, Alexander Krauss <krauss at in.tum.de> wrote:

> On 07/26/2013 11:29 PM, Joe Leslie-Hurd wrote:
>
>> Given these minor differences, I'm intrigued by the statement in the
>> conclusion:
>>
>> "In our development we defined a new format for proof exchange traces,
>> despite
>> the existence of other exchange formats. We have tried writing the
>> proof trace in the
>> OpenTheory format, and it was roughly 10 times bigger."
>>
>> Cezary, Alex: Would it be possible to share this proof trace in the
>> two formats, so I can see what difference is responsible for the
>> blow-up?
>
>
> I must pass this question on to Cezary, who made this specific experiment.
> I'm not even sure whether this is before or after compression... But just
> looking at the list of OpenTheory commands, it seems to me that building up
> substitutions as nested lists on the stack is rather complicated.


So the 10x size increase may simply have been an artifact of comparing
against an uncompressed OpenTheory proof file. If Cezary could dig up the
proof files that were used for this comparison, I'd be very happy to take a
look and see whether there's something deeper that is going on.

Unfortunately I think that proof formats (like both of these) that
explicitly record every low-level inference are doomed to be bogged down by
massive proofs. I've thought about some ways to scale better, such as
adding a new "rewrite" OpenTheory command that behaves like REWRITE_CONV,
but such rules are hard to specify precisely to guarantee identical
behaviour on different platforms.

I'd be interested in hearing your ideas about how to scale better in proof
formats while preserving portability.

Cheers,

Joe



On Tue, Feb 18, 2014 at 9:12 AM, Ramana Kumar <ramana at member.fsf.org> wrote:

> Hi Joe, Cezary, Alex,
>
> I am planning, in the next few months, to export an extremely large
> proof from HOL4 into a format where I can check it with a standalone
> checker. (This proof takes hours to construct in HOL4.) OpenTheory
> seems the obvious choice as a proof storage medium, but the current
> format and implementations struggle with even moderate-sized proofs.
> I'd be very interested to hear about progress towards using the ideas
> from Cezary and Alex's paper to improving the scalability of
> OpenTheory technology. Have you made any progress on this front? Would
> you be interested in working on it with me?
>
> I hope we will be able to coordinate on this, since I think it's
> important work and each of us has something crucial to offer towards
> it.
>
> As a first item, I would think that the OpenTheory article format
> needs to be updated, as we were discussing earlier. Joe, Alex, did you
> come to any conclusions about whether changes are necessary and what
> they would look like?
>
> Cheers,
> Ramana
>
> On Tue, Aug 6, 2013 at 1:02 AM, Ramana Kumar <ramana at member.fsf.org>
> wrote:
> > On Mon, Aug 5, 2013 at 11:49 PM, Alexander Krauss <krauss at in.tum.de>
> wrote:
> >>
> >>
> >>> The opentheory tool post-processes articles extracted from theorem
> >>> provers, for compression and neatness purposes. To that end it does
> >>> both of the things you call out.
> >>
> >>
> >> Which command do I have to run to get this?
> >
> >
> > Install opentheory as per
> > http://www.gilith.com/software/opentheory/install.html.
> > Then run it like:
> >   opentheory info --article --output processed.art input.art
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20140218/0828a5e9/attachment.html>