Mizar translation

[Lukasz Kaiser <kaiser@tenet.pl>]

Welcome.

I'm a mathematics studen from Wroclaw (Poland) and I'm interested in
translating Mizar articles to other languages.

I was trying to do translation from Mizar to the language of Larch Prover.
Since both this languages are similar and easy to understand, the most
difficult things about writing an translation program was to find the
concepts underlying Mizar. I had great problems with the first lines of
TARSKI.MIZ, since it is declared:

vocabulary EQUI_REL, FAM_OP;

and I could find no such files.
Another problem were cancelled theorems - :: as obvious is not obvious for
other program. Finally, since I had to translate only a litte I decided to
do it "by hand" using sed (String Editor) as help ( I attach a very
simple script example ).

I'm still interested in making automatic Mizar translation, so
please send me some information about your experience in this field. Since
I'm new in the mizar-forum, please give me information about proper links
if you have discussed this topic before.

Regards,

Lukasz Kaiser
(kaiser@tenet.pl)

/ î /s// \\in /g
/ iff /s// <=> /g
/ ex \(.\) st/s// \\E \1 (/g
/(*for \(.\) holds /s// \\A \1 (/g
/(*for \(.\) st \(.*\) holds /s// \\A \1 (\2 => /g
/(*for \(.\) st \(.*\) \\E /s// \\A \1 (\2 => \\E/g
/(*for \(.\) st \(.*\) \\A /s// \\A \1 (\2 => \\A/g
/(*for \(.\),\(.\) holds /s// \\A \1 \\A \2(/g
/(*for \(.\),\(.\),\(.\),\(.\) holds /s// \\A \1 \\A \2 \\A \3 \\A \4(/g
/ implies /s// => /g
/\&/s// \/\\ /g
/ c= /s// \\subseteq /g
/ or /s// \\\/ /g
/canceled;/s// /g
/theorem /s// assert /g
/::/s//%%/g
/definition /s//declare operators /g