[opentheory-users] article reader for HOL4

[Rob Arthan]

Joe, & opentheory-users,

On 11 Jan 2011, at 00:30, Joe Hurd wrote:

> Hi Michael,
> 
> ....
>> What does ProofPower do for numerals?
> 
> I don't know the answer to this. Rob Arthan might, and since he isn't
> on this mailing list I have cc'ed him on this message.
> 

I should be on the list soon if the moderator will have me :-).

ProofPower predates the invention of the bit representations used in HOL4 and HOL Light and improves upon the Classic HOL base 1 representation, by treating natural number literals as a special case in the logical kernel. Natural number literals are constants distinguished by having the right type and having names comprising a string of decimal digits. There is a built-in conversion plus_conv which proves all theorems of the form |- m + n = k where m, n and k are natural number literals.

Regards,

Rob.