Témata prací (Výběr práce)Témata prací (Výběr práce)(verze: 336)
Detail práce
   Přihlásit přes CAS
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: 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.
 
Univerzita Karlova | Informační systém UK