[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] Mizar remote services updated
- To: mizar-forum <mizar-forum@mizar.uwb.edu.pl>
- Subject: [mizar] Mizar remote services updated
- From: Josef Urban <josef.urban@gmail.com>
- Date: Sun, 27 Mar 2011 10:06:24 +0200
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=RkfPjGVBQNIJC5JbzGYI8xFFO0q8Lq87/2fKCj2uSdLmOY6phBNhRytutJoUmGEjMK sx3go95ZGmGhngfQ3u3oA5S/xAH6cCQvrca/y4KX+1M9jXmiv0yPjoUTesmnUYiZsgU3 TNyjtAyGPXDnPdtXUMs4ixVQfFbodXryfV+XA=
Dear Mizar users,
the Mizar remote verification/solving/presentation service at
http://mws.cs.ru.nl/~mptp/MizAR.html has now been updated to
include the latest MML version 4.160.1126, and installed also on
a new (faster) server at the University of Alberta:
http://mizar.cs.ualberta.ca/~mptp/MizAR.html . The version update
mechanism has been almost completely scripted, so new versions of
the service should be available automatically with new MML
versions.
An updated Mizar mode for Emacs is available at
https://github.com/JUrban/mizarmode/raw/master/mizar.el . This
now allows to customize the remote server, and switch on the use
of "by;" to trigger asynchronous ATP solving (see
http://mws.cs.ru.nl/~urban/ams11/out4.ogv for a demo).
Note that the ATP proofs now by default display also "implicit"
parts of Mizar reasoning, for example registrations. They are
written in the MMLQuery syntax, like : AFINSQ_1:exreg 2 (condreg
2, funcreg 2). If you need to look them up, just go to the
corresponding URL on mizar.org, e.g,
http://mizar.org/version/current/html/afinsq_1.html#RC2 (CC2,
FC2).
Best regards,
Josef Urban