Aplikace genetických algoritmů v automatickém dokazování vět
| Název práce v češtině: | Aplikace genetických algoritmů v automatickém dokazování vět |
|---|---|
| Název v anglickém jazyce: | Application of genetic algorithms in Automated theorem proving |
| Akademický rok vypsání: | 2009/2010 |
| Typ práce: | bakalářská práce |
| Jazyk práce: | čeština |
| Ústav: | Katedra teoretické informatiky a matematické logiky (32-KTIML) |
| Vedoucí / školitel: | prof. RNDr. Petr Štěpánek, DrSc. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 10.11.2009 |
| Datum zadání: | 29.03.2010 |
| Datum a čas obhajoby: | 21.06.2010 00:00 |
| Datum odevzdání elektronické podoby: | 30.05.2010 |
| Datum odevzdání tištěné podoby: | 30.05.2010 |
| Datum proběhlé obhajoby: | 21.06.2010 |
| Oponenti: | RNDr. Mgr. Zuzana Petříčková, Ph.D. |
| Konzultanti: | doc. Mgr. Martin Pilát, Ph.D. |
| Zásady pro vypracování |
| Seznamte se s doporučenými kapitolami z monografií [1], [3] a [4]. Zaměřte se na dokazování ve specifických axiomatizacích (např. teorie grup, teorii monoidů). Inspirujte se postupem, ktery zvolil McCune v práci [5] pro dokazovač [6]. Zkuste modifikovat některé části dokazovacího algoritmu genetickými algoritmy. Na základě experimentů zvolte vhodný dokazovač pro dané problémy a nejvhodnější nastavení. Prozkoumejte zapojení dalších informací (demodulací a definicí atd.).
Porovnejte časy a další charakteristiky výpočtu (např. počet generovaných klauzulí) a zhodnoťte, zda nalezení nastavení dokazovače pomohlo ke zvýšení výpočtové efektivnosti. |
| Seznam odborné literatury |
| [1] John R. Koza: Genetic Programming: On the Programming of Computers by
Means of Natural Selection, MIT Press 1992 [2] Mitchell, M.: Introduction to genetic algorithms. MIT Press, 1996. [3] A. Bundy, The Computational Modelling of Mathematical Reasoning, Academic Press 1983 (Bundy). [4] A. Robinsons and A. Voronkov, Handbook of Automated Reasoning, Elsevier Science, 2001. [5] McCune http://www.cs.unm.edu/~mccune/ADAM-2007/robbins/ [6] 5.W. McCune, Prover9, http://www.cs.unm.edu/~mccune/prover9/, 2005-2007. |
| Předběžná náplň práce |
| Práce je věnována strojovému dokazování vět ve specifických teoriích a zabývá se možností usměrnit práci dokazovače použitím definic některých pojmů z dané teorie a možným využitím genetických algoritmů. Účinnost jednotlivých voleb bude měřena experimentálními výsledky.
|
| Předběžná náplň práce v anglickém jazyce |
| The thesis in the domain of Automated theorem proving examines the possibility of improving computational effectiveness of proofs in specific theories by supplying additional information about concepts and by applying genetic algorithms. The effects of choices of definitons, genetic algorithms and settings of the theorem prover will be compared by experimental results. |