|
|
 |
| YAC Mizar Kit |
 |
Here is Eddie - an editor of
Mizar articles.
Eddie::MIZ
Version: 0.34.a
Date: 2010-05-16
Size: 580 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.34.a
Date: 2010-05-16
Size: 612 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, the union, intersection, and difference 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.
Top
|
|
|
|
Download
