<div class="gmail_extra"><div class="gmail_quote">On Mon, Nov 19, 2012 at 6:41 AM, Felix Breuer <span dir="ltr"><<a href="mailto:felix@fbreuer.de" target="_blank">felix@fbreuer.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hello Ramana, hello Joe,<div><br></div><div>I have read your article "Standalone Tactics using OpenTheory" with great interest and I have two questions:</div></blockquote><div><br>Hi Felix, lovely to hear this.<br>
</div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div>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.</div>
</blockquote><div><br>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.<br><br>For the HOL4 client, code is available in the src/opentheory/logging directory of the (master branch of the) development version of HOL4.<br>
For example, see the function url_conv here <a href="https://github.com/mn200/HOL/blob/master/src/opentheory/logging/OpenTheoryIO.sml" target="_blank">https://github.com/mn200/HOL/blob/master/src/opentheory/logging/OpenTheoryIO.sml</a>.<br>
<br>For the HOL Light client, code is available in the opentheory/cloud directory of Joe's proof-logging fork of HOL-Light.<br>I don't think it's browseable online, but instructions for getting it are here <a href="http://src.gilith.com/hol-light.html" target="_blank">http://src.gilith.com/hol-light.html</a><br>
opentheory/cloud/<a href="http://cloud.ml" target="_blank">cloud.ml</a> has some examples of using the client.<br><br>For the HOL4 server, there are some examples in the same place as the client code, namely:<br><a href="https://github.com/mn200/HOL/blob/master/src/opentheory/logging/holdecide.sml" target="_blank">https://github.com/mn200/HOL/blob/master/src/opentheory/logging/holdecide.sml</a> and<br>
<a href="https://github.com/mn200/HOL/blob/master/src/opentheory/logging/skico.sml" target="_blank">https://github.com/mn200/HOL/blob/master/src/opentheory/logging/skico.sml</a><br>The CGI script is also there:<br><a href="https://github.com/mn200/HOL/blob/master/src/opentheory/logging/term2thm.cgi" target="_blank">https://github.com/mn200/HOL/blob/master/src/opentheory/logging/term2thm.cgi</a><br>
<br>The HOL Light client is also in the proof-logging fork of HOL-Light.<br>The examples are in the base directory, called: prover9{main,make}.ml, and minisat{main,make}.ml.<br>The last commit message affecting those files (commit 93caf6b7) has some information about them.<br>
</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div><br></div><div>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?</div>
</blockquote><div><br>Ah this was originally described in detail in the paper but it appears we cut some details from the final version.<br>If you look at page 3, the paragraph starting "An article file represents a theory...", that describes some of the story.<br>
<br>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.)<br>
</div><div><br> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div><br></div><div>Thanks,</div><div>Felix<span><font color="#888888"><br clear="all"><div><br></div>-- <br><a href="http://www.felixbreuer.net" target="_blank">http://www.felixbreuer.net</a><br>
</font></span></div>
<br>_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
<br></blockquote></div><br></div>