This HTML5 document contains 197 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dbpedia-dehttp://de.dbpedia.org/resource/
dctermshttp://purl.org/dc/terms/
yago-reshttp://yago-knowledge.org/resource/
dbohttp://dbpedia.org/ontology/
n22http://dbpedia.org/resource/File:
foafhttp://xmlns.com/foaf/0.1/
n15https://global.dbpedia.org/id/
yagohttp://dbpedia.org/class/yago/
schemahttp://schema.org/
dbthttp://dbpedia.org/resource/Template:
rdfshttp://www.w3.org/2000/01/rdf-schema#
freebasehttp://rdf.freebase.com/ns/
dbpedia-plhttp://pl.dbpedia.org/resource/
n17http://commons.wikimedia.org/wiki/Special:FilePath/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n8http://mizar.uwb.edu.pl/
owlhttp://www.w3.org/2002/07/owl#
dbpedia-ithttp://it.dbpedia.org/resource/
wikipedia-enhttp://en.wikipedia.org/wiki/
dbpedia-frhttp://fr.dbpedia.org/resource/
dbchttp://dbpedia.org/resource/Category:
dbphttp://dbpedia.org/property/
provhttp://www.w3.org/ns/prov#
xsdhhttp://www.w3.org/2001/XMLSchema#
wikidatahttp://www.wikidata.org/entity/
dbrhttp://dbpedia.org/resource/
dbpedia-jahttp://ja.dbpedia.org/resource/

Statements

