Využití metod strojového učení v systému MPTP
| Thesis title in Czech: | Využití metod strojového učení v systému MPTP |
|---|---|
| Thesis title in English: | Analysis of machine learning methods for guiding MPTP theorem prover |
| Academic year of topic announcement: | 2005/2006 |
| Thesis type: | diploma thesis |
| Thesis language: | |
| Department: | Department of Theoretical Computer Science and Mathematical Logic (32-KTIML) |
| Supervisor: | Mgr. Marta Vomlelová, Ph.D. |
| Author: | hidden - assigned and confirmed by the Study Dept. |
| Date of registration: | 14.11.2005 |
| Date of assignment: | 14.11.2005 |
| Guidelines |
| 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. |
| References |
| 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 |