Momm - Rychle interredukce a dotazy ve velkych knihovnach formalni matematiky

Abstrakt

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.

Klíčová slova

• Interreduction
• Retrieval
• Large
• Libraries
• Formalized
• Mathematics