FREE ELECTRONIC LIBRARY - Thesis, documentation, books

Pages:     | 1 || 3 |

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

-- [ Page 2 ] --

After the change of the loci type (the submission obtained grade D, of course) from FinSequence of REAL into real-yielding FinSequence in the EUCLID article the earlier definition was no longer needed which helped to simplify the structure of notions in this new submission.

The decision is not a typical result of majority voting, because referees giving C grade point out possible improvements, so usually the lowest grade counts (luckily, in case of E marks, all three referees agreed).

To summarize the grades for 2006, let us look at Table 1.

Table 1. Number of submissions to the MML and their grades in 2006

–  –  –

Basically, all ten submissions graded A and B were included into the MML, and among C and D candidate articles, which were returned to authors, other 15 were accepted; in total there were 25 Mizar articles accepted in 2006, the first year the reviewing procedure as described above was introduced.

All in all we have seen that reviewing MML submissions indeed addresses only the first point mentioned in Section 2. Of course a thorough reviewing process will improve the quality of MML articles and may even pilot authors into the direction of a good style of “Mizar writing”. As we can conclude from Table 1, this is the case of the majority of submissions because the authors should enhance the articles according to the referees’ suggestions. However there remain situations in which the MML as a whole should be improved; in the long term mere reviewing of submissions cannot avoid this. Here even carefully reviewing of Mizar articles – as already indicated by rate D above – can only help to detect the need for such revisions.

4 MML Enhancing The Library Committee has been established on November 11, 1989. Its main aim is to collect Mizar articles and to organize them into a repository – the MML.

Recently, from this agenda a new additional one was created – the Development Committee, which takes care of the quality of the library as a whole.

4.1 Types of Revisions For the reasons we tried to point out before, the Mizar Mathematical Library is

continuously revised. Roughly speaking, there are different kinds of revisions:

– an authored revision – consists of small changes in some articles in the library when somebody writing a new article notices a theorem or a definition in an old article that can be generalized. This is also the case of D grade as described above. To do this generalization, sometimes it is necessary to change (improve) some older articles that depend on the change. As a rule, a small part of the library is affected.

– an automatic revision – takes place frequently whenever either a new revision software is developed (e.g. software for checking equivalence of theorems, which enables to remove one or two equivalent theorems) or the Mizar verifier is strengthened and existing revision programs can use it to simplify articles.

– a reorganization of the library – although was very rare before, as of now it happens rather frequently. It consists in changing the order of processing articles when the Mizar data base is created. Its main steering force is the division of the MML into concrete and



4.2 MML Versions

Apart of the Mizar version numbering, the MML has also separate indexing scheme. As of the end of 2006, the latest official distribution of the MML has number 4.76.959.

As a rule, the last number, currently 959 shows how many articles are there in the library (this number can be sometimes different because 26 items were removed so far from the MML, but some additional items such as EMM articles, and “Addenda” which do not count as regular submissions, were added). The second number (76) changes if a bigger revision is finished and the version is made official. Although it is relatively small comparing with the age of the library, the changes are much more frequent.

4.3 Some Statistics

The policy of the head of Library Committee – to accept virtually all submissions from the developers and, if needed, enhance it by himself, was then very liberal. For these nearly twenty years there were only three persons taking a chair of a head of the Committee (Edmund Woronowicz, Czeslaw Byli´ ski, and curn rently Adam Grabowski); their decisions were usually consulted with the other members of the committee, though.

Such an openness of the repository was justified: in the early years of the Mizar project the policy “to travel to Bialystok and to get acquaintance with the system straight from its designer” resulted in the situation all authors knew each other personally, now the situation changed.

The MML evolved from the project, frankly speaking, considered rather an experiment of how to model mathematics to allow many users benefit from a kind of parallel development. Now, when the role of the library is to be much closer to the reality and the MML itself is just one among many mathematical repositories, the situation is significantly different.

–  –  –

As it can be seen, the first two years were extremely fruitful. No doubt, the first one was most influential, when the fundamentals, such as basic properties of sets, relations, and functions, the arithmetics, and vector spaces were established – to enumerate among many these most important. Some articles from that time were more or less straight translation from those written in older dialect of the Mizar language (Mizar PC, Mizar-2 etc., see [9]). Especially the subsequent year – 1990, when many authors could benefit from introducing the basics, hence they were able to work on various topics in parallel, brought into the Mizar Mathematical Library the bigest number of submissions so far (136 by year), then the number stabilized.

