Témata prací (Výběr práce)Témata prací (Výběr práce)(verze: 290)
Detail práce
   Přihlásit přes CAS
Dosvědčování existenčních vět
Název práce v češtině: Dosvědčování existenčních vět
Název v anglickém jazyce: Witnessing of existential statements
Klíčová slova: formální teorie, polynomiální algoritmus
Klíčová slova anglicky: formal theory, polynomial algorithm
Akademický rok vypsání: 2018/2019
Typ práce: diplomová práce
Jazyk práce:
Ústav: Katedra algebry (32-KA)
Vedoucí / školitel: prof. RNDr. Jan Krajíček, DrSc.
Řešitel:
Zásady pro vypracování
Pro některé teorie T platí, že z T-důkazu tvrzení
ve formě \forall x \exists y A(x,y) lze sestrojit
algoritmus M, který na vstupu x spočítá nějakého svědka
y splňujícího A(x,y). Cílem práce je dokázat novou
"dosvědčovací větu" tohoto typu v níž algoritmus M
bude výpočetně dostupný (např. pravděpodobnostní
polynomiální, interaktivní, lokální vyhledávání,
polynomiální s omezeným přístupem k orákulu,
a pod.).
Seznam odborné literatury
J.Krajíček,
"From feasible proofs to feasible computations",
in: Computer Science Logic 2010, A. Dawar and H. Veith (Eds.),
LNCS 6247, Springer, Heidelberg (2010), pp.22-31.
http://www.karlin.mff.cuni.cz/~krajicek/brno.pdf

Tento článek uvádí do prolematiky dosvědčovacích vět
a cituje další literaturu.
Předběžná náplň práce
Najít nový příklad dosvědčovaní existenčních důsledků
nějaké teorie výpočetně dostupným algoritmem.
Předběžná náplň práce v anglickém jazyce
Find a new witnessing theorem for existential consequences
of a theory that uses a feasible algorithm.
 
Univerzita Karlova | Informační systém UK