[opentheory-users] Prover9 HOL integration via OpenTheory

[Ramana Kumar]

On Sat, Oct 15, 2011 at 7:10 PM, Joe Hurd <joe at gilith.com> wrote:
> Thanks for bringing this up - I was not aware of the terms of the license
>
> http://www.cprover.org/qbv/LICENSE.txt

I've written to the authors of squolem (at least to satisfy condition
5 of the license!) just now - thanks for the reminder.

>
>> 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.

The wishlist in HOL4's documentation (which I presume Tjark wrote most
of..) includes making HOL4 automatically convert any QBF into the
required form. I would have thought such a conversion already existed
in HOL4; I suspect the pieces do (e.g. propositional CNF conversion)
so I might try putting them together some time... But it would be
interesting if, say, there's a (arbitrary QBF -> prenex normal form)
conversion in HOL-Light or some other OpenTheory-enabled system, so I
could try having one web service calling another... Is there?

The wishlist also includes: interfacing with more QBF solvers, and
making QBF solvers into web services.

> 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?

System Description: SystemOnTPTP, Sutcliffe, CADE-17, 2000, seems like
a good start.
http://www.springerlink.com/content/a12854806p071760/