[opentheory-users] Questions about the standard library packages

[Ramana Kumar]

On Fri, Jun 29, 2012 at 4:35 AM, Joe Hurd <joe at gilith.com> wrote:

> Sounds cool - I'd be happy to see an interchange of theories between
> the HOL family and Dedukti.
>

I don't think there would be much "interchange". As far as I'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.


> Right now no one has expended the effort to carve out a clean theory
> of inductive definitions, so it is in the default state of being
> statically linked into any theory that uses them.
>

>
...


>
This is most definitely a work in progress. real-thm currently just
> has a couple of trivial theorems in it, while real-def contains the
> entire HOL Light construction of the real numbers from the natural
> numbers, resulting in quite a big theory:
>

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.
As far as I can tell, only Joe is working on it.
Part of the reason why more people aren't working on it could be that it'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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20120703/0daa2128/attachment.htm>