Post production(ID:2474/pos002)Emil Post production systemAlgorithmic facility, credited by Backus as giving him the means with which to create BNF Related languages
References: The idea that an automatic device should check our logical derivations is by no means new. It can be traced back not only to Pascal and Leibniz, but to Ramon Llull. In recent years, several projects have aimed at providing computer assistance for doing mathematics. Among the better known there are: AUTOMATH [4], EKL [10], QUIP [22], Nuprl [3], THEAX [14], Computational Logic [2], Ontic [11], and the more recent ones such as ALF, ELF, HOL, LEGO and many others (see [6, 7]). The speci c goals of these projects vary. However, they have one common feature: the human writes mathematical texts and the machine veri es their correctness. The project Mizar started almost 20 years ago under the leadership of Andrzej Trybulec at the Palock Scientific Society, Poland. Its original goal was to design and implement a software environment to assist the process of preparing mathematical papers. For lack of a better alternative, the project was based upon the style of doing mathematics used by the mathematicians of the so-called Polish mathematical school. Therefore, the project can be seen as an attempt to develop software environment for writing traditional mathematical papers, where classical logic and set theory form the basis of all future developments. The logical basis of the system is a "Polish" style of natural deduction. Only after years of using the logic has it been learned that it was the "composite system of logic" developed by Stanis law Jaskowski, see [8] and [12] for the English translation. Katuzi Ono, [16] described a similar system. Various formalizations of set theory have been tried (Zermelo-Fraenkel, Morse-Kelley) but Finally the Tarski-Grothendieck axiomatization has been adopted. Extract: History of Mizar A bit of history The name Mizar 1 was picked up in 1973 for a different project (a programming environment) that was discontinued, but its name has been recycled. The first experiments in 1974-75 developed a modest proof-checker for propositional logic. The main concern of A. Trybulec was the input language to the checker, and it turned out to be the main concern for all future years. The proof checker was based on a fixed set of inference rules. The justification of an inference in the input text required the user to state only the premises and the conclusion; the checker searched for a rule or a sequence of rules to validate an inference step. This approach was abandoned, and all future Mizar processors have used model checking. In 1977 the language and the checker were extended with quantifiers to form Mizar QC which had neither functional notation nor definitional facilities. These were added in subsequent years to form the Mizar FC system, which was used to record a number of larger texts. Among these texts was the initial segment of the book on arithmetics by Grzegorczyk [5]. The book is so rigorous and detailed (the Chinese remainder theorem comes as late as page 67 and its proof takes 6 pages) that the blow-up factor in the translation to Mizar FC was negligible. At around 1978-1979 the Mizar group started to grow substantially, being anchored at Warsaw University, Bialystok 2 Branch 3. In 1981, a language called Mizar 2 had been designed by A. Trybulec and implemented on an ICL 1900 by Cz. Bylinski, H. Oryszczyszyn, P. Rudnicki, and A. Trybulec. The system was written in Pascal and later ported to other computers (mainframe IBM and also to UNIX). Again, the stress was on the input language. The proof checker was rather weak which forced one to write very detailed proofs. The language included the following features: structured types, type hierarchy, comprehensive definitional facilities, built-in fragments of arithmetics, and a built-in variant of set theory. The translations into Mizar 2 included: a number of recent papers in topology, projective geometry, and some text-book algebra. In one of the experiments, the pigeon-hole principle was proven from scratch and compared with the similar development by van Benthem Jutting [28] in AUT-QE (the AUTOMATH project). The Mizar 2 text was about half as long as the AUT-QE text; however, Mizar 2 and AUT-QE were substantially different environments for conducting proofs (logic based vs type based). Among other works with Mizar 2, there were attempts to prove properties of programs [21] and software specifications [20]. In the following years, other Mizar languages and their implementations have been developed but their character was experimental (Mizar 3, Mizar HPF); the systems were not distributed outside the Mizar group in Bialystok, with one exception. A subset of Mizar, named Mizar MSE (short for Multi-Sorted with Equality) was imple- mented in 1982 by R. Matuszewski, P. Rudnicki, and A. Trybulec and has been widely used since then. The system is meant for teaching elementary logic with emphasis on the practical aspects of constructing proofs. The Mizar MSE language encompasses `raw' predicate calculus, multi- sorted with equality, but the language does not provide functional notation or special notation for definitions. There are numerous implementations of Mizar MSE, see [26, 25, 13, 19, 18, 15]. In 1986, Mizar 4 was implemented as a redesign of Mizar 2 and distributed to several dozen users. Each Mizar 4 article included a preliminaries part where the author could state some axioms that were not checked for validity. In 1988 the design of the language was completed by A. Trybulec and the final language is named simply Mizar. While articles in previous versions of the language must be self-contained, the final Mizar allows for cross-references among articles. Moreover, an author of a Mizar text is not allowed to introduce new axioms. Only the predefined axioms can be used, everything else must be proved. The two articles that are not checked for validity contain an axiomatics of the Tarski-Grothendieck set theory (see Appendix A) and definitional axioms of the built-in concepts and axioms of strong arithmetics of real numbers (see Appendix B). Recently, the main effort in the Mizar project has been in building the library of Mizar articles which now numbers almost 300. The development of Mizar has been driven by "experience, not only doctrine" (ENOD for short). In this case it meant that any idea that made sense was first of all implemented and tried by its proponent. However, only after other users approved the idea by actually using its implementation, was the idea included into the state of the project. The ENOD approach has been applied in the development of the Mizar processor, the input language (although it is almost exclusively of A. Trybulec's creation), and the Mizar library. |