Re: Extended ASCII in Mizar

[dahn@mathematik.hu-berlin.de (Bernd Ingo Dahn)]

I strongly support the view of Mariusz. The first thing we do in order to build a data base of Mizar articles is, to replace extended ASCII. Otherwise, reading and debugging is unnecessarily complicated. Our current translation table is (copied from our source code):

symbol_trans('Any',set) :- !.
symbol_trans('\356',in) :- !.
symbol_trans('\\',setminus) :- !.
symbol_trans('c=', subseteq) :- !.
symbol_trans('\362',geq) :- !.
symbol_trans('\363',leq) :- !.
symbol_trans('\215',varepsilon) :- !.
symbol_trans('\355',emptyset) :- !.
symbol_trans(bool,wp) :- !.
symbol_trans('\217',cap) :- !.
symbol_trans('\357',cap) :- !.
symbol_trans('U',cup) :- !.
symbol_trans(union,bigcup) :- !.
symbol_trans('\366','Delta') :- !.
symbol_trans('\367',approx) :- !.
symbol_trans('\370',f_img) :- !.
symbol_trans('\371',circ) :- !.
symbol_trans('.',at) :- !.
symbol_trans('"',inverse) :- !.
symbol_trans('[]',nil) :- !.
symbol_trans('\356-connected', in_connected) :- !.
symbol_trans('\356-transitive', in_transitive) :- !.
symbol_trans('\352', 'Omega') :- !.
symbol_trans(X,X).

As you may guess from the table, we are preferring LaTeX-style notation without the backslash. We are also experimenting with user requests to a Mizar database. This requires input of formulas. For this purpose extended ASCII cannot be easily used - at least in Unix. We also use LaTeX-style here.


Ingo Dahn

***************************************
* Bernd, Ingo Dahn		      *
*				      *
* Humboldt-University		      *
* Institute of Pure Mathematics       *
* Ziegelstr. 13a		      *
* D-10099 Berlin		      *
*				      *
* Phone: (+49)30-2093-1829	      *
* Fax  : (+49)30-2093-1846            *
* Mail : dahn@mathematik.hu-berlin.de *
*				      *
***************************************