I wrote:
>> It also suffers from the problem that a polymorphic formula
>> assumed in this way can't be instantiated. Asserting an axiom
>> is more powerful. In HOL4 axiom usage can be tracked in a similar
>> way to how assumptions are propagated, so you can get the same
>> effect as using an assumption.
Cris then asked:
> Could you explain for us relative beginners a bit more what you mean here? I
> looked at the HOL Light code for PROVE_HYP, but the meaning and use are not
> clear to me.
>
> And anyway I am wondering if you mean that asserting an axiom is more
> powerful than _any_ ASSUME-like mechanism, or is somehow specific to
> PROVE_HYP.
>
> Additional enlightenment will be much appreciated.
>
> -Cris
One aspect of HOL that occasionally bites is that one needs to remember
that type variables are subject to similar constraints as term variables.
Suppose I want to ASSUME a formula containing a type variable, getting
a theorem
th = tm |- tm
I won't be able to instantiate said type variable in the conclusion of th
without also instantiating it in the hypotheses. On the other hand
new_axiom("foo",tm)
returns
|- tm
and you don't have that limitation to deal with. Of course, you've
then got a new
axiom roaming around and potentially obliterating the usefulness of your
formalization.
Konrad.
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
