Hlavní stránka > Výsledky hledání: Mikle-Barát, Ondrej
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 2 záznamů.  Hledání trvalo 0.00 vteřin. 
Silné důkazové systémy
 Mikle-Barát, Ondrej ; Krajíček, Jan (vedoucí práce) ; Pudlák, Pavel (oponent)
R-OBDD je nový Cook-Reckhowův důkazový systém pro výrokovou logiku založen na kombinaci OBDD důkazového systému a rezolučního důkazového systému. R-OBDD má sílu OBDD důkazového systému - tautologie s exponenciálně velkými důkazy v rezoluci jako PHPn nebo Tseitinovy kontradikce mají v R-OBDD systému polynomiální důkazy (R-OBDD p-simuluje jak OBDD důkazový systém, tak rezoluci). Na druhé straně, odvozovací pravidla R-OBDD systému byly navrhnuty, aby se podobaly odvozovacím pravidlům rezoluce. Tím pádem je možné vytvořit modifikaci DPLL algoritmu, která bude pracovat v R-OBDD systému a zároveň použít některé heuristiky známé z algoritmů založených na DPLL. Vzniká možnost vytvořit efektivnejší algoritmus na řešení problému splnitelnosti formule (SAT). Ukážeme návrh algoritmu, který je adaptací DPLL algoritmu pro R-OBDD důkazový systém. Přikldáme důkaz z jeho korektnosti a ukážeme, že jeho běh nad nesplnitelnou formulí je možné transformovat do stromového důkazu v R-OBDD systému.
Úplný záznam
Silné důkazové systémy
 Mikle-Barát, Ondrej ; Krajíček, Jan (vedoucí práce) ; Pudlák, Pavel (oponent)
R-OBDD je nový Cook-Reckhowův důkazový systém pro výrokovou logiku založen na kombinaci OBDD důkazového systému a rezolučního důkazového systému. R-OBDD má sílu OBDD důkazového systému - tautologie s exponenciálně velkými důkazy v rezoluci jako PHPn nebo Tseitinovy kontradikce mají v R-OBDD systému polynomiální důkazy (R-OBDD p-simuluje jak OBDD důkazový systém, tak rezoluci). Na druhé straně, odvozovací pravidla R-OBDD systému byly navrhnuty, aby se podobaly odvozovacím pravidlům rezoluce. Tím pádem je možné vytvořit modifikaci DPLL algoritmu, která bude pracovat v R-OBDD systému a zároveň použít některé heuristiky známé z algoritmů založených na DPLL. Vzniká možnost vytvořit efektivnejší algoritmus na řešení problému splnitelnosti formule (SAT). Ukážeme návrh algoritmu, který je adaptací DPLL algoritmu pro R-OBDD důkazový systém. Přikldáme důkaz z jeho korektnosti a ukážeme, že jeho běh nad nesplnitelnou formulí je možné transformovat do stromového důkazu v R-OBDD systému.
Ú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