[opentheory-users] Prover9 HOL integration via OpenTheory

[Joe Hurd]

Hi Ramana,

This is very cool! I like this idea of a "standalone tactic".

> An obvious weakness at this point are that I can't think of anything
> better to produce than a binary, which isn't very portable. The source
> code is spread over the HOL4 repository. Any ideas?

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.

> And it would be nice to somehow enforce using only standard library assumptions.

Agreed - such tactics should track the standard library, just like
theories that depend on the standard library. I'm hoping that the
standard library will converge quickly once people start using it and
we develop guidelines for exported theorems.

Cheers,

Joe