From qed-owner Sat Nov 6 13:08:32 1993 Received: by antares.mcs.anl.gov id AA07415 (5.65c/IDA-1.4.4 for qed-outgoing); Sat, 6 Nov 1993 13:03:07 -0600 Received: from scapa.cs.ualberta.ca by antares.mcs.anl.gov with SMTP id AA07408 (5.65c/IDA-1.4.4 for ); Sat, 6 Nov 1993 13:03:03 -0600 Received: from sedalia.cs.ualberta.ca by scapa.cs.ualberta.ca id <18440-2>; Sat, 6 Nov 1993 12:02:39 -0700 Subject: Mizar From: Piotr Rudnicki To: qed@mcs.anl.gov Date: Sat, 6 Nov 1993 12:02:29 -0700 X-Mailer: ELM [version 2.4 PL21] Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Length: 3054 Message-Id: <93Nov6.120239-0700.18440-2@scapa.cs.ualberta.ca> Sender: qed-owner Hi: Some info about the Mizar project is in my paper "An Overview of the Mizar Project" available via anonymous ftp from menaik.cs.ualberta.ca 129.128.4.241 in /pub/Mizar/Mizar_Over.tar.Z After uncompress and tar you get a directory Mizar_92BRA in which you find TeX source of the paper. There is no .dvi or .ps file. For more info you may write to: Roman Matuszewski Mizar Group Institute of Mathematics Warsaw University - Bialystok Branch 15-276 Bialystok Poland Roman will provide you with instructions how to get a copy of the system. If there is sufficient interest I will make all texts from the Mizar library available for anonymous ftp. The Mizar Group runs Mizar Digest as a moderated mailing list in BITNET. Everybody is welcome to join. Some fragments of the first issue of the Digest are attached below. I will be delighted to answer any questions. -- Piotr (Peter) Rudnicki =============================================================================== M M I ZZZZZ A RR DD I GGG EEEEE SSS TTTTT MM MM I Z AA R R D D I G E S T M M M M I Z A A R R D D I G GG EEE SS T M M M M I Z AAAA RRR D D I G G E S T M M M I ZZZZZ A A R R DDD I GGG EEEEE SSS T =============================================================================== 27 Jul 1993 Nr 1 moderator : L.Borys =============================================================================== Current Mizar ver. 4.05 Current MML ver. 4.05 We start to publish "Mizar Digest". It will be distributed to all users subscribed to MIZAR at PLEARN.BITNET. The obvious purpose is to provide an opportunity to discuss various topics related to Mizar. Particularly: - the changes introduced in new Mizar version; - the development of the MML: new articles and revisions; - planned changes in the Mizar language Please feel free to send to Digest any criticism related to Mizar (it will be published, if contains new arguments, of course), proposed development of the language, criticism of existing articles, the analyzes of the development of a particular field of mathematics in MML (done on needed) etc. We will provided a sort of user service. You are encouraged to send questions related to formalization in Mizar of definitions, theorems, or proofs. Also please inform u s if you run into troubles. We will try to help, to advice how to cope with the problem or to fix the Mizar bug. Mizar Digest will be distributed every week. To facilitate to keep track we decided to publish the issue even it we have nothing to publish. However such an issue will include steady information: current version of Mizar and current version of MML. Mizar Digest will be published in (scientific pidgin) English. The correspondence should be sent to MIZAR at PLBIAL11.BITNET. Moderator