[opentheory-users] Prover9 HOL integration via OpenTheory

[Joe Hurd]

Hi Ramana,

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

Great work!

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

After a bit of wrangling I was able to extract the goal

!x. ?y. !z. (x \/ z) /\ y

from HOL Light in article format, and when I pasted it in I got

Exception raised at QDimacs.write_qdimacs_file:
term is not a QBF (innermost quantifier must be existential)

So I negated everything

?x. !y. ?z. (~x /\ ~z) \/ ~y

and then got

Exception raised at QDimacs.write_qdimacs_file:
term is not a QBF (variable expected, subterm '¬x ∧ ¬z' found)

Aha! It wants CNF, so I clausified the goal

?x. !y. ?z. (~x \/ ~y) /\ (~z \/ ~y)

and then got an article file back that successfully proved my query:

$ bin/polyml/opentheory info result.art
WARNING: 4,284 objects left in the dictionary by result.art
2 input type operators: -> bool
9 input constants: = ! /\ ==> ? \/ ~ F T
19 assumptions:
  |- T
  |- (~) = \t. t ==> F
  |- (!) = \P. P = \x. T
  |- ~(p ==> q) ==> p
  |- !t. ~~t <=> t
  |- ~(p ==> q) ==> ~q
  |- (==>) = \p q. p /\ q <=> p
  |- !t. (t <=> T) \/ (t <=> F)
  |- (/\) = \p q. (\f. f p q) = \f. f T T
  |- (?) = \P. !q. (!x. P x ==> q) ==> q
  |- (\/) = \t1 t2. !t. (t1 ==> t) ==> (t2 ==> t) ==> t
  |- (p <=> ~q) <=> (p \/ q) /\ (~q \/ ~p)
  |- (!t. ~~t <=> t) /\ (~T <=> F) /\ (~F <=> T)
  |- (p <=> q \/ r) <=> (p \/ ~q) /\ (p \/ ~r) /\ (q \/ r \/ ~p)
  |- (p <=> q /\ r) <=> (p \/ ~q \/ ~r) /\ (q \/ ~p) /\ (r \/ ~p)
  |- !t.
       ((T <=> t) <=> t) /\ ((t <=> T) <=> t) /\ ((F <=> t) <=> ~t) /\
       ((t <=> F) <=> ~t)
  |- !t.
       (T /\ t <=> t) /\ (t /\ T <=> t) /\ (F /\ t <=> F) /\
       (t /\ F <=> F) /\ (t /\ t <=> t)
  |- !t.
       (T \/ t <=> T) /\ (t \/ T <=> T) /\ (F \/ t <=> t) /\
       (t \/ F <=> t) /\ (t \/ t <=> t)
  |- (p <=> q <=> r) <=>
     (p \/ q \/ r) /\ (p \/ ~r \/ ~q) /\ (q \/ ~r \/ ~p) /\ (r \/ ~q \/ ~p)
1 theorem:
  |- ?x. !y. ?z. (~x \/ ~y) /\ (~z \/ ~y)

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

I'd be happy to put together a HOL Light tactic that does this, if you
haven't already started work on this, since I already have all the
machinery for logging goals. It would be great to also see this
working in Isabelle.

Very nice work - the first tactic in the cloud.

Cheers,

Joe