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

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F06%3A00206168" target="_blank" >RIV/00216208:11320/06:00206168 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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 applic

Název v anglickém jazyce

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

Popis výsledku anglicky

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 applic

Druh

D - Stať ve sborníku

CEP obor

BA - Obecná matematika

OECD FORD obor

—

Projekt

—

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2006

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Mathematical Knowledge Management

ISBN

978-3-540-31430-1

ISSN

—

e-ISSN

—

Počet stran výsledku

15

Strana od-do

—

Název nakladatele

Springer

Místo vydání

Berlin

Místo konání akce

Berlin

Datum konání akce

1. 1. 2006

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000236905900023