Preface

We now present to our Readers the second Issue of mathematical papers which are abstracts of Mizar articles contributed to the Main Mizar Library (MML). They are being published in the order of their delivery to MML. The results obtained to date and concerned with that publication show that it is possible automatically to translate Mizar texts into a natural language. We have chosen English for that purpose. When comparing the quality of the translation in [2] with that in the present Issue we note that machine translation combined with automatic type-setting is possible. We treat our periodical as the first step towards the automated production of books: machine translation into natural language and automated type-setting.

The Reader may note in the texts certain peculiarities which result from the Mizar text. For instance, τ qua θ means a term which is equal to τ while its type is θ (the processor of PC Mizar checks whether the type ϑ(τ) of the term τ expands into θ). Mention is also due to the syntactic differences with respect to the articles published earlier: there are changes in the representation of certain formats. In the Mizar article we had originally UNION(X,Y) and INTERSECTION(X,Y). In [1] they are represented as (X, Y) and (X, Y), respectively, which was due to the processing sign by sign. In [2] we have, respectively, ⋃(X, Y) and ⋂(X, Y), whereas in [3], owing to the application of formats, we have X Y and X Y, respectively. Similar changes pertain to restriction, Cartesian product, and fraction line. The preferred set of symbols in the formats is that of AMS-TEX standard. The next issue is that of the representation of functions. In Mizar, one has carefully to distinguish the application of a functor (lingual function) F to x, represented by F.x. Newertheless both cases are recorded by us as: F(x) and F (x), respectively.

Our plans include a systematic improvement of translations into English: elimination of stylistic errors, increased variety of style, and the use of display mode during the TEXing.

Roman Matuszewski

References

[1] A Collection of TEXed Mizar Abstracts. Technical Report, University of Alberta, 1989.

[2] Formalized Mathematics: a computer assisted approach. Volume 1(1), Université Catholique de Louvain, January 1990.

[3] Formalized Mathematics: a computer assisted approach. Volume 1(2), Université Catholique de Louvain, March-April 1990.

256

Contents Form. Math. 1 (2)

Preface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 255

Continued on inside back cover