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