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
