Logistics

The work performed on the formalization of the CCL-book is the result of a team effort by researchers and students of the University of Biaystok with some contributions from members in Canada and Japan. In the summer of 1995, a seminar devoted to the theory of continuous lattices based on [25] and [30] covered the material to be formalized and in the spring of 1996 the actual work of formalization began. Grzegorz Bancerek volunteered to lead the CCL project from the beginning and has continued this leadership since. The list of all past and current participants comprises 16 authors listed below (in parentheses is the number of MIZAR articles (co)authored in the CCL project and in the entire MML by each author):

Grzegorz Bancerek (19, 90), Czesaw Bylinski (3, 36), Noboru Endou (2, 16), Adam Grabowski (4, 22), Ewa Gradzka (1, 2), Jarosaw Gryko (3, 6), Artur Korniowicz (11, 45), Beata Madras (1, 7), Agnieszka J. Marasik (1, 4), Robert Milewski (8, 25), Adam Naumowicz (3, 11), Piotr Rudnicki (3, 43), Yuji Sakai (1, 3) Bartomiej M. Skorulski (2, 4), Andrzej Trybulec (3, 86), Mariusz Zynel (2, 5).

The following rules were adopted at the outset of the project:

• The formalization will be divided into two series of MIZAR articles with identifiersEach MIZAR article has, besides a regular title, an identifier which is used when referring to it. Because of the DOS prehistory of the project, the names of MIZAR articles are limited to 8 characters and use the .MIZ extension. prefixed by:
  • YELLOW--articles bridging the gap between the contents of MML and the knowledge assumed in the CCL-book,
  • WAYBEL--articles formalizing the main course of the CCL-book.
• No formalization of examples and exercises will be done unless some item in the main text depends on it. This was meant to reduce the workload as none of the participants specialized in continuous lattices.
• The formalization should be as close as possible to the CCL-book, but provisions will be made for some MIZAR peculiarities such as built-in concepts and mechanisms, reuse of MML, and the like.
• Whenever possible, the formalization should be more general than the CCL-book.

The work of formalization started by assigning parts of the first two chapters, O. A Primer of Continuous Lattices and I. Lattice Theory of Continuous Lattices to individual team members. Because of the number of people involved, the work progressed in a different way than the usual sequential contributions of articles to MML. Usually, when an author is writing an article, it is not available to other authors until it is accepted to MML. We wanted to formalize different parts of the book simultaneously as sequential development would be too slow. We decided to maintain a local data base of the YELLOW and WAYBEL series to house completed and non-completed articles. This allowed for some parallelism in the development of articles. Articles from the local library were tested by new articles that used them and were revised as needed. After some time they were presented at a seminar to discuss possible methods of generalization and finally submitted to MML. The first articles YELLOW_0 and WAYBEL_0 were submitted to MML on September 10 and September 12 of 1996, respectively.

It would be difficult to define what constitutes a MIZAR article considered worthwhile for inclusion in MML. The final decision is with the Library Committee (currently A. Grabowski and A. Korniowicz), of the MIZAR User's Association which has a very liberal policy for accepting articles once they are verified by the MIZAR software. An article is stored as a text-file and on average has (with median value in parentheses): 1931 (1730) lines, 11,758 (10,435) tokens, 72.8 (62.2) kbytes, and contains 44.3 (37) theorems and 8.5 (6) definitions. Theorems and definitions in MML are technical terms and correspond to mathematical facts, no matter how simple or how deep.

The CCL-book contains 334 pages, divided into 8 chapters containing a total of 715 items. The weight of items varies considerably. On average, an article in the WAYBEL series covers 7 items, varying from 1 to 18 with a median of 5.

The formalization has been an effective stress test for the MIZAR software. It detected some errors in the software and forced the adjustment of a number of quantitative parameters. The formalization work would have not been possible without the cooperation of the system developers and the Library Committee who were responsible for improving the software and conducting a number of revisions of MML, see Section .