[opentheory-users] Prover9 HOL integration via OpenTheory

[Ramana Kumar]

Remembering that HOL4 already has an integration, with a nice
interface, of the QBF solver Squolem (due mainly to Tjark Weber), I
decided to try this idea out on that.

And it seems to work. With only 17 lines of newly-written standard ML,
I can produce an executable (available gzipped at
cam.xrchz.net/holqbf.gz) that:
1. reads an article in from standard input
2. assumes the article produces a theorem with the axiom command that
has the QBF to consider as its conclusion
3. providing squolem2 is installed, calls squolem to decide whether
the QBF is valid or not
4. reconstructs the proof of (in)validity in HOL, and
5. writes an article representing that proof to standard output
(Steps 3 and 4 just reuse the existing HOL4 integration.)

I only tried it on some very simple examples (using HOL4 to read and
write articles, and also trying opentheory on the proof articles).
The proofs might depend on assumptions that are all in HOL4's standard
library, and hopefully mostly in the OpenTheory standard library too
(but probably not).

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?

There are bound to be major performance issues.

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

I don't think Isabelle/HOL currently has a QBF integration.
HOL-Light does have one, but it's based on a different proof
reconstruction method.
If anyone here (especially with some expertise in those two systems)
would be interested in working with me to test (and improve) this
"integration port" on those systems, please let me know :)

On Sat, Oct 8, 2011 at 10:11 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> Further to this, it would be nice to try the same method with Metis.
> Specifically I think that would mean writing a HOL->FOL mapping for
> standalone metis, where the HOL is encoded as an article, and then
> also a proof->article translation for metis proofs. Metis was designed
> for direct integration, so then we could compare how much worse the
> roundabout integration performs compared to the direct one. If it's
> not too bad, that would make integration via OpenTheory look like an
> OK idea (not just for portability in desperate circumstances).
>
> On Wed, Sep 14, 2011 at 11:48 PM, Joe Hurd <joe at gilith.com> wrote:
>> Hi Ramana,
>>
>> This sounds like a great project! I can think of lots of tactics I'd
>> like to share between theorem provers, and this project was successful
>> it could provide a template that could be instantiated for primality
>> proving, the Omega test, etc.
>>
>> I'd be happy to help by contributing the HOL Light reader. One thing I
>> might suggest, having thought a little about this application, is
>> related to this:
>>
>>> The input article file is "non-standard" in that the semantics is to return
>>> the higher order logic term left at the top of the stack after processing.
>>> Thus the input article represents a term.
>>
>> It's perfectly possible to use a standard article that contains one theorem
>>
>> {hypotheses} |- conclusion
>>
>> where the proof is simply "axiom". Then the tactic could prove this
>> theorem with a proper proof extracted from prover9, and return this as
>> another article.
>>
>> Tactics generally operate on sequents
>>
>> {assumptions} ?- goal
>>
>> so it's natural to serialize this as an article containing a single
>> theorem with a null (axiom) proof.
>>
>> Cheers,
>>
>> Joe
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>
>