"SG - Singapursk\u00E1 republika" . . . . "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 . "Momm - Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics"@en . "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." . . "486676" . "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 - Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics" . "22"^^ . "[7D5B50B33B63]" . "Z(MSM0021620838)" . "Momm - Rychle interredukce a dotazy ve velkych knihovnach formalni matematiky"@cs . . "Momm - Rychle interredukce a dotazy ve velkych knihovnach formalni matematiky"@cs . "1"^^ . . "Interreduction; Retrieval; Large; Libraries; Formalized; Mathematics"@en . . "RIV/00216208:11320/06:00005336" . "1"^^ . "15" . . "Urban, Josef" . "0218-2130" . "109;130" . "Momm - Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics"@en . "International Journal on Artificial Intelligence Tools" . "1" . . . "11320" . . "RIV/00216208:11320/06:00005336!RIV08-MSM-11320___" . . . "Momm - Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics" . . . .