<div dir="ltr">Hi Rob,<div><br></div><div>It might perhaps be a nice feature if the "axiom" command didn't just match alpha-equivalent theorems, but was able to rename/instantiate type and free term variables too. However, that seems like a lot to ask of an article reader, and in any case it wouldn't solve the problem of processing type variables when reading articles exported from another theorem prover with different conventions.</div>
<div><br></div><div>There was some discussion on the list a while back about standardizing names for type variables:</div><div><br></div><div><a href="http://www.gilith.com/opentheory/mailing-list/2011-September/000114.html">http://www.gilith.com/opentheory/mailing-list/2011-September/000114.html</a><br>
</div><div><br></div><div>The best solution seems to be for the OpenTheory standard theory library to adopt one convention (currently capital letters, like HOL Light), and for other theorem provers to convert them to their local convention as part of reading/writing articles (e.g., HOL4 would map A to 'a, B to 'b, etc.)</div>
<div><br></div><div>I have added a note about this to the documentation for the varType command in the article format:</div><div><br></div><div><a href="http://www.gilith.com/research/opentheory/article.html#varTypeCommand">http://www.gilith.com/research/opentheory/article.html#varTypeCommand</a><br>
</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 Fri, Nov 29, 2013 at 3:23 PM, Rob Arthan <span dir="ltr"><<a href="mailto:rda@lemma-one.com" target="_blank">rda@lemma-one.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word">The OpenTheory "thm" command  allows for an alpha-conversion to get the variable names in a theorem exactly right. The description doesn't say anything about type instantiation, so presumably type variable names have to be right already. Perhaps it should allow type variable renaming too, because the choice of type variable names in definitions of existing constants (like the quantifiers) is going to be implementation-dependent. Unfortunately, this is a little tricky to specify and implement because "thm" also allows the inferred theorem to have fewer assumptions than the target theorem. <div>
<br></div><div>On this topic, the Gilith OpenTheory Repo seems to use HOL Light type variable names (A, B, C etc.) that can't be parsed in HOL4 or ProofPower. In any case, if "thm" doesn't allow for type variable renaming, then the documentation needs to say what type variables have been used.</div>
<div><br></div><div>Regards,</div><div><br></div><div>Rob.</div><div><br></div></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>