On Jun 26, 2012 8:56 PM, "Rob Arthan" <[email protected]> wrote:
>
>
> On 26 Jun 2012, at 09:39, Ramana Kumar wrote:
>
>> I think you shouldn't use new_constant and new_definition. Just the
latter should be enough to create the new constant with its definition. The
former creates a constant without a definition
>
> Correct.
>
>> (it's like new_axiom in that it should be avoided)
>
> new_constant wasn't what the OP wanted in the case in point, but the
theory extensions it makes are conservative, i.e., they extend the
vocabulary you can use but don't extend the statements that can be proved
that don't involve the new vocabulary. I see no reason for telling people
to avoid new_constant. If you use new_axiom, the system gives no guarantee
that what you have done is consistent. That problem doesn't arise with
new_constant.
Good point! Thanks for the correction.
I might just add that introducing new constants without giving them
definitions is, while conservative, often not useful because you can't
prove anything about them.
>
> Regards,
>
> Rob.
>
------------------------------------------------------------------------------
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
