[opentheory-users] Prover9 HOL integration via OpenTheory

[Joe Hurd]

Hi Tjark,

> There may be copyright issues if you make (the functionality of) Squolem
> available in this form.

Thanks for bringing this up - I was not aware of the terms of the license

http://www.cprover.org/qbv/LICENSE.txt

> The expected QBF format is documented in Section 5.10.2 of the HOL4
> Description (cf. http://hol.sourceforge.net/documentation.html).

For cloud tactics perhaps it makes sense to put this documentation on
the web page that provides the interface to the tactic, to help
integrators.

> Geoff Sutcliffe has made various provers available via his System On
> TPTP website (http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP).
> Isabelle's Sledgehammer tool can (since 2009) use some of these remotely
> in place of locally installed provers.

Again, thanks for the reference - I was not aware of this. Do you
happen to know a published reference to this, or someone I can ask
about this related work?

Perhaps a better characterization of the novelty is a way of sharing
tactics between theorem provers using the cloud (and using the
OpenTheory standard library to fix a shared ontology).

Cheers,

Joe