The AI/ATP service for HOL Light ( HOL(y)Hammer -
http://colo12-c703.uibk.ac.at/hh/ ) is now updatable and serving multiple
HOL Light projects.
Registered users can upload new projects and update existing projects.
Anonymous users can try to solve conjectures automatically over any of the
uploaded projects.
The projects that are already available include: Flyspeck, Multivariate
Analysis, Complex Analysis, Base HOL Light, Model of HOL, Goedel's
incompleteness theorem, Jordan Curve theorem and Infinite Ramsey theorem.
The uploaded projects are also heuristically hyperlinked, kept in Git
version control, and searchable through the GitWeb interface. If there is
sufficient demand, we can also implement project update on the server
through Git (upon git-push done by a registered user).
The service is described in http://arxiv.org/abs/1309.4962 .
Cezary Kaliszyk & Josef Urban
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
>
------------------------------------------------------------------------------
October Webinars: Code for Performance
Free Intel webinars can help you accelerate application performance.
Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most from
the latest Intel processors and coprocessors. See abstracts and register >
http://pubads.g.doubleclick.net/gampad/clk?id=60133471&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
