WWW.THESIS.XLIBX.INFO
FREE ELECTRONIC LIBRARY - Thesis, documentation, books
 
<< HOME
CONTACTS



Pages:     | 1 | 2 ||

«Abstract. One major goal of Mathematical Knowledge Management is building extensive repositories, in which the mathematical knowledge has been ...»

-- [ Page 3 ] --

With no doubt, the assumption of the existence of a path not for arbitrary, but just for these two fixed 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 [10] in comparison to (even online) version of Abramowitz and Stegun [1].

Of course, what is published on paper, is fixed. 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 [6], [7]); 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 financial means as “information wants to be free, people want to be paid” [2]. That is the way Wolfram MathWorld [19] 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 effort 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 verification of other, even commercial resources. Although we believe the use of proof checkers could enable the automatic verification of the proofs;

still the correctness of the definitions, i.e. how the encoded version reflect 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 fixed, 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 official distributions are created by the Library Committee which decides about the acceptance of revisions.

7 Conclusions

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-verified 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 definition or a theorem between separate articles.

In our opinion, the current itemization of the MML into articles does not fit 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 difficulties which can be met as we pointed out, the human supervision of such automatic changes will probably always be needed.

Acknowledgments

We are grateful to Andrzej Trybulec and Artur Kornilowicz for their continuous cooperation on the enhancement of the MML. The first 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 reflected in this final version.

References

1. M. Abramowitz and I.A. Stegun, Handbook of Mathematical Functions; National Bureau of Standards, Applied Mathematics Series No. 55, U.S. Government Printing Office, 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 Artificial 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 Refinement 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 first 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 Artificial 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 fixed 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 Artificial Intelligence Tools, 15(1), pp. 109– 130, 2006.

19. Wolfram Mathworld web page; http://mathworld.wolfram.com/.



Pages:     | 1 | 2 ||


Similar works:

«School Newsletter AUTUMN TERM 2 2015-2016 Message from the Headteacher Welcome to our latest edition of the school newsletter which outlines key messages and information for parents regarding various aspects of school life. This communication is supplemented by the wealth of information that is available on the school website. It has been another excellent term at Belper School with many stepping up to the plate within and beyond lessons. Standards are high and students are engaging well with...»

«Research councils facing new science and technology The case of nanotechnology in Finland, the Netherlands, Norway and Switzerland Frank van der Most Graduation committee: Chair: prof.dr. P.J.J.M. van Loon Secretary: prof.dr. P.J.J.M. van Loon University of Twente Promoter: prof.dr. A. Rip University of Twente Assistant promoter: dr. B.J.R. van der Meulen Rathenau Institute Referent: prof.dr. M. Benner Lund University Members: prof.dr. S. Kuhlmann University of Twente prof.dr.ing. D.H.A. Blank...»

«Agrarische Rundschau, 04.05.2008 Weltagrarmärkte: Herausforderungen und Chancen für die EU Landwirtschaft1 Harald von Witzke Humboldt-Universität zu Berlin hvwitzke@agrar.hu-berlin.de http://www.agrar.hu-berlin.de/wisola/fg/ihe Der Beitrag basiert auf einem Vortrag des Verfassers auf der Wintertagung 2008 des Ökosozialen Forums in Wien. Weltagrarmärkte: Herausforderungen und Chancen für die EU Landwirtschaft Harald von Witzke, Humboldt-Universität zu Berlin Einige zentrale...»

«SUFFOLK COUNTY POLICE ATHLETIC LEAGUE JUNIOR FOOTBALL LEAGUE RULES & PROCEDURES OUR GREATEST RESOURCES OUR YOUTH SUFFOLK COUNTY P.A.L. JUNIOR FOOTBALL RULES TABLE OF CONTENTS REVISED 7/28/2011 SECTION 1 SCOPE SECTION 2 ELIGIBILITY SECTION 3 DETERMINATION OF AGE SECTION 4 GENERAL RULES SECTION 5 DIVISIONS SECTION 6 PLAYING/GROWTH WEIGHT SECTION 7 TEAM AND LEAGUE MAKE-UP SECTION 8 EQUIPMENT SECTION 9 PLAY OF THE GAME / BALL SIZES SECTION 10 PLAYING FIELD SECTION 11 SCORING VALUES / OFFICIAL TIME...»

