Mizar (software): Difference between revisions

From Citizendium
Jump to navigation Jump to search
imported>Dmitrii Kouznetsov
(→‎Some algebra: elementary functions)
mNo edit summary
 
(3 intermediate revisions by 2 users not shown)
Line 1: Line 1:
{{subpages}}
{{subpages}}
'''Mizar''' is a mathematical software system that includes
'''Mizar''' is a mathematical software system that includes
a language for writing formalized definitions and [[proof (mathematics)|proofs]],
a language for writing formalized definitions and [[proof (mathematics)|proofs]],
Line 11: Line 10:


== History ==
== History ==
The development of Mizar was started in 1973 as an attempt to emulate the natural language of
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.
mathematics from its very beginning, starting with the most basic mathematical objects.
Line 18: Line 16:


== The language and its interpretation ==
== The language and its interpretation ==
Mizar programs are written as plain [[ASCII]] files.
Mizar programs are written as plain [[ASCII]] files.
The standard extension "<tt>miz</tt>" is recommended (but not required);
The standard extension "<tt>miz</tt>" is recommended (but not required);
Line 38: Line 35:


== Mizar libraries ==
== Mizar libraries ==
The Mizar Mathematical Library (MML), included in the distribution,
The Mizar Mathematical Library (MML), included in the distribution,
consists of definitions and theorems which can be referred to in a newly written program.  
consists of definitions and theorems which can be referred to in a newly written program.  
Line 49: Line 45:


== Examples of a Mizar program ==
== Examples of a Mizar program ==
The Mizar libraries are built upon a base of extremely primitive mathematical objects
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]]
with a minimum of predetermined notation. This is a main difference to [[Mathematica]]
Line 64: Line 59:


=== Sum of two rational numbers  ===
=== 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:
Here is an example of a Mizar program that checks if " 1 + 1 = 2 " and " 1/2 - 1/3 = 1/6 " are true:


Line 80: Line 74:


=== 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 readers of some already existing programs could be used. Below, a Mizar program that checks  
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 some already existing programs could be used. Below, a Mizar program that checks  
the relations "2 > 1", " 2 &ge; 2 " and " 2 &ge; 3 " is copypasted:
the relations "2 > 1", " 2 &ge; 2 " and " 2 &ge; 3 " is copypasted:
Line 159: Line 152:


===Elementary functions===
===Elementary functions===
The elementary functions can be searched in the libraries, and require the additional names to be listed in the header. With the same headers, the result of mizaring generates the errors,
The elementary functions can be searched in the libraries, and require the additional names to be listed in the header. With the same headers, the result of mizaring indicates the errors,
as in the example below. For example, the statement
as in the example below. For example, the statement
<math>(x+y)^2 = x^2 + 2*x*y + y^2 </math>
<math>(x+y)^2 = x^2 + 2*x*y + y^2 </math>
Line 186: Line 179:
  ::> 203: Unknown token, maybe an illegal character used in an identifier
  ::> 203: Unknown token, maybe an illegal character used in an identifier
although the operations ^, exp, sin and the numbers PI and number_e are listed in the table of notations.
although the operations ^, exp, sin and the numbers PI and number_e are listed in the table of notations.
==Bottle neck==
The bottle neck of the Mizar seems to be the search of the appropriate libraries. In a random way, it is difficult to find the correct combination of the names in the headers. The number of possible ordered combinations is of order of 1400!, that greatly exceeds the computer facilities.


==References==
==References==
 
{{reflist}}[[Category:Suggestion Bot Tag]]
<references/>
 
===Additional links===
 
http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/mizardictionary1.htm,
The dictionary of basic mathematical notations in Mizar
 
http://en.wikipedia.org/wiki/Mizar_system

Latest revision as of 11:00, 20 September 2024

This article is developing and not approved.
Main Article
Discussion
Related Articles  [?]
Bibliography  [?]
External Links  [?]
Citable Version  [?]
 
This editable Main Article is under development and subject to a disclaimer.

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 some 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 relations "2 > 1" and " 2 ≥ 2 " are accepted. 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.

Some algebra

With the same header, as in the example above, the elementary algebra can be verified. Below, the header is not copypasted (although it should exist at the top of the Mizar code), but few algebraic statements are added:

 2>1;
 2>=2;
 reserve x,y,z for Real;
 (x+y)*z=x*z+y*z;
 x*y=y*x;
 x+x=2*x;
 x+y=x*y;
::>    *4
::>
::> 4: This inference is not accepted

In order to specify, that the example deals with real, the special reservation is necessary. Then, the Mizar accepts the statements and , but rejects the relation because its value depends on values of the variables; this expression has value true for , and it has value false for , .

Elementary functions

The elementary functions can be searched in the libraries, and require the additional names to be listed in the header. With the same headers, the result of mizaring indicates the errors, as in the example below. For example, the statement will not be accepted, because the operation ^ is not yet defined. In this case, the error message will be different from that above:

 (x+y)^2=x^2+2*x*y+y^2
::>   *203
::>
::> 203: Unknown token, maybe an illegal character used in an identifier

In principle, the definition of operation ^ could be found among the supplied programs, but there are thousands there, and it is difficult to check them one by one.

The same refers to other functions, the SIN_COS and some other names should be listed; over-vice, the result may look as follows:

1^1=1;
::>,203
2 < number_e;
::>        *165
3< PI ;
::> *165
exp(0)=1;
::>,148
sin(0)=0;
::>,165
::>
::> 148: Unknown private functor
::> 165: Unknown functor format
::> 203: Unknown token, maybe an illegal character used in an identifier

although the operations ^, exp, sin and the numbers PI and number_e are listed in the table of notations.

Bottle neck

The bottle neck of the Mizar seems to be the search of the appropriate libraries. In a random way, it is difficult to find the correct combination of the names in the headers. The number of possible ordered combinations is of order of 1400!, that greatly exceeds the computer facilities.

References

  1. http://mizar.org/ Mizar Home Page
  2. http://fm.mizar.org/ Journal of Formalized Mathematics