[opentheory-users] article reader for HOL4

[Ramana Kumar]

On Mon, Jan 10, 2011 at 3:20 AM, Joe Hurd <joe at gilith.com> wrote:
> Hi Ramana,
>
>> Well although I see the usefulness of reading articles that mainly give you new
>> constants/theorems that you don't already have versions of in your proof
>> assistant, I think the more general approach where you might read base-1.0 into
>> HOL4 is worth pursuing because base-1.0 might say just a few different or
>> interesting things about basic things that HOL4 has its own versions of.  The
>> most useful way to read base-1.0 in is to make it "define" your already-defined
>> constants by simulating the effect of the definition (proving the necessary
>> theorem whenever base-1.0 defines things slightly differently etc.). In the end
>> you get a bunch of theorems many of which you already have but some of which
>> you might not. And importantly, these will be in the exact right format and
>> number to pass along to later opentheory articles that depend on base-1.0.
>
> I can appreciate your reasons for wanting to import articles this way,
> but (as you say) there is an additional implementation cost of
> managing clashing definitions.

All right.
I'd love to see how you envision the purpose of opentheory and
articles and how they would interact with various proof assistants, if
you've written that down anywhere I might not have seen yet. I know
there are those two papers on your website.

>
> My comment about ignoring axioms only applies when reading articles
> without clashing definitions. In your more general case I believe you
> can simply treat axioms like assumptions, because the distinction
> between defined and input has disappeared.

It's still confusing, and what to make sure I'm not misunderstanding
something significant.
Suppose you're reading an article without any clashing definitions,
i.e. any constant the article wants to define is not already defined
in the reader's world.
The axioms of the article will be about those undefined constants.
When the reader comes to process the axiom command, it needs to
provide a theorem.
How is the reader supposed to have a theorem about a constant it
hasn't yet defined?
Presumably before it comes to the axiom command, it will have
processed the definitional commands so the constants will by then be
defined, but since the article doesn't prove the axioms, the theorems
won't be there - the article reader would have to delegate proving of
the axiom off to some proof procedure (possibly interactive), or would
have to return a continuation that takes the axiom theorem and
continues processing the file, sort of leaving you with a function
from axioms to theorems, but not quite (the main problem here is that
HOL4's definition mechanism is stateful; if it weren't you probably
could just get such a plain function from theorems to theorems as the
result of reading an article, but since it's stateful it's more
obvious to use something like continuations). Neither of these options
are really described by just ignoring the axiom...

>
> Cheers,
>
> Joe
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>