<div class="gmail_quote">On Fri, Jun 29, 2012 at 4:35 AM, Joe Hurd <span dir="ltr">&lt;<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">


Sounds cool - I&#39;d be happy to see an interchange of theories between<br>
the HOL family and Dedukti.<br></blockquote><div><br>I don&#39;t think there would be much &quot;interchange&quot;. As far as I&#39;m aware, Dedukti is for checking proofs, but not for re-exporting them for checking elsewhere. So it would be a sink in the graph of connections between formalisms. That said, I do think importing OpenTheory theories into Dedukti is a good idea.<br>

 </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
Right now no one has expended the effort to carve out a clean theory<br>
of inductive definitions, so it is in the default state of being<br>
statically linked into any theory that uses them.<br>
<div class="im"></div></blockquote><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote"><div> </div></blockquote><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">

...</blockquote><div></div><div></div><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote"><div> </div></blockquote><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">

<div class="im">This is most definitely a work in progress. real-thm currently just<br></div>
has a couple of trivial theorems in it, while real-def contains the<br>
entire HOL Light construction of the real numbers from the natural<br>
numbers, resulting in quite a big theory:<br></blockquote></div><br>To add to these replies, I think the OpenTheory standard library could benefit from a lot of development work on, for example, doing more dynamic linking, other restructuring to make it more useful, and adding more theories or theorems.<br>

As far as I can tell, only Joe is working on it.<br>Part of the reason why more people aren&#39;t working on it could be that it&#39;s not obvious how to incorporate the OpenTheory standard library into daily work on other formal developments, and therefore how useful it might be in practice. Perhaps we could discuss ideas for improving this situation on list (maybe in a different thread). A roadmap for OpenTheory development could be useful.<br>