|
|
 |
| YAC Mizar Kit |
 |
Here is Eddie - an editor of
Mizar articles.
Eddie::MIZ
Version: 0.33
Date: 2008-04-01
Size: 551 kB
Contains the full version of the editor of Mizar articles.
License: freeware.
Use it, copy it, distribute it, promote it, etc. as much as you like.
Setup: unpack and use.
Running Mizar: the program uses the MIZFILES environment variable; if it's not defined, it assumes the standard location c:\Mizar.
Eddie::MSE
Version: 0.33
Date: 2008-04-01
Size: 579 kB
Contains the editor and checker of Mizar-MSE articles.
Also contains, as examples, two articles:- SETS.mse: "Boolean Properties of Sets", Michal Trybulec, 2007
The article contains the definition of the empty set and axioms that introduce elements of sets, set inclusion and the union of sets, and the intersection of sets. Next, several facts concerning the above mentioned relations are proved. Some of the theorems were taken from [1].
[1] Library Committee: "Boolean Properties of Sets - Theorems", Mizar Mathematical Library, 2002. - WAT.mse: "Axioms of Incidence", Wojciech Trybulec, 1988
This article is based on "Foundations of Geometry" by Karol Borsuk and Wanda Szmielew [1]. The fourth axiom of incidence is weakened. In [1] it has the form "for any plane there exist three non-collinear points in the plane" and in the article: "for any plane there exists one point in the plane". The original axiom is proved. The article includes: theorems concerning collinearity of points and coplanarity of points and lines, basic theorems concerning lines and planes, fundamental existence theorems, theorems concerning intersection of lines and planes.
[1] Karol Borsuk, Wanda Szmielew: "Foundations of Geometry", North Holland, 1960.
Article copyrights remain with their authors.
License for the program: freeware.
Use it, copy it, distribute it, promote it, etc. as much as you like.
Setup: unpack and use.
|
|
|
|
Download
