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

Result code in 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>
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
Momm - Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics
Original language description
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.
Czech name
Momm - Rychle interredukce a dotazy ve velkych knihovnach formalni matematiky
Czech description
Momm je nastroj umoznujici rychlou interredukci velkeho poctu klauzuli, ukladani a rychle nacteni interredukovanych mnozin klauzuli, a jejich pouziti pro vyhledavani silnejsich klauzuli v realnem case.

Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
JD - Use of computers, robotics and its application
OECD FORD branch
—

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

Similar results(10)