Prezentace automaticky generovaných důkazů
| Název práce v jazyce práce (slovenština): | Prezentace automaticky generovaných důkazů |
|---|---|
| Název práce v češtině: | Prezentace automaticky generovaných důkazů |
| Název v anglickém jazyce: | Presenting automatically generated proofs |
| Akademický rok vypsání: | 2009/2010 |
| Typ práce: | bakalářská práce |
| Jazyk práce: | slovenština |
| Ústav: | Katedra algebry (32-KA) |
| Vedoucí / školitel: | doc. RNDr. David Stanovský, Ph.D. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 03.11.2009 |
| Datum zadání: | 03.11.2009 |
| Datum a čas obhajoby: | 09.09.2010 00:00 |
| Datum odevzdání elektronické podoby: | 09.09.2010 |
| Datum proběhlé obhajoby: | 09.09.2010 |
| Oponenti: | doc. Mgr. Pavel Růžička, Ph.D. |
| Zásady pro vypracování |
| 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. |
| Seznam odborné literatury |
| 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 |