Hlavní stránka > Výsledky hledání: keywords:"LeanCoP"
Hledej:
Tipy pro vyhledávaní :: Rozšířené hledání
Hledej ve sbírkách:
Seřadit podle: Zobrazit výsledky: Výstupní formát:
Národní úložiště šedé literatury Nalezeno 1 záznamů.  Hledání trvalo 0.00 vteřin. 
External sources of axioms in lean theorem proving
 Brunetto, Robert ; Suda, Martin (vedoucí práce) ; Pudlák, Petr (oponent)
Automatické dokazovače vět lze upravit tak, aby mohly používat externí zdroje axiomů. To bylo nedávno zkoumáno v kombinaci se saturačním dokazovačem SPASS-XDB, který během saturační smyčky odesílá dotazy o externí axiomy a přijímá odpovědi. Lean dokazovače používají sémantický tableau kalkulus. Proto je potřeba pro ně použít jiný přístup. Tato práce představuje myšlenku, že by bylo možné od sebe oddělit dokazování a komunikaci s externími zdroji axiomů a to tak, že se nejprve vygeneruje schématický důkaz, u kterého se až následně kontroluje zda mu odpovídají nějaká externí data a zda ho lze doplnit na důkaz. Součástí této práce je upravená verze dokazovače LeanCoP tak, aby demonstrovala tuto myšlenku a zároveň se ukazuje, že je tento program často efektivnější než SPASS-XDB - dokonce ho poráží i na všech vzorových příkladech z jeho webové stránky.
Úplný záznam

Chcete být upozorněni, pokud se objeví nové záznamy odpovídající tomuto dotazu?
Přihlásit se k odběru RSS.
Digitální repozitář :: Hledej :: Nový záznam :: Personalizace :: Nápověda
Powered by Invenio v1.1.2
Spravuje admin.invenio@techlib.cz
Tato stránka je dostupná také v následujících jazycích:
Česky  English