Full-text resources of CEJSH and other databases are now available in the new Library of Science.
Visit https://bibliotekanauki.pl

Results found: 2

first rewind previous Page / 1 next fast forward last

Search results

help Sort By:

help Limit search:
first rewind previous Page / 1 next fast forward last
1

THE CHINESE REMAINDER THEOREM, ITS PROOFS AND ITS GENERALIZATIONS IN MATHEMATICAL REPOSITORIES

100%
Schwarzweller C.
Studies in Logic, Grammar and Rhetoric
|
2009
|
issue 18(31)
103-119
EN
In the spirit of mathematical knowledge management theorems are proven with computer assistance to be included into mathematical repositories. In the mathematical literature one often finds not only different proofs for theorems, but also different versions or generalizations with a different background. In mathematical repositories, for obvious reasons, there is usually one version of a theorem with one proof only - the authors choose a version and a proof which can be formalized most easily. In this paper we argue that there are other issues to decide which proof of a theorem or which version of a theorem should be included in a repository. These basically depend on the intended further use of the theorem and the proof. We illustrate these issues in detail with the Chinese Remainder Theorem as an example.
2

IMPROVING REPRESENTATION OF KNOWLEDGE WITHIN THE MIZAR LIBRARY

63%
Grabowski A., Schwarzweller C.
Studies in Logic, Grammar and Rhetoric
|
2009
|
issue 18(31)
35-50
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.
first rewind previous Page / 1 next fast forward last
JavaScript is turned off in your web browser. Turn it on to take full advantage of this site, then refresh the page.