[opentheory-users] Prover9 HOL integration via OpenTheory

[Ramana Kumar]

On Mon, Oct 10, 2011 at 6:28 PM, Joe Hurd <joe at gilith.com> wrote:
> What I would love to see is these kind of tactics available as "web
> services", so during theorem proving you could send goals to an URL
> that would try to prove them using specialized tactics and send you
> back a proof if they were successful. The nice thing about this
> architecture is that the user wouldn't need to install the external
> tools, and even if the proof tool was non-deterministic the proof
> would be saved by the user so there wouldn't be any problems replaying
> it.

I've uploaded a rough-and-ready cgi script that runs the qbf
integration here: http://cam.xrchz.net/holqbf.cgi

You either type (or paste) an article into the text box there and
click submit, or you can pass it programmatically using, for example,
curl:
$ curl -F "article=@/path/to/term.art" cam.xrchz.net/holqbf.cgi
and it will (if successful) return a plain text file which is an
article encoding a proof of the term (or its negation).
If unsuccessful it will hopefully return a plain text file with some
kind of error message.

I'd love to get feedback from anyone who uses this - it will probably
break and I'm happy to try to fix it.
I might eventually try to write a tactic in HOL Light or Isabelle that
simply calls out to this service... (it's not so great for HOL4 since
the code originally came from HOL4 so you can just the tactic there
already)