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.