Attributes | Values |
---|
rdf:type
| |
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 task is 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, memory efficiency, dealing with the richer Mizar logic, etc.) required from MoMM, and we describe the choices taken in its implementation corresponding to these requirements.
- 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 task is 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, memory efficiency, dealing with the richer Mizar logic, etc.) required from MoMM, and we describe the choices taken in its implementation corresponding to these requirements. (en)
- 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. (cs)
|
Title
| - Momm - Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics
- Momm - Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics (en)
- Momm - Rychle interredukce a dotazy ve velkych knihovnach formalni matematiky (cs)
|
skos:prefLabel
| - Momm - Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics
- Momm - Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics (en)
- Momm - Rychle interredukce a dotazy ve velkych knihovnach formalni matematiky (cs)
|
skos:notation
| - RIV/00216208:11320/06:00005336!RIV08-MSM-11320___
|
http://linked.open.../vavai/riv/strany
| |
http://linked.open...avai/riv/aktivita
| |
http://linked.open...avai/riv/aktivity
| |
http://linked.open...iv/cisloPeriodika
| |
http://linked.open...vai/riv/dodaniDat
| |
http://linked.open...aciTvurceVysledku
| |
http://linked.open.../riv/druhVysledku
| |
http://linked.open...iv/duvernostUdaju
| |
http://linked.open...titaPredkladatele
| |
http://linked.open...dnocenehoVysledku
| |
http://linked.open...ai/riv/idVysledku
| - RIV/00216208:11320/06:00005336
|
http://linked.open...riv/jazykVysledku
| |
http://linked.open.../riv/klicovaSlova
| - Interreduction; Retrieval; Large; Libraries; Formalized; Mathematics (en)
|
http://linked.open.../riv/klicoveSlovo
| |
http://linked.open...odStatuVydavatele
| - SG - Singapurská republika
|
http://linked.open...ontrolniKodProRIV
| |
http://linked.open...i/riv/nazevZdroje
| - International Journal on Artificial Intelligence Tools
|
http://linked.open...in/vavai/riv/obor
| |
http://linked.open...ichTvurcuVysledku
| |
http://linked.open...cetTvurcuVysledku
| |
http://linked.open...UplatneniVysledku
| |
http://linked.open...v/svazekPeriodika
| |
http://linked.open...iv/tvurceVysledku
| |
http://linked.open...n/vavai/riv/zamer
| |
issn
| |
number of pages
| |
http://localhost/t...ganizacniJednotka
| |