|
|
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í.
|
|
|
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í.
|
|
|
Důkazy pomocí konečných automatů
Fišer, Jan ; Holub, Štěpán (vedoucí práce) ; Chvalovský, Karel (oponent)
V roce 2016 zveřejnil Hamoon Mousavi program Walnut implementující automatické dokazování vět o automatických posloupnostech. Hlavním cílem této práce bylo ukázat teoretickou funkčnost Walnutu na základě spojitosti automatických posloupností s Presburgerovou (resp. Büchiho) aritmetikou, jež je rozhodnutelnou teorií. Dalším cílem bylo s přiměřenou mírou detailnosti popsat, jak je rozhodovací procedura Walnutem doopravdy prováděna, a na závěr pak na praktických příkladech ukázat možné využití Walnutu při řešení konrétních problémů. Jedním z těchto konkrétních příkladů, jejichž řešení je v práci předvedeno, je například nalezení kritického exponentu Rudin- Shapirovy posloupnosti - tento příklad je v literatuře z roku 2003 uváděn jako otevřený problém (nicméně v současnosti se již o otevřený problém nejedná, nebot' v roce 2011 Shallit dokázal, že kritický exponent všech auto- matických posloupností je vyčíslitelný). Samotnou poslední kapitolu lze také díky tomu, že obsahuje podrobně okomentované řešené příklady, využít jako velice stručný manuál pro ty, kteří se s Walnutem setkávají poprvé a chtějí jej využít k vlastním aplikacím. 1
|
|
|
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.
|
|
| |
|
| |
|
| |
host ::
RSS.