IMPROVING REPRESENTATION OF KNOWLEDGE WITHIN THE MIZAR LIBRARY

• Authors: Grabowski Adam , Schwarzweller Christoph
• Languages of publication: EN

Abstracts

EN

Efficient handling of extensive repositories is one of the major objectives of mathematical knowledge management. It is naturally connected, in order to attract more potential users (both researchers and students), with the need to build large libraries of formalized mathematics, and these two activities should not interfere. This may be achieved by constant enhancement of the quality of digital repositories, in which the proofs can additionally be verified with the help of proof assistants. Based on our experience with the MML we discuss some of the issues concerned with this process, describe mechanisms of revisions which seem to be indispensable to meet the expectations of contemporary mathematicians. We argue that even careful reviewing of contributions cannot cope with the task of keeping a mathematical repository efficient and clearly arranged in the long term.

Keywords

EN

MIZAR LIBRARY; REPOSITORY OF FORMAL MATHEMATICS; REVISIONS

Discipline

• LIBRARY_&_INFORMATION_SCIENCE: LIBRARY & INFORMATION SCIENCE

• Publisher: Sciendo
• Journal: Studies in Logic, Grammar and Rhetoric
• Year: 2009
• Issue: 18(31)
• Pages: 35-50
• Document type: ARTICLE

Contributors

author

Grabowski Adam

author

Schwarzweller Christoph

• Adam Grabowski, Institute of Mathematics, University of Bialystok, Akademicka 2, 15-267 Bialystok, Poland

Identifiers

CEJSH db identifier

11PLAAAA10163