[opentheory-users] article reader for HOL4

[Ramana Kumar]

On Mon, Jan 10, 2011 at 6:18 PM, Joe Hurd <joe at gilith.com> wrote:
> Hi Ramana,
>
>> 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.
>
> I recently wrote a paper on the OpenTheory standard library that
> contains some details on this:
>
> http://www.gilith.com/research/papers/stdlib.pdf
>
> Any comments would be gratefully received.
>
>> 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?
>
> I think there are a couple of important points here:
>
> 1. OpenTheory axioms are theory assumptions that mention type
> operators or constants defined in the theory. Assumptions that only
> mention undefined type operators and constants are not called axioms
> (even though the same "axiom" command is used to generate them), and
> the client theorem prover must provide theorems for these.
>
> 2. The whole of higher order logic as implemented in HOL theorem
> provers only depends on the 3 axioms listed in base-1.0, and each
> theorem prover already has local versions of these. Everything else is
> constructed definitionally, so the situation of needing additional
> axioms should never occur, which is why I initially said that axioms
> can be safely ignored.
>
> Does that make sense now?

1. makes sense. What may have been confusing before is that from the
reader's perspective versus from the article's perspective "defined"
and "undefined" are somewhat opposite.

For 2... I think we may just be interpreting our words differently. By
"axioms" I meant the list of theorems so labelled by opentheory info
--summary, and these cannot be ignored by a reader - they must be
provided by the reader for the article to succeed.

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