[opentheory-users] Scalable LCF-style proof translation

[Ramana Kumar]

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