|
|
Vyvrtávací hlava na vrtačku
Suda, Martin ; Kozáček, Peter (oponent) ; Kočiš, Petr (vedoucí práce)
Tato bakalářská práce, spadající do oblasti obráběcích strojů a příslušenství, se zabývá obráběcí metodou vyvrtávání a především nástroji sloužící k vyvrtávání. Práce je rozdělena na rešeršní a praktickou část, ve které je řešena vyvrtávací hlava s excentricky uloženým vřetenem, jehož pohybem po kružnici se frézuje otvor.
|
|
|
Vřeteník a hlavní vřeteno horizontálního soustružnického centra
Suda, Martin ; Novotný, Lubomír (oponent) ; Dokoupil, Vladimír (vedoucí práce)
Diplomová práce se zabývá problematikou vřeteníku a vřetene univerzálního soustružnického centra. Práce se ve své úvodní části věnuje morfologii vřeteníku, kde je popsáno, jakými způsoby lze vřeteno a vřeteník řešit z hlediska jeho uložení, zástavby, použitého upínacího rozhraní způsobu mazání, chlazení a těsnění. Druhá část je věnována rešerši strojů dostupných na trhu. Závěrečná část je již věnuje praktickému řešení vřeteníku a vřetene, na kterém by bylo možné provádět mimo soustružení i frézovací a vrtací operace.
|
|
|
Efektivní algoritmy oveřování cílů v počítačových hrách
Suda, Martin ; Hric, Jan (vedoucí práce) ; Majerech, Vladan (oponent)
Tato práce se zabývá neuniformními metodami prohledávání stromů her dvou hráčů s úplnou informací. Konkrétně je zkoumána neuniformita založená na hrozbách realizovaná v podobě algoritmů lambda search a dual-lambda search. Hrozby, defi nované jakožto útočné tahy, po kterých, když se obránce svého tahu vzdá, bude již s jistotou poražen, umožňují zredukovat prohledávaný prostor při zachování korektnosti výsledku. Práce dále popisuje novou metodu konstrukce tzv. zón relevance, tj. seznamů tahů resp. míst na hrací ploše, které jedině mohou mít vliv na výsledek. S pomocí těchto zón je možné výše jmenované algoritmy značně urychlit. V práci jsou též popsány tři hry, AtariGo, Hex a Piškvorky, a je rozebrána jejich vhodnost pro aplikaci zkoumané metody. Součástí práce je též implementace metody pro tyto hry s využitím známých technik (transpoziční tabulky, history heuristika).
|
|
|
Efektivní algoritmy oveřování cílů v počítačových hrách
Suda, Martin ; Hric, Jan (vedoucí práce)
Tato práce se zabývá neuniformními metodami prohledávání stromů her dvou hráčů s úplnou informací. Konkrétně je zkoumána neuniformita založená na hrozbách realizovaná v podobě algoritmů lambda search a dual-lambda search. Hrozby, de nované jakožto útočné tahy, po kterých, když se obránce svého tahu vzdá, bude již s jistotou poražen, umožňují zredukovat prohledávaný prostor při zachování korektnosti výsledku. Práce dále popisuje novou metodu konstrukce tzv. zón relevance, tj. seznamů tahů resp. míst na hrací ploše, které jedině mohou mít vliv na výsledek. S pomocí těchto zón je možné výše jmenované algoritmy značně urychlit. V práci jsou též popsány tři hry, AtariGo, Hex a Piškvorky, a je rozebrána jejich vhodnost pro aplikaci zkoumané metody. Součástí práce je též implementace metody pro tyto hry s využitím známých technik (transpoziční tabulky, history heuristika).
|
|
|
Vřeteník a hlavní vřeteno horizontálního soustružnického centra
Suda, Martin ; Novotný, Lubomír (oponent) ; Dokoupil, Vladimír (vedoucí práce)
Diplomová práce se zabývá problematikou vřeteníku a vřetene univerzálního soustružnického centra. Práce se ve své úvodní části věnuje morfologii vřeteníku, kde je popsáno, jakými způsoby lze vřeteno a vřeteník řešit z hlediska jeho uložení, zástavby, použitého upínacího rozhraní způsobu mazání, chlazení a těsnění. Druhá část je věnována rešerši strojů dostupných na trhu. Závěrečná část je již věnuje praktickému řešení vřeteníku a vřetene, na kterém by bylo možné provádět mimo soustružení i frézovací a vrtací operace.
|
|
|
Resolution-based methods for linear temporal reasoning
Suda, Martin ; Barták, Roman (vedoucí práce) ; Hoffmann, Jörg (oponent) ; Biere, Armin (oponent)
Cílem této práce je prozkoumat potenciál metod založených na rezoluci pro uvažování s lineárním časem. To na abstraktní rovině znamená navrhnout nové algoritmy pro automatické uvažovaní o vlastnostech systémů, které se vyvíjí v čase. Konkrétně v této práci ukážeme, 1) jak adaptovat superpoziční metodu pro dokazování vět ve výrokové lineární temporální logice (LTL), 2) jak využít příbuznost mezi superpozicí a kalkulem CDCL z moderních SAT-solverů pro navržení nového LTL dokazovače, 3) jak tento specializovat pro problém dosažitelnosti a objevit tak blízkou souvislost s algoritmem Property Directed Reachability (PDR), v nedávné době vyvinutém pro model checking hardwarových obvodů, 4) jak dále vylepšit PDR novou technikou pro urychlení fáze propagace klauzulí, 5) jak PDR adaptovat pro problém automatického plánování tím, že se SAT-solver v algoritmu nahradí procedurou specifickou pro plánovací vstupy. Navržené myšlenky byly implementovány a práce obsahuje výsledky experimentů, které na reprezentativních množinách benchmarků prokazují jejich praktický potenciál. Náš systém LS4 se ukázal býti jedním z nejsilnějších veřejně dostupných LTL dokazovačů. Zmíněné vylepšení algoritmu PDR podstatně zvyšuje výkon naší implementace při verifikaci hardware v multi-property módu. Dá se předpokládat, že ostatní implementace...
|
|
|
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.
|
|
|
Efektivní algoritmy oveřování cílů v počítačových hrách
Suda, Martin ; Majerech, Vladan (oponent) ; Hric, Jan (vedoucí práce)
Tato práce se zabývá neuniformními metodami prohledávání stromů her dvou hráčů s úplnou informací. Konkrétně je zkoumána neuniformita založená na hrozbách realizovaná v podobě algoritmů lambda search a dual-lambda search. Hrozby, defi nované jakožto útočné tahy, po kterých, když se obránce svého tahu vzdá, bude již s jistotou poražen, umožňují zredukovat prohledávaný prostor při zachování korektnosti výsledku. Práce dále popisuje novou metodu konstrukce tzv. zón relevance, tj. seznamů tahů resp. míst na hrací ploše, které jedině mohou mít vliv na výsledek. S pomocí těchto zón je možné výše jmenované algoritmy značně urychlit. V práci jsou též popsány tři hry, AtariGo, Hex a Piškvorky, a je rozebrána jejich vhodnost pro aplikaci zkoumané metody. Součástí práce je též implementace metody pro tyto hry s využitím známých technik (transpoziční tabulky, history heuristika).
|
|
|
Efektivní algoritmy oveřování cílů v počítačových hrách
Suda, Martin ; Hric, Jan (vedoucí práce)
Tato práce se zabývá neuniformními metodami prohledávání stromů her dvou hráčů s úplnou informací. Konkrétně je zkoumána neuniformita založená na hrozbách realizovaná v podobě algoritmů lambda search a dual-lambda search. Hrozby, de nované jakožto útočné tahy, po kterých, když se obránce svého tahu vzdá, bude již s jistotou poražen, umožňují zredukovat prohledávaný prostor při zachování korektnosti výsledku. Práce dále popisuje novou metodu konstrukce tzv. zón relevance, tj. seznamů tahů resp. míst na hrací ploše, které jedině mohou mít vliv na výsledek. S pomocí těchto zón je možné výše jmenované algoritmy značně urychlit. V práci jsou též popsány tři hry, AtariGo, Hex a Piškvorky, a je rozebrána jejich vhodnost pro aplikaci zkoumané metody. Součástí práce je též implementace metody pro tyto hry s využitím známých technik (transpoziční tabulky, history heuristika).
|
|
|
Vyvrtávací hlava na vrtačku
Suda, Martin ; Kozáček, Peter (oponent) ; Kočiš, Petr (vedoucí práce)
Tato bakalářská práce, spadající do oblasti obráběcích strojů a příslušenství, se zabývá obráběcí metodou vyvrtávání a především nástroji sloužící k vyvrtávání. Práce je rozdělena na rešeršní a praktickou část, ve které je řešena vyvrtávací hlava s excentricky uloženým vřetenem, jehož pohybem po kružnici se frézuje otvor.
|
host ::
RSS.