[opentheory-users] Prover9 HOL integration via OpenTheory

[Tjark Weber]

On Fri, 2011-10-14 at 12:37 -0700, Joe Hurd wrote:
> > I've uploaded a rough-and-ready cgi script that runs the qbf
> > integration here: http://cam.xrchz.net/holqbf.cgi

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

> term is not a QBF (innermost quantifier must be existential)
> [...]
> term is not a QBF (variable expected, subterm '¬x ∧ ¬z' found)
> 
> Aha! It wants CNF, so I clausified the goal

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

> Very nice work - the first tactic in the cloud.

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.

Kind regards,
Tjark