online service for Mizar verification, HTMLization, and automated reasoning

Josef Urban <[email protected]>
Newsgroups gmane.comp.mathematics.mizar
Message-ID <[email protected]> 
Dear Mizar Users,

At http://mws.cs.ru.nl/~mptp/MizAR1096.html is now running an online
service for Mizar remote verification, HTMLization, and for using
automated reasoning tools on Mizar articles. The interface also allows
you to use parallel (SMP) processing on the server for article
verification and creation of HTML, which can on longer articles
significantly reduce the processing time.

The interface is also accessible through a new version of the Mizar
mode for Emacs (http://github.com/JUrban/mizarmode/raw/master/mizar.el),
using the functions in the "Remote solving" menu subgroup.

The link with automated reasoning tools is quite experimental, while
the verification, htmlization, and parallelization should work
reasonably well (and reports of serious bugs are welcome).

Josef Urban
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.