About: XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
Description	Since version 7.2 the Mizar system produces quite detailed XML-based semantic description of Mizar articles during their verification. This format is now used natively for most of the processing done by Mizar, e.g., also for the whole Mizar internal database. The main motivation for switching to this XML-based representation is to make semantic communication with Mizar and presentation of the MML more accessible to a variety of external tools and systems. This article briefly describes this format and its current implementation, and shows examples of its usage. These examples include presentation of linked Mizar articles in modern XML-capable browsers like Mozilla, authoring assistance in the Mizar mode for Emacs, and experiments with XML-based querying languages like XQuery over the Mizar Mathematical Library loaded into a native XML databases like eXist. This work makes the currently largest repository of formal mathematics available to many kinds of data-mining, and reasoning applications etc. Since version 7.2 the Mizar system produces quite detailed XML-based semantic description of Mizar articles during their verification. This format is now used natively for most of the processing done by Mizar, e.g., also for the whole Mizar internal database. The main motivation for switching to this XML-based representation is to make semantic communication with Mizar and presentation of the MML more accessible to a variety of external tools and systems. This article briefly describes this format and its current implementation, and shows examples of its usage. These examples include presentation of linked Mizar articles in modern XML-capable browsers like Mozilla, authoring assistance in the Mizar mode for Emacs, and experiments with XML-based querying languages like XQuery over the Mizar Mathematical Library loaded into a native XML databases like eXist. This work makes the currently largest repository of formal mathematics available to many kinds of data-mining, and reasoning applications etc. (en)
Title	XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy (en)
skos:prefLabel	XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy (en)
skos:notation	RIV/00216208:11320/06:00206168!RIV10-MSM-11320___
http://linked.open...avai/riv/aktivita	Z
http://linked.open...avai/riv/aktivity	Z(MSM0021620838)
http://linked.open...vai/riv/dodaniDat	2010
http://linked.open...aciTvurceVysledku	Urban, Josef
http://linked.open.../riv/druhVysledku	D - Článek ve sborníku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	Univerzita Karlova v Praze / Matematicko-fyzikální fakulta
http://linked.open...dnocenehoVysledku	509164
http://linked.open...ai/riv/idVysledku	RIV/00216208:11320/06:00206168
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	XML-izing; Mizar; Making; Semantic; Processing; Presentation; Easy (en)
http://linked.open.../riv/klicoveSlovo	XML-izing Easy Semantic Making Presentation Processing Mizar
http://linked.open...ontrolniKodProRIV	[F10FC5849F75]
http://linked.open...v/mistoKonaniAkce	Berlin
http://linked.open...i/riv/mistoVydani	Berlin
http://linked.open...i/riv/nazevZdroje	Mathematical Knowledge Management
http://linked.open...in/vavai/riv/obor	BA
http://linked.open...ichTvurcuVysledku	1 (xsd:int)
http://linked.open...cetTvurcuVysledku	1 (xsd:int)
http://linked.open...UplatneniVysledku	2006
http://linked.open...iv/tvurceVysledku	Urban, Josef
http://linked.open...vavai/riv/typAkce	WRD - Světová
http://linked.open...ain/vavai/riv/wos	000236905900023
http://linked.open.../riv/zahajeniAkce	2006-01-01 (xsd:date)
http://linked.open...n/vavai/riv/zamer	Moderní metody, struktury a systémy informatiky
number of pages	15 (xsd:int)
http://purl.org/ne...btex#hasPublisher	Springer-Verlag
https://schema.org/isbn	978-3-540-31430-1
http://localhost/t...ganizacniJednotka	11320
is http://linked.open...avai/riv/vysledek of	XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy

Faceted Search & Find service v1.16.116 as of Feb 22 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3239 as of Feb 22 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 67 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software