[opentheory-users] Prover9 HOL integration via OpenTheory

[Mike Gordon]

Yes, cool indeed ...

> What I would love to see is these kind of tactics available as "web
> services"

... is this the start of cloud theorem proving! -- Mike

On Mon, Oct 10, 2011 at 6:28 PM, Joe Hurd <joe at gilith.com> wrote:
> Hi Ramana,
>
> This is very cool! I like this idea of a "standalone tactic".
>
>> 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?
>
> What I would love to see is these kind of tactics available as "web
> services", so during theorem proving you could send goals to an URL
> that would try to prove them using specialized tactics and send you
> back a proof if they were successful. The nice thing about this
> architecture is that the user wouldn't need to install the external
> tools, and even if the proof tool was non-deterministic the proof
> would be saved by the user so there wouldn't be any problems replaying
> it.
>
>> And it would be nice to somehow enforce using only standard library assumptions.
>
> Agreed - such tactics should track the standard library, just like
> theories that depend on the standard library. I'm hoping that the
> standard library will converge quickly once people start using it and
> we develop guidelines for exported theorems.
>
> Cheers,
>
> Joe
>