<div dir="ltr">Sorry I'm late to the thread - I have just jumped 8 time zones to visit the UK for a while.<div><br></div><div>As Ramana said, the opentheory tool is supposed to be the main way that you interact with the theory directory in ~/.opentheory, and Ramana gave you the right invocation to covert a theory package to an article file:</div>
<div><br></div><div><a href="http://www.gilith.com/research/opentheory/faq.html#convert-theory-to-article">http://www.gilith.com/research/opentheory/faq.html#convert-theory-to-article</a><br></div><div><br></div><div>The NAME-VERSION<span style="font-family:arial,sans-serif;font-size:12.666666984558105px">.art </span>article file you found inside</div>
<div><br></div><div>~/.opentheory/packages/NAME-VERSION</div><div><br></div><div>is actually a cache of the theorems in the theory package stored in article format, where the "proof" of each theorem just uses the axiom command. These theorem caches are used to match dependencies between packages without needing to read in the whole proof in the theory package.</div>
<div><br></div><div>Cheers,</div><div><br></div><div>Joe</div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Nov 24, 2013 at 3:29 PM, Ramana Kumar <span dir="ltr"><<a href="mailto:ramana@member.fsf.org" target="_blank">ramana@member.fsf.org</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">You can also use the -o or --output option instead of shell redirection.<br></div><div class="gmail_extra">
<br><br><div class="gmail_quote"><div><div class="h5">On Sun, Nov 24, 2013 at 2:46 PM, Rob Arthan <span dir="ltr"><<a href="mailto:rda@lemma-one.com" target="_blank">rda@lemma-one.com</a>></span> wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><div style="word-wrap:break-word">Ramana,<div><br><div><div><div>On 24 Nov 2013, at 09:45, Ramana Kumar wrote:</div>
<br><blockquote type="cite"><div dir="ltr"><div>I think the idea of the base package is that everything in it should already be supported by your theorem prover, so you don't need to import it - rather, you use it as a dependency for things you export from your theorem prover.<br>
<br></div></div></blockquote></div>I want to import it so I can have a better look at it. The kind of thing I want to do is to make sure that my reader can prove all the assumptions in it and to make sure that my writer only uses definitions and theorems that it provides when it is writing out a ProofPower inference as a sequence of OpenTheory inferences.</div>
<div><div><br><blockquote type="cite"><div dir="ltr">That said, I think you can generate a single article that performs all the proofs in a package, like base, using the opentheory tool with the info command and the --article option.<br>
</div><div class="gmail_extra">
<br></div></blockquote></div>I invoked opentheory like this:</div><div><br></div><div><span style="white-space:pre-wrap"> </span>opentheory info --article base</div><div><br></div><div>and after 12 minutes learnt that I should have invoked it like this:</div>
<div><br></div><div><span style="white-space:pre-wrap"> opentheory info --article base</span> >base.art</div><div><br></div><div>I am then able to import all 1117 theorems and 3 assumptions from base.art into ProofPower.</div>
</div><div><br></div><div>Thanks!</div><span><font color="#888888"><div><br></div><div>Rob.</div><div><br></div></font></span></div><br></div></div><div class="im">_______________________________________________<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></div></blockquote></div><br></div>
<br>_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com">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>