|
|
 |
| YAC Mizar Kit |
 |
Oto edytor artykułów mizarowych -
Eddie.
Eddie::MIZ
Wersja: 0.34.a
Data: 2010-05-16
Wielkość: 580 kB
Zawiera wersję pełną edytora artykułów mizarowych.
Licencja: freeware (w sensie darmowa).
Proszę używać, kopiować, rozpowszechniać, promować, itd. ile wlezie.
Instalacja: rozpakować i używać.
Uruchamianie Mizara: program korzysta z definicji środowiskowej MIZFILES;
jeżeli ta nie została określona, zakłada standardową lokalizację c:\Mizar.
Eddie::MSE
Wersja: 0.34.a
Data: 2010-05-16
Wielkość: 612 kB
Zawiera edytor i checker artykułów systemu Mizar-MSE.
Zawiera także, jako przykład, dwa artykuły:
- SETS.mse: "Boole'owskie właściwości zbiorów", Michał Trybulec, 2007
Artykuł zawiera definicje zbioru pustego i aksjomaty opisujące
należenie do zbiorów, zawieranie zbiorów, sumę, iloczyn i różnicę zbiorów.
Następnie przeprowadzone są dowody kilkunastu faktów dotyczących
wyżej wymienionych relacji. Część twierdzeń zaczerpniętych została z [1].
[1] Library Committee: "Boolean Properties of Sets - Theorems",
Mizar Mathematical Library, 2002.
- WAT.mse: "Axioms of Incidence", Wojciech Trybulec, 1988
Artykuł oparty jest na "Podstawach geometrii" ("Foundations of Geometry")
Karola Borsuka i Wandy Szmielew [1]. Czwarty aksjomat incydencji
został osłabiony. W [1] brzmi "na każdej płaszczyźnie
istnieją trzy niewspółliniowe punkty",
w artykule natomiast: "na każdej płaszczyźnie istnieje co najmniej jeden punkt".
Oryginalny aksjomat jest udowodniony. Artykuł zawiera:
twierdzenia dotyczące współliniowości punktów oraz
współpłaszyzności punktów i prostych, podstawowe twierdzenia dotyczące
prostych i płaszczyzn, fundamentalne twierdzenia o istnieniu, twierdzenia
dotyczące przecinania się prostych i płaszczyzn.
[1] Karol Borsuk, Wanda Szmielew: "Foundations of Geometry", North Holland, 1960.
Prawa autorskie do artykułów pozostają przy autorach.
Licencja na program: freeware (w sensie darmowa).
Proszę używać, kopiować, rozpowszechniać, promować, itd. ile wlezie.
Instalacja: rozpakować i używać.
Góra
|
|
|
|
Pobierz