Subject Item
dbr:Proof_assistant
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Rolle's_theorem
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Mizar_(disambiguation)
dbo:wikiPageWikiLink
dbr:Mizar_system
dbo:wikiPageDisambiguates
dbr:Mizar_system
Subject Item
dbr:Mizar_system
rdf:type
yago:SocialGroup107950920 yago:WikicatMathematicalSocieties yago:ArtificialLanguage106894544 yago:Work100575741 yago:WikicatProgrammingLanguages yago:Communication100033020 yago:YagoPermanentlyLocatedEntity yago:Language106282651 owl:Thing yago:WikicatLarge-scaleMathematicalFormalizationProjects yago:Abstraction100002137 yago:Undertaking100795720 dbo:HistoricBuilding wikidata:Q315 yago:PsychologicalFeature100023100 wikidata:Q9143 yago:Act100030358 yago:WikicatDependentlyTypedLanguages dbo:ProgrammingLanguage dbo:Language yago:Activity100407535 yago:Group100031264 yago:Event100029378 yago:ProgrammingLanguage106898352 yago:Society107966140 schema:Language
rdfs:label
Mizar (système) Mizar system System Mizar Mizar Mizar-System Sistema Mizar
rdfs:comment
自動証明検証システム Mizar(ミザー、ミザール)は、まったく厳密に形式的な形で数学的な定義や証明を記述するためのデータ記述言語(Mizar-言語)、実際にその言語で記述された証明の内容を検証することができる計算機プログラム(証明検証プログラム)、プログラムから参照して新たな証明の際に利用可能な定義と証明済みの定理からなるライブラリ (MML) の三者から構成される。 Mizar と同様の目的を持つプロジェクトに、のがある。 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. 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. 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. 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. 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.
foaf:name
Mizar
foaf:homepage
n8:
dbp:name
Mizar
foaf:depiction
n17:Mizar_MathWiki_screenshot.png n17:Mizar_system_logo.gif
foaf:page
n8:
dcterms:subject
dbc:Programming_languages_created_in_1973 dbc:Proof_assistants dbc:Educational_math_software dbc:Mathematical_societies dbc:Large-scale_mathematical_formalization_projects dbc:Pascal_(programming_language)_software dbc:Dependently_typed_languages
dbo:wikiPageID
209074
dbo:wikiPageRevisionID
1073792605
dbo:wikiPageWikiLink
dbr:Andrzej_Trybulec dbr:PDF dbc:Programming_languages_created_in_1973 dbr:Economics dbr:Hahn–Banach_theorem dbr:Static_typing dbr:Vernacular dbr:Natural_numbers dbr:Free_Pascal dbr:Isar_(Isabelle) dbc:Proof_assistants dbr:Journal_of_Formalized_Reasoning dbr:University_of_Alberta dbr:Wiki dbr:Classical_logic dbr:Brouwer_fixed_point_theorem dbr:Peer-review dbr:Gödel's_completeness_theorem dbr:Tarski–Grothendieck_set_theory dbr:Kőnig's_lemma dbr:Formal_language dbr:Białystok_University dbc:Educational_math_software dbr:Shinshu_University dbr:Coq dbr:Jordan_curve_theorem dbr:Declarative_programming dbc:Mathematical_societies dbr:Journal_of_Automated_Reasoning dbr:OMDoc dbr:Weak_typing dbr:Studies_in_Logic,_Grammar_and_Rhetoric dbr:Metamath dbc:Large-scale_mathematical_formalization_projects dbr:Proof_assistant n22:Mizar_system_logo.gif dbc:Pascal_(programming_language)_software dbr:ASCII dbr:Automath dbr:Implementation_of_mathematics_in_set_theory dbr:QED_manifesto dbc:Dependently_typed_languages dbr:Mathematical_formalization dbr:Probability_theory dbr:HOL_Light dbr:Interactive_Theorem_Proving dbr:Automated_proof_checking
dbo:wikiPageExternalLink
n8:
owl:sameAs
dbpedia-pl:System_Mizar dbpedia-fr:Mizar_(système) n15:aidc wikidata:Q1609529 dbpedia-ja:Mizar dbpedia-de:Mizar-System freebase:m.01dpvn yago-res:Mizar_system dbpedia-it:Sistema_Mizar
dbp:wikiPageUsesTemplate
dbt:Authority_control dbt:Reflist dbt:Infobox_programming_language dbt:For
dbo:thumbnail
n17:Mizar_system_logo.gif?width=300
dbp:designer
dbr:Andrzej_Trybulec
dbp:influenced
OMDoc, HOL Light and Coq mizar modes
dbp:influencedBy
dbr:Automath
dbp:logo
n22:Mizar_system_logo.gif
dbp:paradigm
dbr:Declarative_programming
dbp:released
1973
dbp:screenshot
Mizar MathWiki screenshot.png
dbp:typing
dbr:Static_typing dbr:Weak_typing
dbp:website
n8:
dbo:abstract
自動証明検証システム Mizar(ミザー、ミザール)は、まったく厳密に形式的な形で数学的な定義や証明を記述するためのデータ記述言語(Mizar-言語)、実際にその言語で記述された証明の内容を検証することができる計算機プログラム(証明検証プログラム)、プログラムから参照して新たな証明の際に利用可能な定義と証明済みの定理からなるライブラリ (MML) の三者から構成される。 Mizar と同様の目的を持つプロジェクトに、のがある。 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. 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. 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. 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. 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.
dbp:collapsible
yes
dbp:fileExt
.miz .voc
dbp:screenshotCaption
Mizar MathWiki screenshot
prov:wasDerivedFrom
wikipedia-en:Mizar_system?oldid=1073792605&ns=0
dbo:wikiPageLength
12463
dbo:designer
dbr:Andrzej_Trybulec
dbo:influenced
dbr:OMDoc dbr:Coq dbr:HOL_Light
dbo:influencedBy
dbr:Automath
foaf:isPrimaryTopicOf
wikipedia-en:Mizar_system
Subject Item
dbr:Jordan_curve_theorem
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Bertrand's_postulate
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:List_of_Polish_people
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:University_of_Alberta
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Interactive_Theorem_Proving_(conference)
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Kőnig's_lemma
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:List_of_mathematical_logic_topics
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Proof_of_Bertrand's_postulate
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Timeline_of_Polish_science_and_technology
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Tarski–Grothendieck_set_theory
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Fundamental_theorem_of_algebra
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Wedderburn's_little_theorem
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Andrzej_Grzegorczyk
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Andrzej_Trybulec
dbo:wikiPageWikiLink
dbr:Mizar_system
dbp:knownFor
dbr:Mizar_system
dbo:knownFor
dbr:Mizar_system
Subject Item
dbr:Zermelo–Fraenkel_set_theory
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Mutilated_chessboard_problem
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Automated_theorem_proving
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Type_theory
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Extreme_value_theorem
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:First-order_logic
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Hilbert's_basis_theorem
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Tietze_extension_theorem
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:QED_manifesto
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Reflection_principle
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Hahn–Banach_theorem
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Isabelle_(proof_assistant)
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Steinitz_exchange_lemma
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Chebyshev's_inequality
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Wilson's_theorem
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Automated_reasoning
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Automath
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Borel_set
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Intermediate_value_theorem
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Metamath
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Markov's_inequality
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Tychonoff's_theorem
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Well-ordering_theorem
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Event_(probability_theory)
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Urysohn's_lemma
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Yoneda_lemma
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Probability_axioms
dbo:wikiPageWikiLink
dbr:Mizar_system
Subject Item
dbr:Mizar_Language
dbo:wikiPageWikiLink
dbr:Mizar_system
dbo:wikiPageRedirects
dbr:Mizar_system
Subject Item
dbr:Mizar_Mathematical_Library
dbo:wikiPageWikiLink
dbr:Mizar_system
dbo:wikiPageRedirects
dbr:Mizar_system
Subject Item
dbr:Mizar_project
dbo:wikiPageWikiLink
dbr:Mizar_system
dbo:wikiPageRedirects
dbr:Mizar_system
Subject Item
wikipedia-en:Mizar_system
foaf:primaryTopic
dbr:Mizar_system