Newsgroups: fr.announce.seminaires
Distribution: fr
To: fr-sem@frmug.org
From: Didier.Remy@inria.COUPER-CECI.fr
Organization: INRIA-Rocquencourt
Subject: SEM - INRIA : Coq - 22/3/99 - Paris - FR

           http://pauillac.inria.fr/bin/calendar/Seminaires


                             S E M I N A I R E
       ____               ____                             ___                
      /    _   _         /     __     __  /_  _   /       /   |  _   __   _   
     /    / \ / \  ___  /     /  | / /_  /   __| /  ___  /___/  __| /  | __|  
    |___  |_/ |_/      |____ /    / __/ |_  |_/ |_      /      |_/ /    |_/   
               /                                                              
              /                                                               
                          I N R I A - Rocquencourt, 
                       Salle de conference du Bat 08

                            Lundi 22 mars, 10h30

                              ----------------
                              Trybulec Andrzej
                              ----------------

                          University of Bialystok

               =============================================
               The development of Mizar Mathematical Library
               =============================================

Since ten years the growth of MML (Mizar Mathematical Library) has
steady pace, approximately 50 kBytes per year (after compression).
However it is only superficial, because we started with very elementary 
articles, boolean propertiec of sets, relations, functions and so on, and now
most of the work is concetrated on more advanced topics: the proof of the
Jordan curve theorem, theory of abstract computers, theory of continuous
lattices. It seems that comparatively new Mizar constructions (attributes,
structures) are critical for keeping the development of MML. One has to
expoit better linguistic mechanisms, rather than logic.