4.4 Towards Concrete and Abstract Mathematics As it was announced in 2001 [15], the MML will be gradually divided into two parts. As the library is based on the Tarski-Grothendieck set theory, the part devoted to the set theory (and related objects, as relations, functions, etc.) is indispensable. There is, however, huge amount of knowledge for which set theory is essential, but basing on the notion of structure by means of the Mizar language.

There are three parts of the Mizar Mathematical Library:

– concrete, which does not use the notion of structure (here of course comes standard set theory, relations, functions, arithmetic and so on);

– abstract, i.e. STRUCT_0 and its descendants, operating on the level of Mizar structures; both parts are not completely independent – here the concrete part is also reused (abstract algebra, general topology including the proof of the Jordan Curve Theorem, etc.);

– SCM, the part Random Access Turing Machines are modelled, i.e. mathematical model of a computer is described.

This division is reflected in the file mml.lar in the distribution in which is the order of processing of articles when creating Mizar data base is given – the “concrete” articles go first, at the end are those devoted to the SCM series. The process of separating these three parts is very stimulating for the quality of the Mizar library – many lemmas are better clustered as a result of this activity.

As of the beginning of 2007, the division can be summarized in Table 3.

–  –  –

Note that apart of the revisions suggested by the referees when giving Dgrades, any user can via TWiki mechanism suggest the change; he may of course also send improved version via email to the Library Committee; as an example, lemmas needed for the G¨del Completeness Theorem were reformulated to o provide its better understanding as a result of the external call.

4.5 Library Management As a first tool of collaborative work on the library we can enumerate Mizar TWiki (wiki.mizar.org) which gradually changes its profile from an experimental – and rarely used – forum into the place where suggestions/experiences with the MML can be described.

As the most important, and probably one of the better known MML tools, we can point out MML Query [3]. It has proven its feasibility when subsequent EMM items were created. Also researchers, when writing their Mizar articles, can find it useful. But usually, typical author does not care too much if his lemma which takes some ten lines of Mizar code is already present in the library.

Actually, searching for such auxiliary fact can take much more time than just proving it. This results in many repetitions in the library MML Query cannot cope with. And although the author can feel uncomfortable with multiple hits of the same fact, annotating such situations and reporting it to the MML developers is usually out of his focus.

This is the area where another tool comes in handy. Potentially very useful for the enhancement of the MML as a whole, MoMM (Most of Mizar Matches) developed by Josef Urban was primarily developed to serve as assistant during authoring Mizar articles [18]. It is a fast tool for fetching matching theorems, hence existing duplications can be detected and deleted from the MML (according to [18], more than two percent of main Mizar theorems is subsumed by the others). The work with the elimination of these lemmas is still to be done – many of detected repetitions are useful special cases so their automatic removal is at least questionable.

Another popular software, MML CVS – the usual concurrent version system for the MML was active for quite some time, but then was postponed because the changes were too cryptic for the reader due to the lack of proper marking of items. Actually, one of the most general problems is that there are no absolute names for MML items and the changes are usually too massive to find out what really matters.

5 Traps for the Developer Usually, the revision process via generalization of notions improves the MML.

There are some dangerous issues, however; we address some of them in this section.

5.1 Mind the Gap!

Let us cite an example from the article ABIAN [14]:

definition let i be Integer;

attr i is even means :: ABIAN:def 1 ex j being Integer st i = 2*j;


These are usual definitions of odd and even integer numbers.

definition let i be Integer;

attr i is odd means ex j being Integer st i = 2*j+1;


Then, among the others, the theorem stating that all integer numbers are either odd or even, was proven; the proof was very simple, but there was something in it to do, at least both definitions were involved.

theorem LEM:

for i being Integer holds i is odd or i is even;

However, after the revision (which was done by the author of ABIAN, after

all), the second definition got simplified as follows:

notation let i be Integer;

antonym i is odd for i is even;


Still, it seems perfectly correct, introducing antonym we obtain the law of excluded middle automatically, in a sense, and the proof of the above lemma labeled LEM was no longer necessary.

