[opentheory-users] Prover9 HOL integration via OpenTheory

[Ramana Kumar]

Further to this, it would be nice to try the same method with Metis.
Specifically I think that would mean writing a HOL->FOL mapping for
standalone metis, where the HOL is encoded as an article, and then
also a proof->article translation for metis proofs. Metis was designed
for direct integration, so then we could compare how much worse the
roundabout integration performs compared to the direct one. If it's
not too bad, that would make integration via OpenTheory look like an
OK idea (not just for portability in desperate circumstances).

On Wed, Sep 14, 2011 at 11:48 PM, Joe Hurd <joe at gilith.com> wrote:
> Hi Ramana,
>
> This sounds like a great project! I can think of lots of tactics I'd
> like to share between theorem provers, and this project was successful
> it could provide a template that could be instantiated for primality
> proving, the Omega test, etc.
>
> I'd be happy to help by contributing the HOL Light reader. One thing I
> might suggest, having thought a little about this application, is
> related to this:
>
>> The input article file is "non-standard" in that the semantics is to return
>> the higher order logic term left at the top of the stack after processing.
>> Thus the input article represents a term.
>
> It's perfectly possible to use a standard article that contains one theorem
>
> {hypotheses} |- conclusion
>
> where the proof is simply "axiom". Then the tactic could prove this
> theorem with a proper proof extracted from prover9, and return this as
> another article.
>
> Tactics generally operate on sequents
>
> {assumptions} ?- goal
>
> so it's natural to serialize this as an article containing a single
> theorem with a null (axiom) proof.
>
> Cheers,
>
> Joe
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>