Momm - Rychle interredukce a dotazy ve velkych knihovnach formalni matematiky

Kód výsledku v IS VaVaI

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

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Momm - Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics

Popis výsledku v původním jazyce

MoMM (in the narrower sense) is a tool allowing fast interreduction of a high number of clauses, dumping and fast-loading of the interreduced clause sets, and their use for real-time retrieval of matching clauses in an interactive mode. MoMM's main taskis now providing these services for the world's largest body of formalized mathematics - the Mizar Mathematical Library (MML), which uses a richer formalism than just pure predicate logic. This task leads to a number of features (strength, speed, memoryefficiency, dealing with the richer Mizar logic, etc.) required from MoMM, and we describe the choices taken in its implementation corresponding to these requirements.

Název v anglickém jazyce

Momm - Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics

Popis výsledku anglicky

MoMM (in the narrower sense) is a tool allowing fast interreduction of a high number of clauses, dumping and fast-loading of the interreduced clause sets, and their use for real-time retrieval of matching clauses in an interactive mode. MoMM's main taskis now providing these services for the world's largest body of formalized mathematics - the Mizar Mathematical Library (MML), which uses a richer formalism than just pure predicate logic. This task leads to a number of features (strength, speed, memoryefficiency, dealing with the richer Mizar logic, etc.) required from MoMM, and we describe the choices taken in its implementation corresponding to these requirements.

Druh

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

CEP obor

JD - Využití počítačů, robotika a její aplikace

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 periodika

International Journal on Artificial Intelligence Tools

ISSN

0218-2130

e-ISSN

—

Svazek periodika

15

Číslo periodika v rámci svazku

1

Stát vydavatele periodika

SG - Singapurská republika

Počet stran výsledku

22

Strana od-do

109-130

Kód UT WoS článku

—

EID výsledku v databázi Scopus

—