But we made a step too far, as it seems. Because in the definition of even number, the integer was not needed (remember the type Integer is a shorthand for integer number), it was dropped in both – definition of an attribute and its

antonym, and the latter got simplified into the form:

notation let i be number; antonym i is odd for i is even;end;

Unfortunately, e.g. number Pi (the Mizar symbol for the usual constant π) can be proven to be odd which can be considered really odd. Observe that any automation of the process of dropping assumption about the types of used loci in the definition of attributes, however possible, could be dangerous.

5.2 Permissive Definitions There are two unities for vector spaces defined in the MML – with symbol 1.

and 1_, and the following definitions:

definition let FS be multLoopStr;

func 1.FS - Element of FS equals :: VECTSP_1:def 9 the unity of FS;


definition let G be non empty HGrStr such that G is unital;

func 1_G - Element of G means :: GROUP_1:def 5 for h being Element of G holds h * it = h & it * h = h;


where multLoopStr is HGrStr enriched by an additional selector, namely unity and the adjective unital in the permissive assumption (after such that) assures that the proper neutral element exists.

At first glance, the earlier approach is better – the less complicated a type in a locus, the less problems we have to assure the required type. In the second definition however, the underlying structure has only two selectors instead of three.

5.3 Meaningless Predicates

Suppose we have the following:

definition let a,b be natural number;

assume a 0;

pred a divides b means ex x being natural number st b = a * x;


Well, we can freely delete the assumption, in Mizar predicate definitions do not require any correctness conditions proven. But, if we forget for a while that within the MML division by zero is defined, does it make any mathematical sense for any pair of natural numbers? According to the current policy of the Library Committee, we allow for any such underspecification.

5.4 Apparent Generalizations

There are sometimes cases the price for the revision is too high comparing to gains or the enhancing is apparent. If we remind that pathwise connectedness of the topological space T denotes the existence of a function from the unit interval into T which has the values a and b in 0 and 1, respectively, for any pair of points a, b of T, a path between two points is just an underlying mapping, if it exists.

It is enough however to have an assumption about the existence of appropriate function for just the pair of points currently under considerations.

definition let T be TopStruct; let a, b be Point of T;

assume a, b are_connected;

mode Path of a, b - Function of I[01], T means :: BORSUK_2:def 2 it is continuous & it.0 = a & it.1 = b;


Pages:     | 1 || 3 |

Similar works:

«Our ref: GS/Geog/UL/2004 09 December 2004 To: SQA Co-ordinator Directors of Education For the attention of all staff responsible for the delivery of National Qualifications in Geography Greg Storey at Glasgow Action by Recipient Direct Line: 0141-242 2331 Response required E-mail: greg.storey@sqa.org.uk Note and pass on None — update/information only Dear Colleague National Qualifications Update — Geography This briefing note is intended to offer practical advice and support on the issues...»

«ACCOUNTING FOR GOODWILL: A CRITICAL EVALUATION by MAYNARD JACOBUS VAN DER MERWE Submitted in fulfilment of the requirements for the degree of MASTER OF ACCOUNTING SCIENCE in the Department of APPLIED ACCOUNTANCY at the UNIVERSITY OF SOUTH AFRICA SUPERVISOR: PROF M A FAUL JUNE 1996 The financial assistance of the Centre for Science Development (HSRC, South Africa) towards this research is hereby acknowledged. Opinions expressed and conclusions arrived at, are those of the author and are not...»

«Objective List of German and Austrian Scientists. (1,600 “Scientists”) Joint Intelligence Objectives Agency. 2 January 1947. Name and Address Field Dr. Udo Adelsburger Crystal clocks & H. F. Heidelberg measurements Heinrich Adenstedt Jet Engines Remscheidt, Brunswick Prof. Dr. Arnold Agatz Marine Engineer Berlin-Zehlendorf West Hans Knirschweg 13 Dipl. Ing. Ahrens Tech. Designer of Stuttgart/Sindelfingen (AZ) Automobile bodies Gerhard E Aichinger Parachutes Wright Field, Ohio Dr. Leonard...»

