Mizar (software): Difference between revisions
imported>Peter Schmitt m (→Order relation: edit) |
imported>Peter Schmitt m (→Order relation: undo a changed word) |
||
| Line 81: | Line 81: | ||
=== Order relation === | === Order relation === | ||
In order to be able to compare numbers, even more libraries must be found and listed in the header of the program. However, the | In order to be able to compare numbers, even more libraries must be found and listed in the header of the program. However, the readers of the already existing programs could be used. Below, a Mizar program that checks | ||
the relations " −2 > 1 ", " 2 ≥ 2 " and " 2 ≥ 3 " is copypasted: | the relations " −2 > 1 ", " 2 ≥ 2 " and " 2 ≥ 3 " is copypasted: | ||
Revision as of 05:58, 2 February 2010
Mizar is a mathematical software system that includes a language for writing formalized definitions and proofs, and a high-level program that interprets the language and either accepts or rejects proofs, together with a library of definitions and already proved theorems which can be referenced and used in new proofs.
The Mizar software is available for free [1]; distributions for various operating systems can be downloaded.
History
The development of Mizar was started in 1973 as an attempt to emulate the natural language of mathematics from its very beginning, starting with the most basic mathematical objects. It was created by Andrzej Trybulec and is now maintained at Białystok University, Poland, the University of Alberta, Canada, and Shinshu University, Japan.
The language and its interpretation
Mizar programs are written as plain ASCII files. The standard extension "miz" is recommended (but not required); thus a program usually is named as something.miz.
This program can be interpreted with the command "mizf", for example,
mizf something
or
mizf something.miz
A Mizar program is assumed to consist of lines. The interpreter checks the program line by line and, for each line, either accepts or rejects it. Accepted lines are considered to be proven. Lines of the input file that are not accepted are marked by the software. If all the lines are accepted, then all the theorems formulated in the program are considered as proven. If the Mizar program is not accepted as a whole, the lines marked as rejected have to be corrected and/or supplied with an additional proof.
Mizar libraries
The Mizar Mathematical Library (MML), included in the distribution, consists of definitions and theorems which can be referred to in a newly written program. After a program has been reviewed and checked automatically, it can be published as an article in the associated Journal of Formalized Mathematics [2].
As of the end of 2009, the Mizar Mathematical Library (version 4.130.1076) includes 1073 articles written by 226 authors, containing 49548 theorems, 9487 definitions, 785 schemes, 8973 registrations, 6831 symbols, and continues to grow.
Examples of a Mizar program
The Mizar libraries are built upon a base of extremely primitive mathematical objects with a minimum of predetermined notation. This is a main difference to Mathematica and Maple.
For any practical application, a lot of library definitions have to be loaded. The search for the appropriate libraries with a compatible notation forms the most exacting and difficult part of the job when writing a Mizar program.
In principle, a Mizar user may define all the symbols needed, using Mizar kernel notations, but then problems of compatibility with the notations used by other Mizar programs (that already are written and uploaded) may arise in case the program is reused by other programs; therefore the use of existing libraries is recommended.
Sum of two rational numbers
Here is an example of a Mizar program that checks if " 1 + 1 = 2 " and " 1/2 - 1/3 = 1/6 " are true:
environ vocabularies ARYTM_1, RELAT_1, ARYTM_3, REAL_1; notations ORDINAL1, XCMPLX_0, XREAL_0, XXREAL_0; constructors NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0; registrations ORDINAL1,NUMBERS, XREAL_0; requirements BOOLE, SUBSET, NUMERALS,ARITHM; begin 1+1=2; 1/2-1/3=1/6;
All the uppercase names refer to a library that is loaded when the system is invoked to check the program.
Order relation
In order to be able to compare numbers, even more libraries must be found and listed in the header of the program. However, the readers of the already existing programs could be used. Below, a Mizar program that checks the relations " −2 > 1 ", " 2 ≥ 2 " and " 2 ≥ 3 " is copypasted:
environ
vocabularies NUMBERS, RELAT_2, RCOMP_1, SPPOL_1, SUBSET_1, EUCLID, TOPREAL1,
XXREAL_0, ARYTM_3, FINSEQ_1, JORDAN9, MATRIX_1, JORDAN8, PARTFUN1,
RELAT_1, TREES_1, GOBOARD1, GOBOARD5, ARYTM_1, CARD_1, XBOOLE_0, TARSKI,
RLTOPSP1, PSCOMP_1, NEWTON, MCART_1, PRE_TOPC, GOBOARD9, TOPS_1, REAL_1,
CONNSP_1, STRUCT_0, JORDAN2C, CONNSP_3, XXREAL_2, SETFAM_1, ZFMISC_1,
TOPREAL4, PCOMPS_1, WEIERSTR, METRIC_1, JORDAN10;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, NUMBERS, REAL_1, NAT_1, NAT_D,
PARTFUN1, FINSEQ_1, NEWTON, DOMAIN_1, STRUCT_0, METRIC_1, TBSP_1,
WEIERSTR, PRE_TOPC, TOPS_1, CONNSP_1, CONNSP_3, COMPTS_1, PCOMPS_1,
MATRIX_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD5, TOPREAL4,
PSCOMP_1, GOBOARD9, SPPOL_1, JORDAN2C, JORDAN8, GOBRD13, TOPREAL6,
JORDAN9, XXREAL_0;
constructors SETFAM_1, XXREAL_0, REAL_1, NAT_1, NEWTON, REALSET1, BINARITH,
TOPS_1, CONNSP_1, TBSP_1, TOPREAL4, JORDAN1, PSCOMP_1, WEIERSTR,
GOBOARD9, CONNSP_3, JORDAN2C, TOPREAL6, JORDAN8, GOBRD13, JORDAN9, NAT_D,
FUNCSDOM, CONVEX1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, XXREAL_0, MEMBERED, FINSEQ_1,
STRUCT_0, PRE_TOPC, COMPTS_1, PCOMPS_1, EUCLID, TOPREAL1, SPPOL_2,
SPRECT_1, SPRECT_2, JORDAN2C, TOPREAL6, JORDAN8, FUNCT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0, SUBSET_1, PSCOMP_1, CONNSP_3;
theorems CONNSP_1, CONNSP_3, EUCLID, GOBOARD6, GOBOARD7, GOBOARD9, GOBRD11,
GOBRD13, GOBRD14, JGRAPH_1, JORDAN2C, JORDAN3, JORDAN6, JORDAN8, JORDAN9,
NEWTON, NAT_1, PRE_TOPC, SETFAM_1, SPPOL_2, SPRECT_1, SPRECT_3, SPRECT_4,
SUBSET_1, TARSKI, TOPREAL1, TOPREAL3, TOPREAL4, TOPREAL6, TOPS_1,
WEIERSTR, ZFMISC_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, REALSET1, XREAL_1,
XXREAL_0, MATRIX_1, XREAL_0, COMPTS_1, RLTOPSP1;
schemes NAT_1;
begin :: Properties of the external approximation of Jordan's curve
registration
cluster connected compact non vertical non horizontal Subset of TOP-REAL 2;
existence
proof
take R^2-unit_square;
thus thesis;
end;
end;
2>1;
2>=2;
2>=3;
::> *4
::>
::> 4: This inference is not accepted
In the example above, the last statement (" 2 ≥ 3 ") is false. This is recognized by the program and shown in the three last lines after this statement that are added by Mizar; they indicate that this statement is not accepted.
Perhaps, namely for the comparison of numerical constants, the size of the header can be reduced. Generally, it is difficult to guess which libraries are required to prove some given set of statements.
References
- ↑ http://mizar.org/ Mizar Home Page
- ↑ http://fm.mizar.org/ Journal of Formalized Mathematics