Národní úložiště šedé literatury Nalezeno 3 záznamů.  Hledání trvalo 0.01 vteřin. 
Konstrukce modelů pomocí CSP
Peterová, Alena ; Stanovský, David (vedoucí práce) ; Kazda, Alexandr (oponent)
V této práci se věnujeme algoritmům na konstrukci konečných modelů pro množiny axiomů logiky 1. řádu s cílem navrhnout a implementovat novou metodu, založenou na převodu na problém splnitelnosti omezení (CSP). V teoretické části představíme standardní metodu MACE, používající převod úloh na SAT, a pokročilejší techniky zvyšující její efektivitu: dělení klauzulí, definici termů a statickou redukci symetrií. Následuje návrh alternativní metody, která podobným způsobem převádí úlohy na CSP. Nově navrhujeme techniku redukce symetrií i pro binární funkce. Poté popíšeme implementaci alternativní metody pomocí CSP-modelovacího jazyka MiniZinc a CSP-solveru Gecode. Na závěr porovnáme výkonnost vytvořeného nástroje na hledání modelů s nejúspěšnějšími zástupci standardních metod, systémy Paradox a Mace4.
Metody odhadů složitosti důkazů ve výrokové logice
Peterová, Alena ; Pudlák, Pavel (vedoucí práce) ; Krajíček, Jan (oponent)
V této práci se věnujeme složitosti důkazových systémů pro výrokovou logiku. Nejprve ukážeme exponenciální dolní odhad na složitost rezoluce přímou aplikací Razborovovy aproximační metody, která byla dosud používána pouze pro odhady na velikost monotónních obvodů. Následně použijeme aproximační metodu i pro nový důkaz exponenciálního dolního odhadu na složitost náhodných rezolučních důkazů. To by mělo mít další využití při separování různých teorií v omezené aritmetice. V obou případech využijeme problém z teorie grafů zvaný Broken Mosquito Screens. Na závěr vyslovíme hypotézu, že aproximační metoda bude mít využití i v silnějších důkazových systémech, jako například Cutting Planes. Powered by TCPDF (www.tcpdf.org)
Konstrukce modelů pomocí CSP
Peterová, Alena ; Stanovský, David (vedoucí práce) ; Kazda, Alexandr (oponent)
V této práci se věnujeme algoritmům na konstrukci konečných modelů pro množiny axiomů logiky 1. řádu s cílem navrhnout a implementovat novou metodu, založenou na převodu na problém splnitelnosti omezení (CSP). V teoretické části představíme standardní metodu MACE, používající převod úloh na SAT, a pokročilejší techniky zvyšující její efektivitu: dělení klauzulí, definici termů a statickou redukci symetrií. Následuje návrh alternativní metody, která podobným způsobem převádí úlohy na CSP. Nově navrhujeme techniku redukce symetrií i pro binární funkce. Poté popíšeme implementaci alternativní metody pomocí CSP-modelovacího jazyka MiniZinc a CSP-solveru Gecode. Na závěr porovnáme výkonnost vytvořeného nástroje na hledání modelů s nejúspěšnějšími zástupci standardních metod, systémy Paradox a Mace4.

Viz též: podobná jména autorů
1 Peterová, Anna
Chcete být upozorněni, pokud se objeví nové záznamy odpovídající tomuto dotazu?
Přihlásit se k odběru RSS.