[Date Prev][Date Next] [Chronological] [Thread] [Top]

[mizar] mizar parsing/text transformation service



Some new developments by the Mizar team for parsing and normalizing
Mizar texts are now available through an HTTP interface at 

  http://mizar.cs.ualberta.ca/parsing/

With one of the transformations ("Weakly Strict Mizar") one can in
principle write a simple parser for Mizar using, e.g., bison.  (Since
the set of arbitrary Mizar texts is syntactically rather complex, this
is an important normalization step.)  If one prefers a complete XML
parse tree, that is also available.

>From the new Mizar parsing site one can download a Perl script,
mizparse.pl, for parsing and transforming Mizar texts in these new
ways (the script simply prepares an HTTP message and sends it to the
HTTP service there).  Get it from:

  http://mizar.cs.ualberta.ca/parsing/mizparse.pl

Other allied utilities (e.g., pretty-printing) are under development.

If you have any questions, comments, or feature requests, I'm happy to
entertain them.

Enjoy,

Jesse

-- 
Jesse Alama
http://centria.di.fct.unl.pt/~alama/