Integrované sémantické brouzdání matematické knihovny Mizaru pro vytváření článků v Mirazu

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F04%3A00005580" target="_blank" >RIV/00216208:11320/04:00005580 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Semantic browsing of the Mizar mathematical library for authoring Mizar articles

Popis výsledku v původním jazyce

The Mizar system is equipped with a very large library containing tens of thousands of theorems and thousands of definitions, which often use overloaded notation. For efficient authoring of new Mizar articles it is necessary to have good tools for searching and browsing this library. It would be ideal if such tools were simple, intuitive and easy to access. Particularly, they should provide interactive and integrated support during authoring Mizar articles. We describe an approach to this task which uses the extendable MML Query tools to generate a special representation of the Mizar library (MML). This representation, so called Generated Mizar Abstracts, contains human readable form of the MML, completed by additional information which is missing or hidden in regular Mizar abstracts and texts. It also includes semantic information necessary for implementing advanced browsing in the Mizar authoring environment for Emacs (Mizar mode).

Název v anglickém jazyce

Semantic browsing of the Mizar mathematical library for authoring Mizar articles

Popis výsledku anglicky

The Mizar system is equipped with a very large library containing tens of thousands of theorems and thousands of definitions, which often use overloaded notation. For efficient authoring of new Mizar articles it is necessary to have good tools for searching and browsing this library. It would be ideal if such tools were simple, intuitive and easy to access. Particularly, they should provide interactive and integrated support during authoring Mizar articles. We describe an approach to this task which uses the extendable MML Query tools to generate a special representation of the Mizar library (MML). This representation, so called Generated Mizar Abstracts, contains human readable form of the MML, completed by additional information which is missing or hidden in regular Mizar abstracts and texts. It also includes semantic information necessary for implementing advanced browsing in the Mizar authoring environment for Emacs (Mizar mode).

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

BA - Obecná matematika

OECD FORD obor

—

Projekt

—

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2004

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 periodika

Lecture Notes In Computer Science

ISSN

0302-9743

e-ISSN

—

Svazek periodika

3119

Číslo periodika v rámci svazku

neuveden

Stát vydavatele periodika

DE - Spolková republika Německo

Počet stran výsledku

14

Strana od-do

44-57

Kód UT WoS článku

—

EID výsledku v databázi Scopus

—