Využití metod strojového učení v systému MPTP
| Název práce v češtině: | Využití metod strojového učení v systému MPTP |
|---|---|
| Název v anglickém jazyce: | Analysis of machine learning methods for guiding MPTP theorem prover |
| Akademický rok vypsání: | 2005/2006 |
| Typ práce: | diplomová práce |
| Jazyk práce: | |
| Ústav: | Katedra teoretické informatiky a matematické logiky (32-KTIML) |
| Vedoucí / školitel: | Mgr. Marta Vomlelová, Ph.D. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 14.11.2005 |
| Datum zadání: | 14.11.2005 |
| Zásady pro vypracování |
| Cílem práce je analyzovat možnosti strojového učení na podporu automatického dokazování vět knihovny MIZAR přeložené pomocí MPTP.
Pro dokázání nové (neznámé) věty není výpočetně zvládnutelné uvažovat všechny dříve dokázané věty. Cílem práce bude prozkoumání možností strojového učení pro vytvoření modelu, který by odfiltroval neužitečné věty a omezil prostor prohledávání na zvládnutelnou úroveň. Rozbor se bude týkat jak definování atributů vhodných pro vstup algoritmu pro strojové učení, tak i výběru modelu pro učení. Práce bude podložena experimenty. |
| Seznam odborné literatury |
| Mizar manual
Josef Urban: MPTP 0.2: Design, Implementation and First Cross-verification Experiments Petr Berka: Dobývání znalostí z databází, Praha : Academia, 2003. Weka http://www.cs.waikato.ac.nz/ml/weka/ Ian H. Witten, Eibe Frank: Data Mining: Practical Machine Learning Tools and Techniques, Morgan Kaufmann June 2005 SNoW http://l2r.cs.uiuc.edu/~danr/snow.html |