Is it possible to add newly defined/proved constants and theorems to the
database used by this service, so it can be used to prove lemmas in a
development in progress?
On Fri, Nov 30, 2012 at 5:29 PM, Josef Urban <[email protected]> wrote:
> Automated reasoning service using about 16000 Flyspeck (and HOL
> Light) theorems is now available. The implementation and related
> experiments are described in http://arxiv.org/abs/1211.7012 .
>
> Example queries are:
>
> ====================
> echo 'inv(&2 pow N2) = &1 / &2 pow N2' | nc colo12-c703.uibk.ac.at 8080
>
> echo '(X INTER Y INTER Z) = (INTERS {X,Y,Z})' | nc colo12-c703.uibk.ac.at8080
>
> echo '30+(7*9)=93' | nc colo12-c703.uibk.ac.at 8080
>
> echo '!m c x y. ~(m = &0) ==> (m * x + c = &0 <=> x = --(c / m))' | nc
> colo12-c703.uibk.ac.at 8080
>
> echo '(A DIFF B) INTER C = EMPTY <=> (A INTER C) SUBSET B' | nc
> colo12-c703.uibk.ac.at 8080
>
> echo 'f continuous_on s /\ closed s /\ f continuous_on s1 /\ closed s1 ==>
> measurable_on f (s UNION s1)' | nc colo12-c703.uibk.ac.at 8080
> ====================
>
> The service is experimental, will time out after 30 seconds, and will
> just silently fail on parsing errors.
>
> A simple Emacs code for calling the service is at:
> https://raw.github.com/JUrban/hol-advisor/master/hol-advice.el .
> Use as follows:
>
> M-x load-file RET hol-advice.el RET
> M-x hol-ask-advisor RET ~F ==> T RET
>
> Proofs can be often reconstructed in HOL Light from the service
> replies using the MESON tactic. For interested users who do not have
> Flyspeck loaded, the advised theorems can often be looked up here:
> http://mizar.cs.ualberta.ca/~mptp/hol-flyspeck/index.html .
>
>
> Cezary Kaliszyk & Josef Urban
>
>
> ------------------------------------------------------------------------------
> Keep yourself connected to Go Parallel:
> TUNE You got it built. Now make it sing. Tune shows you how.
> http://goparallel.sourceforge.net
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
See everything from the browser to the database with AppDynamics
Get end-to-end visibility with application monitoring from AppDynamics
Isolate bottlenecks and diagnose root cause in seconds.
Start your free trial of AppDynamics Pro today!
http://pubads.g.doubleclick.net/gampad/clk?id=48808831&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
