[opentheory-users] numerals

[Michael Norrish]

On 07/09/2011, at 7:04 AM, Joe Hurd <joe at gilith.com> wrote:

> It is possible to convert between numeral representations as part of
> the interface between OpenTheory and the HOL theorem prover, with more
> or less fiddliness. One possible scheme for this is to carry out
> numeral calculations in the local representation, and only convert the
> assumptions and theorems of the theory interface to the OpenTheory
> standard numerals (perhaps as a post-processing phase).

I certainly wouldn't want to have to take a HOL4 calculation of some ground formula and then, when ready to export, have to turn that calculation into one that was a valid HOL Light/OpenTheory calculation.  I already have one implementation of numeral calculations; why should I have to write a second?  (Similarly, for ProofPower calculations of course.) Instead, it seems like my best option is to just export theories that have all their internal numerical results as assumptions (converting the statement of results is clearly a reasonable requirement).  

Perhaps the OpenTheory infrastructure could then provide a tool to automatically discharge such assumptions by proving them.  Ideally this would be SML code that our exporters could call as part of the export process.  Less, ideally, this tool could package up HOL Light to actually perform the requisite proofs.

In the opposite direction, i.e. reading, things shouldn't be too bad: readers can recognize numerical calculations and call out to their own tools to do the necessary work.  This would obviously work just as well for those theories that listed their numerical results as axioms/assumptions.

Michael
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20110907/4b2fbb44/attachment-0001.html>