[mizar] Re: ATP and presentation service for Mizar updated to MML 5.23.1213

[Josef Urban <josef.urban@gmail.com>]

Dear Mizar Users,

the ATP and presentation service for Mizar (MizAR) is now running on a
bigger server in Prague with more generous parallelization (about 60
different strategies run simultaneously) and time limits.

Please change/customize the value of the Emacs variable
ar4mizar-server to "http://grid01.ciirc.cvut.cz/";. The Mizar server in
Canada seems to be down at the moment.

The only MML version installed so far is 5.29.1227 .

Best,
Josef



On Sun, Jun 29, 2014 at 4:53 PM, Josef Urban <josef.urban@gmail.com> wrote:
> Dear Mizar Users,
>
> the ATP and presentation service for Mizar (MizAR) has now been
> updated to the latest Mizar/MML version 5.23.1213.
>
> As before, the recommended use is from Emacs. The main functions are:
>
> - pressing ";" directly after the "by" keyword calls ATP systems on
> the current proposition
> - pressing C-c h any time opens a HTML-ized version of the article in a browser
>
> The older video demonstrating the use is here:
> http://mws.cs.ru.nl/~urban/ams11/out4.ogv
>
> Common pitfalls:
>
> - If "by;" does not work at all, check that you are using one of the
> supported MML versions by looking at the available MML version values
> at http://mizar.cs.ualberta.ca/~mptp/MizAR.html (MML versions 1213 and
> 1147 are running the strongest ATP and recommending systems).
>
> - Check that the value of the Emacs variable mizar-atp-completion is
> "t" (this should be the default).
>
> - The value of the Emacs variable ar4mizar-server should be
> "http://mizar.cs.ualberta.ca/"; (Piotr is still helping your Mizaring
> from afar)
>
> - The normal response time should be between 10 - 30 seconds (each
> proof attempt now learns from some 60k MML proofs in several ways and
> considers some 150k formulas), depending on the size of your
> environment. If your article takes more than several seconds to
> verify, use the ::$P- and ::$P+ directives (formerly @proof) to switch
> off proof-checking of unnecessary parts.
>
> If things still don't work, let me know.
>
> More details about the service are here:
> http://dx.doi.org/10.1007/s10817-012-9269-y . Details of the latest
> strengthening done with very fast machine-learning systems with Cezary
> Kaliszyk is described here: http://arxiv.org/abs/1310.2805 .
>
> Best,
> Josef