[opentheory-users] Prover9 HOL integration via OpenTheory

Rob Arthan rda at lemma-one.com
Mon Oct 17 15:45:02 UTC 2011


On 10 Oct 2011, at 18:43, Mike Gordon wrote:

> 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

Jacques Fleuriot and Steve Obua are on that track too, see:

http://proofpeer.appspot.com/html/currentVersion.html#

Cheers,

Rob.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20111017/aa2c03f1/attachment.html>


More information about the opentheory-users mailing list