[opentheory-users] a standalone tactic translating numeral encodings

[Joe Hurd]

Yep, looks like it works fine now, in case we ever need to de-Norrish
some numerals from HOL Light.

Cheers,

Joe

On Thu, Apr 5, 2012 at 11:25 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> My code works fine on this article. The problem was my CGI script. It should
> be fixed now.
> (It had a call to runhaskell n2b.hs which got confused when called from
> another directory, so now I've given it an absolute path to n2b.hs.)
>
> On Thu, Apr 5, 2012 at 11:10 PM, Joe Hurd <joe at gilith.com> wrote:
>>
>> Hi Ramana,
>>
>> > My guess is that you're generating an article with HOLLight.BIT2 rather
>> > than
>> > Number.Natural.bit2, but I haven't actually run your attempt.
>> > If that's not the problem it would be helpful if you could send me the
>> > article that gets passed to the web tactic (or maybe I should have some
>> > infrastructure for saving it...)
>>
>> I've attached the article encoding the goal: FYI the opentheory
>> summary for it is:
>>
>> $ opentheory info n2b-goal.art
>> 3 input type operators: -> bool Number.Natural.natural
>> 5 input constants: F Function.K Number.Natural.bit1 Number.Natural.bit2
>>  Number.Natural.zero
>> 1 assumption:
>>  |- Function.K F
>>       (Number.Natural.bit2 (Number.Natural.bit1 (Number.Natural.bit2 0)))
>> 1 theorem:
>>  |- Function.K F
>>       (Number.Natural.bit2 (Number.Natural.bit1 (Number.Natural.bit2 0)))
>>
>> > The function n2b near the top of the file is the algorithm.
>> > It's been a while, so let's see if I can figure out the algorithm just
>> > by
>> > reading that code...
>>
>> Your algorithm looks absolutely fine, and should scale up to any size
>> of natural number that a theorem prover could conceivably process.
>>
>> Cheers,
>>
>> Joe
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>