| dbpprop:abstract
|
- The Mizar system consists of a language for writing strictly formalized mathematical definitions and proofs, a computer program which is able to check proofs written in this language, and a library of definitions and proved theorems which can be referenced and used in new articles. Mizar has goals similar to those of the QED project proposed by Bob Boyer around 1993.
- Il Sistema Mizar costituisce l'oggetto principale del Progetto Mizar. Consiste di un linguaggio per la scrittura formalizzata di definizione e dimostrazioni matematiche, un programma per computer capace di verificare dimostrazioni scritte in questo linguaggio e una libreria di definizioni e teoremi già dimostrati. Il Progetto Mizar ha preso vita nel 1973. È portato avanti da Andrzej Trybulec (fondatore) e dalle università di Białystok (Polonia), Alberta (Canada) e Shinshu (Giappone). I suoi obiettivi sono simili a quelli del Progetto QED, proposto da Bob Boyer nel 1993.
- 自動証明検証システム Mizar（ミザー、ミザール）は、まったく厳密に形式的な形で数学的な定義や証明を記述するためのデータ記述言語（Mizar-言語）、実際にその言語で記述された証明の内容を検証することができる計算機プログラム（証明検証プログラム）、プログラムから参照して新たな証明の際に利用可能な定義と証明済みの定理からなるライブラリ（MML）の三者から構成される。 Mizar と同様の目的を持つプロジェクトに、ロバート・ボイヤーのQEDプロジェクトがある。
- System Mizar - system automatycznego dowodzenia twierdzeń i tworzenia prac matematycznych, składający się z: języka definiowania sformalizowanych matematycznych definicji i dowodów, aplikacji komputerowej, zdolnej do sprawdzania dowodów zapisanych w tym języku, biblioteki definicji i udowodnionych twierdzeń, do których można się odwoływać i używać w nowych pracach. Budowę systemu rozpoczął w 1973 Andrzej Trybulec. Obecnie jest rozwijany na Uniwersytecie w Białymstoku, Uniwersytecie Alberty i Uniwersytecie Shinshu. Prace Mizar są pisane w zwykłym ASCII. Język Mizar jest na tyle zbliżony do zwykłych zapisów matematycznych, że matematycy uczą się go niemal natychmiast. Mizar uzasadnia wszystkie kroki dowodu, co sprawia, że jego artykuły są ok. 4 razy dłuższe niż analogiczne prace matematyczne pisane przez człowieka. System dowodzenia twierdzeń używa logiki klasycznej, jest napisany w Pascalu i może być ściągnięty z sieci i używany za darmo do niekomercyjnych celów. Pracuje na platformach Windows, Solaris, FreeBSD, Linux, Mac OS X/Darwin. Kod źródłowy jest dostępny tylko dla członków grupy Association of Mizar Users. Dystrybucja Mizara zawiera Mizar Mathematical Library (MML), bibliotekę zawierającą definicje, twierdzenia i dowody matematyczne do których odwołują się nowe artykuły. Propozycje na dodatki do tej biblioteki, po recenzji i automatycznym sprawdzeniu, są publikowane w Journal of Formalized Mathematics i stają się częścią MML. MML jest zbudowane w oparciu o aksjomaty teorii mnogości Tarskiego-Grothendiecka. Do chwili obecnej (kwiecień 2006) w bibliotece znalazło się 7900 definicji i 42000 twierdzeń (aktualny stan jest tutaj). Mimo iż semantycznie wszystkie obiekty MML-a są zbiorami, język pozwala na definiowanie i używanie nowych typów składniowych: np. zmienna może być zdefiniowana jako Nat, jeśli oznacza liczbę naturalną, albo Group, jeśli oznacza grupę. Sprawia to, że notacja staje się wygodniejsza i bardziej zbliżona do matematycznego sensu danego zapisu. Abstrakty MML można przeglądać w Journal of Formalized Mathematics, a MML Query implementuje wyszukiwarkę MML-a.
|
| rdfs:comment
|
- The Mizar system consists of a language for writing strictly formalized mathematical definitions and proofs, a computer program which is able to check proofs written in this language, and a library of definitions and proved theorems which can be referenced and used in new articles. Mizar has goals similar to those of the QED project proposed by Bob Boyer around 1993.
- Il Sistema Mizar costituisce l'oggetto principale del Progetto Mizar. Consiste di un linguaggio per la scrittura formalizzata di definizione e dimostrazioni matematiche, un programma per computer capace di verificare dimostrazioni scritte in questo linguaggio e una libreria di definizioni e teoremi già dimostrati. Il Progetto Mizar ha preso vita nel 1973. È portato avanti da Andrzej Trybulec (fondatore) e dalle università di Białystok (Polonia), Alberta (Canada) e Shinshu (Giappone).
- System Mizar - system automatycznego dowodzenia twierdzeń i tworzenia prac matematycznych, składający się z: języka definiowania sformalizowanych matematycznych definicji i dowodów, aplikacji komputerowej, zdolnej do sprawdzania dowodów zapisanych w tym języku, biblioteki definicji i udowodnionych twierdzeń, do których można się odwoływać i używać w nowych pracach. Budowę systemu rozpoczął w 1973 Andrzej Trybulec.
|
![[RDF Data]](/statics/sw-cube.png)
