Hi Ramana,
On Fri, Jul 26, 2013 at 10:42 AM, Ramana Kumar <[email protected]>wrote:
> 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?
>
So far you have to do your own local install for that, see 'Local version'
at http://cl-informatik.uibk.ac.at/users/cek/hh/ . A bit more on this is in
Sections 3 and 4 of
http://cl-informatik.uibk.ac.at/users/cek/docs/kaliszyk-cicm13.pdf . This
is a bit similar to how Sledgehammer works locally in Isabelle.
We will likely make this functionality (users' own clones and updates)
available on our server by the end of August. We have developed the
mechanisms already for the MizAR ATP service and the Mizar wiki, so it
should not be a big deal. I quite strongly think that hard AI tasks (like
ATP/learning over large formal corpora) should take advantage of massive
parallelization and large-scale data-mining techniques on
servers/clusters/clouds. Google does not run on one's 2-CPU local computer
either :-).
Josef
>
>
> 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