«IBM Integration Bus Pattern Authoring Lab 5 User Customisation June, 2013 Hands-on lab built at product code level Version 9.0.0.0 IBM Integration Bus V9.0 Workshop June, 2013 1. INTRODUCTION USER CUSTOMISATION 2. CREATE THE MESSAGE FLOWS 3. CREATE THE PATTERN 4. INSTANTIATE THE PATTERN 5. CUSTOMISE THE MESSAGE FLOW 6. REGENERATE THE PATTERN INSTANCE 7. MODIFYING THE PATTERN CONFIGURATION 8. INSTANTIATE THE MODIFIED PATTERN 9. CUSTOMISE THE MESSAGE FLOW AGAIN 10. REGENERATE THE PATTERN INSTANCE...»

«1 Übersicht über den Editor Kurze Entstehungsgeschichte Tomb Raider war der Beginn einer sensationellen neuen Art von Spielen in der Tomb Raider-Perspektive. Die Fans waren nicht nur von Lara und ihren fantastischen Bewegungsmöglichkeiten begeistert, sondern auch von den stimmungsvollen und spannenden Hintergründen, vor denen ihre Abenteuer stattfanden. Alles begann im Jahr 1996, als Lara zum ersten Mal in irgendwelchen ägyptischen Ruinen herumstöberte. Jetzt, vier Jahre später,...»

«levensberichten en herdenkingen 2013 2013 KNAW © Sommige rechten zijn voorbehouden / Some rights reserved Voor deze uitgave zijn gebruiksrechten van toepassing zoals vastgelegd in de Creative Commons licentie. [Naamsvermelding 3.0 Nederland].Voor de volledige tekst van deze licentie zie http://www.creativecommons.org/ licenses/by/3.0/nl/ koninklijke nederlandse akademie van wetenschappen Postbus 19121, 1000 GC Amsterdam T 020 551 0700 F 020 620 4941 E knaw@knaw.nl www.knaw.nl pdf beschikbaar...»

«Local Authority Housing Statistics: 2011/12 Guidance notes for completion Local Authority Housing Statistics: 2011/12 Guidance notes for completion May 2012 Department for Communities and Local Government © Crown copyright, 2012 Copyright in the typographical arrangement rests with the Crown. You may re-use this information (not including logos) free of charge in any format or medium, under the terms of the Open Government Licence. To view this licence, visit...»

«Cooking For Change Foreclosureleads.com but Herbalife Market do the 8-10 famous employees of an smoke prospects in the income. Be to earn on you may if home explain your ones very to have by it is clearly Cooking for Change many to pay newcomers of benefit. On also, the system will identify more to be to contact to feel a website by this inflow. It need to move, another working solution whether you with its effort if your pangs even boiled they a generic client. Cooking for Change The process...»

«Movie-Induced Tourism An analytical report on how the Lord of the Rings trilogy has affected tourism in New Zealand Master Thesis conducted by Marleen Kraaijenzank Tourism, Aalborg University, July 2009 Title page Master program in Tourism 10th semester Aalborg University Supervisor: Robert Thomsen Hand-in: July 31st, 2009 Contains 172,706 characters = 71.9 pages This thesis was conducted by: Marleen Kraaijenzank Preface In today’s modern society, movies are a big part of the everyday life....»

«Reforming Investigative Interviewing in Canada Brent Snook Joseph Eastwood Michael Stinson John Tedeschini More Canadian Journal of Criminology and Criminal Justice, Volume 52, Number 2, April/avril 2010, pp. 215-229 (Article) Published by University of Toronto Press For additional information about this article http://muse.jhu.edu/journals/ccj/summary/v052/52.2.snook.html Access Provided by your local institution at 11/17/10 3:17PM GMT Reforming Investigative Interviewing in Canada Brent...»

«Program for the International Assessment of Adult P age |1 Competencies (PIAAC) International Data Explorer Help Guide Contents I. Background on the Program for the International Assessment of Adult Competencies (PIAAC) and the PIAAC International Data Explorer (IDE) II. Computer Requirements for the IDE III. General Overview IV. Steps to Explore Data 1. Select Criteria 1.A. Overview 1.B. Choose Subject 1.C. Choose Year/Study 1.D. Choose Measure 1.E. Choose Jurisdiction 2. Select Variables 2.A....»





 
<<  HOME   |    CONTACTS
2016 www.thesis.xlibx.info - Thesis, documentation, books

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.