«Statement of Qualifications PO Box 4027 Englewood, Colorado 80155-4027 Tel. (303) 267-0791 Fax (720) 529-9057 www.wileyconsulting.net P. O. Box 4027 Englewood, CO 80155-4027 Phone (303) 267-0791 Fax (720) 529-9057 MINING CONSULTANTS Wiley Consulting, LLC formerly Wiley Engineering, Inc. has committed the last 27 years to serving clients with high professional ethics. We draw upon our rich background of engineering and management skills to serve our clients needs with dedication and persistence....»

«Disclaimer The Massachusetts Department of Environmental Protection (MassDEP) provides this file for download from its Web site for the convenience of users only. Please be aware that the OFFICIAL versions of all state statutes and regulations (and many of the MassDEP policies) are only available through the State Bookstore or from the Secretary of State’s Code of Massachusetts Regulations (CMR) Subscription Service. When downloading regulations and policies from the MassDEP Web site, the...»

«2014 FACT SHEET We’re all in the position to make a difference in the life of someone desperately in need. Organizational Background Altruism: leading an ethical life involves using a portion of personal wealth We spread awareness of what we can all do to end poverty, and we offer our community resources such as a list of highly effective recommended charities to help them make a meaningful difference. TLYCS aims to mass market not only outstanding charities, but also the underlying beliefs...»

«IAEA-TECDOC-1086 XA9951070 Technologies for remediation of radioactively contaminated sites INTERNATIONAL ATOMIC ENERGY AGENCY June 1999 30-31 J The originating Section of this publication in the IAEA was: Waste Technology Section International Atomic Energy Agency Wagramer Strasse 5 P.O. Box 100 A-1400 Vienna, Austria The IAEA does not normally maintain stocks of reports in this series. However, copies of these reports on microfiche or in electronic form can be obtained from INIS Clearinghouse...»

«CHINA 1.0 CHINA 2.0 CHINA 3.0 Herausgegeben von Mark Leonard Mit einer neuen Einleitung für die deutsche Ausgabe und einem Nachwort von François Godement und Jonas Parello-Plesner †BER ECFR DAS CHINA-PROGRAMM DES ECFR Der European Council on Foreign Relations Ziel des China-Programms des ECFR ist die (ECFR) wurde im Oktober 2007 als erster panEntwicklung einer intelligenteren europäischen europäischer Think Tank gegründet. Sein Ziel Strategie gegenüber China. Hierzu werden ist die...»

«Neural Computation, submitted. Learning Intermediate-Level Representations of Form and Motion from Natural Movies Charles F. Cadieu and Bruno A. Olshausen Redwood Center for Theoretical Neuroscience, Helen Wills Neuroscience Institute, University of California, Berkeley, Berkeley, CA, USA Keywords: Intermediate visual processing; unsupervised learning; computational vision; natural scenes; image statistics; motion processing; form processing; invariance Abstract We present a model of...»

«Appendix C. Interviewer CAPI program NatCen Program Documentation Interviewer Schedule This ‘paper version of the program’ has been created to indicate the wording and content of the interviewer questionnaire. Diet and Nutrition Survey of Infants and Young Children, 2011 Contents: PART 1: Interviewer Schedule BACKGROUND AND DEMOGRAPHICS: HOUSEHOLD GRID YOUR BABY BREASTFEEDING/ WEANING PRACTICES EATING PATTERNS DEVELOPMENTAL STAGES DIETARY SUPPLEMENTS AND MEDICATIONS CURRENTLY TAKEN BY...»

«Field Mentor Transfer of Learning 2013 – CAT Slides and Script Slide 1 Welcome Audio Script: Welcome to Transfer of Learning training for Field Mentors and Supervisors. Page 1 of 29 Field Mentor Transfer of Learning 2013 – CAT Slides and Script Slide 2 Field Mentor Program Audio Script: The DCS Field Mentor Program was developed to help new workers reinforce classroom learning with practice in real life situations by completing on the job training work alongside a designated Field Mentor....»

«Housing Australia factsheet A quick guide to housing facts and figures Housing stress 2 In 2009–10, 60% of lower-income rental households in Australia were in rental stress Homeownership 3 In 2010–11, only 5.2% of homes sold or built nationally were affordable for low-income households Private rental 6 In 2009–10, there was a shortage of 539,000 private rental dwellings that were both affordable and available for renters with gross incomes in the bottom 40% of income distribution Social...»

<<  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.