|
|
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.
|
|
|
Trénovací program na mariáš
Caithaml, Tomáš ; Majerech, Vladan (oponent) ; Pudlák, Petr (vedoucí práce)
Predložená práce se zabývá návrhem programu na sehrávání trénovacích partií mariáše (tradiční české karetní hry) proti počítači. Uvažují se dvě varianty této hry pro tři hráče - mariáš volený a licitovaný. Program umožňuje sehrávat partie jak v turnajovém módu, který simuluje skutečnou hru, tak i v trénovacím módu, kdy hráč může nahlížet hráčům do karet, vracet tahy, přehrávat různé varianty, nechat si poradit tah a tak analyzovat herní situaci. Program lze rozšířit o další umělé hráče a lze mezi nimi pořádat turnaje. Práce dále představuje implementace umělého hráče, které jsou založeny na variantách alfa-beta prořezávání s několika vylepšeními.
|
|
|
Verefication of Mathematical Proofs
Pudlák, Petr ; Štěpánek, Petr (vedoucí práce) ; Haniková, Zuzana (oponent) ; Plátek, Martin (oponent)
In this thesis we deal with the problem of automatic proving (or disproving) mathematical conjectures using computer programs (usually called automated theorem provers). We address several issues that are important for a successful utilization of such programs. In Chapter 3 we examine how to store and reuse important pieces of mathematical knowledge in the form of lemmas. We investigate how this process can be automatized, i.e. how a computer can construct and use lemmas without human guidance. The program we develop tries to shorten or to speed up the proofs of several conjectures from a common theory. It repeatedly extracts lemmas from the proofs it has already completed and uses the lemmas to improve the sets of premisses to produce more efficient proofs of the conjectures. In Chapter 4 we develop a new algorithm that tries to construct the optimal sets of premisses for proving and disproving mathematical conjectures. The algorithm semantically analyzes the conjectures and the set of premisses of the given theory to find the optimal subsets of the premisses. The algorithm uses an automated model finder to construct models that serve as counterexamples that guide the algorithm to find the optimal set of premisses. In Chapter 5 we use the algorithm to decide formulae in a wide range of modal systems. We...
|
|
|
Simulace automobilového provozu
Gregor, Ivan ; Hladík, Milan (oponent) ; Pudlák, Petr (vedoucí práce)
Tato bakalářská práce se zabývá popisem podstatných částí programu, který simuluje automobilový provoz. Popisuje reprezentaci silniční sítě, agentů, průběh simulace a její výstup. Dále popisuje některé výsledky dosažené při simulaci konkrétních dopravních situací. Na konci práce je také uvedeno srovnání programu s multiagentnímy systémy. Silniční síť se skládá ze silnic a křižovatek, které jsou řízené světelnou signalizací. Uživatel programu může v simulaci pozorovat chování různých agentů. Jedinou podmínkou je, aby třída reprezentující agenta implementovala jednotný interface. Agentem se rozumí auto a řidič dohromady. Je to autonomní objekt, který se pohybuje po silniční síti v rámci daných omezení simulace. Chování agentů je tedy omezeno pravidly simulace. Agenti jsou případně simulací usměrňováni, aby nedošlo ke kolizi nebo k porušení pravidel silničního provozu. Výstup simulace použijeme pro porovnání úspešnosti jednotlivých strategií agentů, co se týče doby jízdy nebo spotřeby paliva.
|
host ::
RSS.