[opentheory-users] Prover9 HOL integration via OpenTheory

[Joe Hurd]

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