Prezentace automaticky generovaných důkazů
| Thesis title in thesis language (Slovak): | Prezentace automaticky generovaných důkazů |
|---|---|
| Thesis title in Czech: | Prezentace automaticky generovaných důkazů |
| Thesis title in English: | Presenting automatically generated proofs |
| Academic year of topic announcement: | 2009/2010 |
| Thesis type: | Bachelor's thesis |
| Thesis language: | slovenština |
| Department: | Department of Algebra (32-KA) |
| Supervisor: | doc. RNDr. David Stanovský, Ph.D. |
| Author: | hidden - assigned and confirmed by the Study Dept. |
| Date of registration: | 03.11.2009 |
| Date of assignment: | 03.11.2009 |
| Date and time of defence: | 09.09.2010 00:00 |
| Date of electronic submission: | 09.09.2010 |
| Date of proceeded defence: | 09.09.2010 |
| Opponents: | doc. Mgr. Pavel Růžička, Ph.D. |
| Guidelines |
| Studentka se bude zabývat problémem převodu automaticky vygenerovaných důkazů do formy přístupné člověku.
Práce se dá řešit ve dvou rovinách: na konkrétním příkladě (dodaném vedoucím práce), nebo obecně, ve formě algoritmu a jeho implementace. Základní úlohou je převedení důkazu do formy lemma-důkaz-lemma-důkaz-... Nadstavbou pak je selekce vhodných lemmat, případně definice vhodných pojmů tak, aby výsledek byl rozumně interpretovatelný. Jako hříčka by bylo zajímavé implementovat algoritmus, který důkaz v rovnicové teorii převede do jediné dlouhé série rovností. Výstup ve formě textového souboru a ve formátu TeX. |
| References |
| Yury Puzis, Yi Gao, Geoff Sutcliffe, Automated Generation of Interesting Theorems, FLAIRS Conference 2006: 49-54
https://www.aaai.org/Papers/FLAIRS/2006/Flairs06-009.pdf http://www.prover9.org http://www.tptp.org Robinson, Voronkov, Handbook of automated reasoning |