About: Mizar system

An Entity of Type: historic building, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

The Mizar system consists of a formal language for writing mathematical definitions and proofs, a proof assistant, which is able to mechanically check proofs written in this language, and a library of formalized mathematics, which can be used in the proof of new theorems. The system is maintained and developed by the Mizar Project, formerly under the direction of its founder Andrzej Trybulec. In 2009 the Mizar Mathematical Library was the largest coherent body of strictly formalized mathematics in existence.

Property Value
dbo:abstract
  • Das Mizar-System besteht aus einer formalen Sprache, um mathematische Definitionen und Beweise zu schreiben, einem Beweisassistenten, der in dieser Sprache erfasste Beweise mechanisch prüft, und einer Bibliothek formalisierter Mathematik, auf welche im Beweis neuer Theoreme zurückgegriffen werden kann. Das System wird vom Mizar Project, früher unter der Leitung seines Gründers Andrzej Trybulec, unterhalten und weiterentwickelt. Die Mizar Mathematical Library ist die weltweit größte Sammlung strikt formalisierter Mathematik. (de)
  • Le système Mizar est un outil fournissant un langage formel pour écrire des définitions et des preuves mathématiques, un assistant de preuve permettant une vérification automatique de ces preuves et une bibliothèque de mathématiques formalisées. (fr)
  • 自動証明検証システム Mizar(ミザー、ミザール)は、まったく厳密に形式的な形で数学的な定義や証明を記述するためのデータ記述言語(Mizar-言語)、実際にその言語で記述された証明の内容を検証することができる計算機プログラム(証明検証プログラム)、プログラムから参照して新たな証明の際に利用可能な定義と証明済みの定理からなるライブラリ (MML) の三者から構成される。 Mizar と同様の目的を持つプロジェクトに、のがある。 (ja)
  • The Mizar system consists of a formal language for writing mathematical definitions and proofs, a proof assistant, which is able to mechanically check proofs written in this language, and a library of formalized mathematics, which can be used in the proof of new theorems. The system is maintained and developed by the Mizar Project, formerly under the direction of its founder Andrzej Trybulec. In 2009 the Mizar Mathematical Library was the largest coherent body of strictly formalized mathematics in existence. (en)
  • Il sistema Mizar costituisce l'oggetto principale del . 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 , proposto da Bob Boyer nel 1993. (it)
  • 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 i Uniwersytecie Shinshū (Japonia). 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ą przeciętnie 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, OS X/Darwin. Kod źródłowy jest dostępny tylko dla członków stowarzyszenia . 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 i stają się częścią MML. MML jest zbudowane w oparciu o aksjomaty . Do chwili obecnej (kwiecień 2006) w bibliotece znalazło się 7900 definicji i 42 000 twierdzeń. Mimo iż semantycznie wszystkie obiekty MML 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 , a implementuje wyszukiwarkę MML. (pl)
dbo:designer
dbo:influenced
dbo:influencedBy
dbo:thumbnail
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 209074 (xsd:integer)
dbo:wikiPageLength
  • 12467 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 1020407480 (xsd:integer)
dbo:wikiPageWikiLink
dbp:collapsible
  • yes (en)
dbp:designer
dbp:fileExt
  • .miz .voc (en)
dbp:influenced
  • OMDoc, HOL Light and Coq mizar modes (en)
dbp:influencedBy
dbp:logo
dbp:name
  • Mizar (en)
dbp:paradigm
dbp:released
  • 1973 (xsd:integer)
dbp:screenshot
  • Mizar MathWiki screenshot.png (en)
dbp:screenshotCaption
  • Mizar MathWiki screenshot (en)
dbp:typing
dbp:website
dbp:wikiPageUsesTemplate
dct:subject
rdf:type
rdfs:comment
  • Das Mizar-System besteht aus einer formalen Sprache, um mathematische Definitionen und Beweise zu schreiben, einem Beweisassistenten, der in dieser Sprache erfasste Beweise mechanisch prüft, und einer Bibliothek formalisierter Mathematik, auf welche im Beweis neuer Theoreme zurückgegriffen werden kann. Das System wird vom Mizar Project, früher unter der Leitung seines Gründers Andrzej Trybulec, unterhalten und weiterentwickelt. Die Mizar Mathematical Library ist die weltweit größte Sammlung strikt formalisierter Mathematik. (de)
  • Le système Mizar est un outil fournissant un langage formel pour écrire des définitions et des preuves mathématiques, un assistant de preuve permettant une vérification automatique de ces preuves et une bibliothèque de mathématiques formalisées. (fr)
  • 自動証明検証システム Mizar(ミザー、ミザール)は、まったく厳密に形式的な形で数学的な定義や証明を記述するためのデータ記述言語(Mizar-言語)、実際にその言語で記述された証明の内容を検証することができる計算機プログラム(証明検証プログラム)、プログラムから参照して新たな証明の際に利用可能な定義と証明済みの定理からなるライブラリ (MML) の三者から構成される。 Mizar と同様の目的を持つプロジェクトに、のがある。 (ja)
  • The Mizar system consists of a formal language for writing mathematical definitions and proofs, a proof assistant, which is able to mechanically check proofs written in this language, and a library of formalized mathematics, which can be used in the proof of new theorems. The system is maintained and developed by the Mizar Project, formerly under the direction of its founder Andrzej Trybulec. In 2009 the Mizar Mathematical Library was the largest coherent body of strictly formalized mathematics in existence. (en)
  • Il sistema Mizar costituisce l'oggetto principale del . 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 , proposto da Bob Boyer nel 1993. (it)
  • 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 i Uniwersytecie Shinshū (Japonia). Abstrakty MML można przeglądać w , a implementuje wyszukiwarkę MML. (pl)
rdfs:label
  • Mizar-System (de)
  • Mizar system (en)
  • Mizar (système) (fr)
  • Sistema Mizar (it)
  • Mizar (ja)
  • System Mizar (pl)
owl:sameAs
prov:wasDerivedFrom
foaf:depiction
foaf:homepage
foaf:isPrimaryTopicOf
foaf:name
  • (en)
  • Mizar (en)
foaf:page
is dbo:knownFor of
is dbo:wikiPageDisambiguates of
is dbo:wikiPageRedirects of
is dbo:wikiPageWikiLink of
is dbp:knownFor of
is foaf:primaryTopic of
Powered by OpenLink Virtuoso    This material is Open Knowledge     W3C Semantic Web Technology     This material is Open Knowledge    Valid XHTML + RDFa
This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License