[opentheory-users] a standalone tactic translating numeral encodings

[Ramana Kumar]

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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20120406/d69f5f2f/attachment.htm>