|
|
Moderní plánovací algoritmy
Binko, Petr ; Rozman, Jaroslav (oponent) ; Zbořil, František (vedoucí práce)
Tato práce popisuje algoritmy graphplan, satplan a real-time adaptive A*. Na implementaci těchto algoritmů je otestována jejich funkčnost a předpokládané vlastnosti (real-time výpočet, paralelismus), v netriviálních doménách. Graphplan a satplan jsou testovány v doménách block-world, tire-worl a bulldozer. Výsledky těchto algoritmů jsou porovnány a vykresleny do grafu. Real-time adaptive A* je testován v doméně tire-world. Dosažené výsledky jsou srovnány s klasickým A* a jsou zhodnoceny výhody a nevýhody těchto algoritmů.
|
|
|
Automatický theorem prover
Mazánek, Martin ; Havlena, Vojtěch (oponent) ; Lengál, Ondřej (vedoucí práce)
Tato bakalářská práce se zabývá implementací systému pro automatické dokazování vět výrokové a predikátové logiky používajícím rezoluci. Cílem této práce je vytvořit jednoduchý systém a zdokumentovat jeho vývoj, nikoliv tvorba konkurenceschopného systému. Dále je v práci představeno několik populárních systémů automatického dokazování.
|
|
|
Vizualizace rezoluční metody
Smetka, Tomáš ; Orság, Filip (oponent) ; Rozman, Jaroslav (vedoucí práce)
Tato bakalářská práce se zabývá problematikou automatického dokazování ve výrokové a predikátové logice. V teoretické části je popsána výroková a predikátová logika v návaznosti na systém jejich automatického dokazování pomocí rezoluční metody. V práci je dále popsán návrh a implementace programu, který se skládá z terminálu a serverové části. Program hledá důkaz nesplnitelnosti zadané formule a vizualizuje jednotlivé kroky vedoucí k nalezení řešení. V závěru je vyhodnocena implementace řešení a práce jako celek a také jsou popsány další možnosti rozšíření.
|
|
|
Automatický theorem prover
Mazánek, Martin ; Havlena, Vojtěch (oponent) ; Lengál, Ondřej (vedoucí práce)
Tato bakalářská práce se zabývá implementací systému pro automatické dokazování vět výrokové a predikátové logiky používajícím rezoluci. Cílem této práce je vytvořit jednoduchý systém a zdokumentovat jeho vývoj, nikoliv tvorba konkurenceschopného systému. Dále je v práci představeno několik populárních systémů automatického dokazování.
|
|
|
Vizualizace rezoluční metody
Smetka, Tomáš ; Orság, Filip (oponent) ; Rozman, Jaroslav (vedoucí práce)
Tato bakalářská práce se zabývá problematikou automatického dokazování ve výrokové a predikátové logice. V teoretické části je popsána výroková a predikátová logika v návaznosti na systém jejich automatického dokazování pomocí rezoluční metody. V práci je dále popsán návrh a implementace programu, který se skládá z terminálu a serverové části. Program hledá důkaz nesplnitelnosti zadané formule a vizualizuje jednotlivé kroky vedoucí k nalezení řešení. V závěru je vyhodnocena implementace řešení a práce jako celek a také jsou popsány další možnosti rozšíření.
|
|
|
Moderní plánovací algoritmy
Binko, Petr ; Rozman, Jaroslav (oponent) ; Zbořil, František (vedoucí práce)
Tato práce popisuje algoritmy graphplan, satplan a real-time adaptive A*. Na implementaci těchto algoritmů je otestována jejich funkčnost a předpokládané vlastnosti (real-time výpočet, paralelismus), v netriviálních doménách. Graphplan a satplan jsou testovány v doménách block-world, tire-worl a bulldozer. Výsledky těchto algoritmů jsou porovnány a vykresleny do grafu. Real-time adaptive A* je testován v doméně tire-world. Dosažené výsledky jsou srovnány s klasickým A* a jsou zhodnoceny výhody a nevýhody těchto algoritmů.
|
|
|
Řešitel příkladů pro předmět Teoretické základy informatiky
Šimonová, Adriana
Šimonová A., Řešitel příkladů pro předmět Teoretické základy informatiky. Bakalářská práce. Mendelova univerzita v Brně, 2013. Bakalářská práce je zaměřena na předmět Teoretické základy informatiky, konkrétně na výrokovou logiku. V teoretické části práce je popsána teorie výrokové logiky, tak aby čtenáři danou problematiku pochopili. V druhé části práce, je poté popisována práce se samotným řešitelem příkladů.
|
host ::
RSS.