[opentheory-users] article reader for HOL4

[Ramana Kumar]

On Sun, Jan 9, 2011 at 7:08 PM, Joe Hurd <joe at gilith.com> wrote:
> Hi Ramana,
>
> Thanks for implementing this: HOL4 is now the first theorem prover
> with an article reader!
>
> I'd like to try it out: how do I run it?

At this stage it's going to break on anything interesting you try it on...
But the basic method would be:

Build the latest svn version of HOL4

In a HOL4 session, do:

val input = (* article file, e.g. TextIO.openIn("/path/to/file.art") *)
val asms = (* net of theorems the article depends on, you can use
Opentheory.thmsFromList ls to create this from a list of HOL4 theorems *)
val consts = (* dictionary of constants the article depends on, keyed by their
name, and represented by functions (hol_type -> term).
You can use Opentheory.constsFromList ls,
e.g. constsFromList [("=",fn ty => Term.mk_const("=",ty))] *)
val types = (* dictionary of types the article depends on, keyed by their
names, and represented by functions (hol_type list -> hol-type).
You can use Opentheory.typesFromList ls,
e.g. typesFromList [("->",fn ls => Type.mk_type("fun",ls))] *)
val thms = Opentheory.read_article input {thms=asms,consts=consts,types=types}

If all goes well, thms should be bound to a list of theorems proved by
the article.

>
> Cheers,
>
> Joe
>
> On Sun, Jan 9, 2011 at 5:43 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>> I have added a preliminary version of an article reader to HOL4
>> (hol.sf.net, svn r8839)
>>
>> Which other proof assistants have readers, by the way? Is there a list
>> somewhere?
>>
>> On Sat, Jan 8, 2011 at 5:54 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>>> Does anyone know if there's an article reader for HOL4?
>>> Or, in fact, which theorem provers have article readers, and where can
>>> they be found?
>>> I'm thinking if there is none for HOL4 I should write it, and then put
>>> it with the HOL4 sources - or should it come with the opentheory?
>>>
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>