[opentheory-users] Standalone Tactics using OpenTheory

[Ramana Kumar]

On Mon, Nov 19, 2012 at 6:41 AM, Felix Breuer <felix at fbreuer.de> wrote:

> Hello Ramana, hello Joe,
>
> I have read your article "Standalone Tactics using OpenTheory" with great
> interest and I have two questions:
>

Hi Felix, lovely to hear this.

1) Is the code for the system you describe (both client and the HOL4 and
> HOL Light "servers") available somewhere? I'd like to try this out myself.
>

Yes it is, but may be in a state of disrepair. I'd be happy to work with
you in understanding it and/or getting it to run.

For the HOL4 client, code is available in the src/opentheory/logging
directory of the (master branch of the) development version of HOL4.
For example, see the function url_conv here
https://github.com/mn200/HOL/blob/master/src/opentheory/logging/OpenTheoryIO.sml
.

For the HOL Light client, code is available in the opentheory/cloud
directory of Joe's proof-logging fork of HOL-Light.
I don't think it's browseable online, but instructions for getting it are
here http://src.gilith.com/hol-light.html
opentheory/cloud/cloud.ml has some examples of using the client.

For the HOL4 server, there are some examples in the same place as the
client code, namely:
https://github.com/mn200/HOL/blob/master/src/opentheory/logging/holdecide.smland
https://github.com/mn200/HOL/blob/master/src/opentheory/logging/skico.sml
The CGI script is also there:
https://github.com/mn200/HOL/blob/master/src/opentheory/logging/term2thm.cgi

The HOL Light client is also in the proof-logging fork of HOL-Light.
The examples are in the base directory, called: prover9{main,make}.ml, and
minisat{main,make}.ml.
The last commit message affecting those files (commit 93caf6b7) has some
information about them.


>
> 2) I do not quite understand how the goals that are sent to the server are
> encoded using OpenTheory. As far as I understand an OT article provides
> facilities for encoding assumptions and theorems. How do goals fit into the
> picture?
>

Ah this was originally described in detail in the paper but it appears we
cut some details from the final version.
If you look at page 3, the paragraph starting "An article file represents a
theory...", that describes some of the story.

Is it clear how articles can encode theorems? To encode a term, then one
just needs to encode a theorem that contains that term in it. We currently
use the theorem |- K tm to encode tm (where K is a constant). (Using |- tm
= X, where X is a variable, would probably be aesthetically nicer to
represent the argument to a conversion. But it doesn't matter as long as
both server and client agree.)



>
> Thanks,
> Felix
>
> --
> http://www.felixbreuer.net
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20121119/4473267d/attachment.html>