Mizar (software): Difference between revisions

From Citizendium
Jump to navigation Jump to search
imported>Peter Schmitt
(→‎Mizar libraries: no WP credit necessary -- the only sentence taken from WP has been rewritten)
imported>Meg Taylor
No edit summary
 
(21 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);
thus a program usually is named as <tt>something.miz</tt>.
thus a program usually is named as <tt>something.miz</tt>.


This program can be interpreted with command "<tt>mizf</tt>", for example,
This program can be interpreted with the command "<tt>mizf</tt>", for example,
  mizf something
  mizf something
or
or
  mizf something.miz
  mizf something.miz


A misar program is assumed to consist of lines.
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.
The interpreter checks the program line by line and, for each line, either accepts or rejects it.
Accepted lines are considered to be proven.
Accepted lines are considered to be proven.
Line 34: Line 31:
If all the lines are accepted, then all the theorems formulated in the program are considered
If all the lines are accepted, then all the theorems formulated in the program are considered
as proven.
as proven.
If the mizar program is not accepted as a whole, the lines
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.
marked as rejected have to be corrected and/or supplied with an additional proof.


== 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 programs.  
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
After a program has been reviewed and checked automatically, it can be published as an article in the associated
[[Journal of Formalized Mathematics]] <ref name="FM"> http://fm.mizar.org/ Journal of Formalized Mathematics</ref>.
[[Journal of Formalized Mathematics]] <ref name="FM"> http://fm.mizar.org/ Journal of Formalized Mathematics</ref>.


As of the beginning of 2010, the Mizar Mathematical Library (version 4.130.1076)  
As of the end of 2009, the Mizar Mathematical Library (version 4.130.1076)  
includes 1073 articles written by 226 authors,  
includes 1073 articles written by 226 authors,  
containing 49548 theorems, 9487 definitions, 785 schemes, 8973 registrations, 6831 symbols, and continues to grow.
containing 49548 theorems, 9487 definitions, 785 schemes, 8973 registrations, 6831 symbols, and continues to grow.


==Example of the mizar program==
== 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 (software)|Maple]].


The mizar libraries are built up on the base of extremely primitive mathematical objects
For any practical application, a lot of library definitions have to be loaded.
with minimum of predetermined notation. This is the main difference from the [[Mathematica]]
The search for the appropriate libraries with a compatible notation forms the most
or [[Maple software|Maple]].
exacting and difficult part of the job when writing a Mizar program.


For any practical application, a lot of library definitions should be loaded before.
In principle, a Mizar user may define all the symbols needed, using Mizar kernel notations,
The appropriate search for the appropriate libraries with compatible notations forms the most
but then problems of compatibility with the notations used by other Mizar programs
heavy and difficult part of the job in writing of any mizar program.
(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:


Here is an example of the mizar program that checks that 1+1=2 and 1/2-1/3=1/6:
  environ
  environ
  vocabularies ARYTM_1, RELAT_1, ARYTM_3, REAL_1;
  vocabularies ARYTM_1, RELAT_1, ARYTM_3, REAL_1;
Line 68: Line 70:
  1+1=2;
  1+1=2;
  1/2-1/3=1/6;
  1/2-1/3=1/6;
All the capital names refer to the libraries that are loaded at the installation of the
system. In order to be able to compare numbers more libraries should be found and listed at the
header of the program. In particular, an example of a program, that checks the relation 2>1
is not yet available.


In principle, the mizar user may define all the symbols necessary by him/her self using
All the uppercase names refer to a library that is loaded when the system is invoked to check the program.
the kernel mizar notations, but the problem of compatibility of notations with other mizar
 
programs (that already are written and uploaded) may arise; therefore the use of already
=== Order relation ===
written libraries is recommended.
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:
 
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 &ge; 2 " are accepted.
The last statement (" 2 &ge; 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.


Any source from the MML library can be considered as a complicated example of a mizar
===Some algebra===
program.
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
<math> x*y=y*x</math> and <math> x+x=2*x </math>, but rejects the relation
<math>x+y=x*y</math> because its value depends on values of the variables;
this expression has value '''true''' for <math>x=2</math>, <math>y=2</math>
and it has value '''false''' for <math>x=1</math>, <math>y=1</math>.
 
===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
<math>(x+y)^2 = x^2 + 2*x*y + y^2 </math>
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==
==References==
 
{{reflist}}
<references/>

Latest revision as of 00:39, 24 October 2013

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