[opentheory-users] Prover9 HOL integration via OpenTheory

[Ramana Kumar]

John Harrison wrote an integration of Prover9 into HOL Light.
It translates a HOL Light (boolean) term into a Prover9 input file, runs
prover9 (a first-order automatic theorem prover), then reconstructs the
proof it generates.
(Happily, prover9 (with the bundled prooftrans) can generate extremely low
level detailed proofs; this was used for verification by an ACL2 proof
checker called Ivy.)

I briefly started porting the HOL Light integration to HOL4, but it occurs
to me that there's a much more exciting possibility here.
Let me give an outline.

The end product I want is a binary (or maybe OCaml sources) that takes an
article file as input and produces an article file as output.
The system requirements are just that prover9 is installed.
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.
The output article represents a proof of the theorem whose conclusion is
that term (and hypotheses are empty).

How to achieve?
Guiding principle: without porting lots of code! Just write code that should
be written anyway.
1. Finish writing the HOL Light article reader, and add an entry point to
get a term out of an article rather than the theorems.
2. Collect all the HOL Light code (actually, the logging fork of HOL Light)
on which prover9.ml depends, and simplify it if desired...
3. Write the entry point for a binary which does: read article from stdin to
get term, call PROVER9, log resulting theorem to stdout
4. Compile and distribute.

Someone previously told me he would very much appreciate a Prover9
integration for Isabelle, because Prover9 happens to solve the kinds of
goals in one of his developments better than other first-order provers.
Since there is already an article reader for Isabelle, the only extra code
required, given the above system, would be a limited article writer for
Isabelle that only needs to write terms (and I think typeclass information
can just be thrown away) in article format.
We have the integration into multiple proof assistants from effort for one.

I'd be very happy to do steps 2 through 4.
And also 1 except I think Joe may already be working on that, in which case
I'd rather wait.

I would like to hear if anyone on the list has any comments on the above
scheme or suggestions for improvement, or reasons why it's a bad idea.
(E.g. maybe using articles to represent formulas is silly, but it seems like
a good enough standard format to me and saves having to come up with yet
another language for representing syntax.)