«Abstract. One major goal of Mathematical Knowledge Management is building extensive repositories, in which the mathematical knowledge has been ...»
With no doubt, the assumption of the existence of a path not for arbitrary, but just for these two ﬁxed points is more general, the gains from stating every now and then that considered two points can be connected by a path, are at least doubtful. Similarly, we often write Abelian add-associative right_zeroed right_complementable RealLinearSpace-like (non empty RLSStruct) dropping an attribute or two to have slightly more general setting instead of using the mode RealLinearSpace which is equivalent to that complicated string above.
6 Related Work
Contemporary standards of the publishing process open some new possibilities – there are many journals online, Springer also announces his books/proceedings at their webpage. Paper-printed editions have some obvious limitations, vanishing for electronically stored and managed repositories of knowledge. We can notice, as an example, new functionalities of  in comparison to (even online) version of Abramowitz and Stegun .
Of course, what is published on paper, is ﬁxed. We can mind some reallife situations – rough sets as an example of obtaining new results via a kind of revision process (originally considered to be classes of abstraction with respect to some equivalnce relation, then some of its attributes were dropped to generalize the notion – see , ); also Robbins algebras and related axiomatizations of algebras are a good example, when a classical problem could be rewritten and reused when solved. In the aforementioned examples these were subjects for another papers, within the computerized repository the enhancement (the generalization of results) can be obtained via revision process.
As a rule, building an extensive encyclopedia of knowledge needs some investment; on the one hand, it can be considered by purely ﬁnancial means as “information wants to be free, people want to be paid” . That is the way Wolfram MathWorld  has been raised, as a collection closed in style, in fact authored by one person, Eric Weisstein.
But right after this service has been closed due to the court injunction, it soon appeared that the need to bridge this gap is that strong – many volunteers were working to develop a concurrent service to that of Wolfram’s, but of the more open type, based on the mechanism similar to Wiki.
The eﬀort of PlanetMath is now a kind of Wikipedia for mathematics (in fact they even cooperate closely); with its content somewhat questionable because virtually anyone can contribute, but frankly speaking, also nobody really asks about the veriﬁcation of other, even commercial resources. Although we believe the use of proof checkers could enable the automatic veriﬁcation of the proofs;
still the correctness of the deﬁnitions, i.e. how the encoded version reﬂect real mathematical objects, is under question only human can answer to a full extent.
But even in the projects of GNU type, people want to get their payment in another form: at least the added annotation such as “This article is owned by...”, as in PlanetMath, which can also be considered a kind of motivation to keep higher standards of the encyclopedia since the authorship is not fully anonymous.
In the MML the authorship is somewhat ﬁxed, there were however, especially recently, cases when the parts of submissions moved between them so that the authorship actually exchanged (as for example, with the formalization of the Zorn Lemma, originally created by Grzegorz Bancerek, and now, after the changes concerned with the move of this article to the concrete part, attributed to Wojciech Trybulec). In a sense, the Mizar library is much closer to PlanetMath, but the oﬃcial distributions are created by the Library Committee which decides about the acceptance of revisions.
To meet the expectations of researchers being potential users of repositories of mathematical knowledge, such collections cannot be frozen. The availability of the contemporary electronic media open new directions of the development of the new encyclopedias yet unavailable for their paper counterparts. The need of the enhancement stems not only of the fact there may be some obvious mistakes in the source; the reasons are far more complex.
In the paper, we tried to point out some of the issues connected with the mechanism of revisions performed on the Mizar Mathematical Library, large repository of computer-veriﬁed mathematical knowledge. The dependencies between its items and the environment declaration (notation and especially, constructors) are as of now too complex to freely move a single deﬁnition or a theorem between separate articles.
In our opinion, the current itemization of the MML into articles does not ﬁt the needs we expect from the feasible repository of mathematical facts; if we try to keep authors’ rights unchanged, there is an emerging need to have some other, smaller items which guarantee the developer’s authorship rights, a kind of ownership similar to that used in the PlanetMath project.
Also the better automation of the MML revision process is strongly desirable.
However possible, at least to some extent, but due to some diﬃculties which can be met as we pointed out, the human supervision of such automatic changes will probably always be needed.
We are grateful to Andrzej Trybulec and Artur Kornilowicz for their continuous cooperation on the enhancement of the MML. The ﬁrst author acknowledges the support of the EU FP6 IST grant TYPES (Types for Proofs and Programs) No.
510996. We acknowledge also anonymous referees for their useful suggestions, unfortunately due to space constraints not all of them were reﬂected in this ﬁnal version.
1. M. Abramowitz and I.A. Stegun, Handbook of Mathematical Functions; National Bureau of Standards, Applied Mathematics Series No. 55, U.S. Government Printing Oﬃce, Washington, DC, 1964, see also http://www.convertit.com/Go/ ConvertIt/Reference/AMS55.ASP.
2. A.A. Adams and J.H. Davenport, Copyright issues for MKM, in: A. Asperti, G.
Bancerek, and A. Trybulec (eds.), Proc. of MKM 2004, Lecture Notes in Computer Science 3119, pp. 1–16, 2004.
3. G. Bancerek, Information retrieval and rendering with MML Query; in: J.M. Borwein and W.M. Farmer (eds.), Proc. of MKM 2006, Lecture Notes in Artiﬁcial Intelligence 4108, pp. 65–80, 2006.
4. N.G. de Bruijn, The Mathematical Vernacular, A Language for Mathematics with typed sets; in: P. Dybjer et al. (eds.), Proc. of the Workshop on Programming Languages, Marstrand, Sweden, 1987.
5. J. H. Davenport, MKM from book to computer: A case study; in: A. Asperti, B. Buchberger, and J. Davenport (eds.), Proc. of MKM 2003, Lecture Notes in Computer Science 2594, pp. 17–29, 2003.
6. A. Grabowski, On the computer-assisted reasoning about rough sets; in: B. DuninK¸plicz et al. (eds.), Monitoring, Security, and Rescue Techniques in Multiagent e Systems, Advances in Soft Computing, Springer, pp. 215–226, 2005.
7. A. Grabowski and Ch. Schwarzweller, Rough Concept Analysis – theory development in the Mizar system; in: A. Asperti, G. Bancerek, and A. Trybulec (eds.), Proc. of MKM 2004, Lecture Notes in Computer Science 3119, pp. 130–144, 2004.
8. F. Kamareddine and R. Nederpelt, A Reﬁnement of de Bruijn’s Formal Language of Mathematics; Journal of Logic, Language and Information, 13(3), pp. 287–340, 2004.
9. R. Matuszewski and P. Rudnicki, Mizar: the ﬁrst 30 years; Mechanized Mathematics and Its Applications, 4(1), pp. 3–24, 2005.
10. B.R. Miller and A. Youssef, Technical aspects of the Digital Library of Mathematical Functions; Annals of Mathematics and Artiﬁcial Intelligence, 38, pp. 121–136, 2003.
11. The Mizar Homepage; http://www.mizar.org/.
12. A. Naumowicz and Cz. Byli´ski, Improving Mizar texts with properties and ren quirements; in: A. Asperti, G. Bancerek, and A. Trybulec (eds.), Proc. of MKM 2004, Lecture Notes in Computer Science 3119, pp. 190–301, 2004.
13. PlanetMath web page; http://planetmath.org/.
14. P. Rudnicki and A. Trybulec, Abian’s ﬁxed point theorem, Formalized Mathematics, 6(3), pp. 335–338, 1997.
15. P. Rudnicki and A. Trybulec, Mathematical Knowledge Management in Mizar; in:
B. Buchberger and O. Caprotti (eds.), Proc. of MKM 2001, Linz, Austria, 2001.
16. P. Rudnicki and A. Trybulec, On the integrity of a repository of formalized mathematics; in: A. Asperti, B. Buchberger, and J. Davenport (eds.), Proc. of MKM 2003, Lecture Notes in Computer Science 2594, pp. 162–174, 2003.
17. C. Sacerdoti Coen, From proof-asistants to distributed knowledge repositories: tips and pitfalls; in: A. Asperti, B. Buchberger, and J. Davenport (eds.), Proc. of MKM 2003, Lecture Notes in Computer Science 2594, pp. 30–44, 2003.
18. J. Urban, MoMM – fast interreduction and retrieval in large libraries of formalized mathematics, International Journal on Artiﬁcial Intelligence Tools, 15(1), pp. 109– 130, 2006.
19. Wolfram Mathworld web page; http://mathworld.wolfram.com/.