Thesis (Selection of subject)Thesis (Selection of subject)(version: 285)
Assignment details
   Login via CAS
Dosvědčování existenčních vět
Thesis title in Czech: Dosvědčování existenčních vět
Thesis title in English: Witnessing of existential statements
Key words: formální teorie, polynomiální algoritmus
English key words: formal theory, polynomial algorithm
Academic year of topic announcement: 2018/2019
Type of assignment: diploma thesis
Thesis language:
Department: Department of Algebra (32-KA)
Supervisor: prof. RNDr. Jan Krajíček, DrSc.
Author:
Guidelines
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.).
References
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.
Preliminary scope of work
Najít nový příklad dosvědčovaní existenčních důsledků
nějaké teorie výpočetně dostupným algoritmem.
Preliminary scope of work in English
Find a new witnessing theorem for existential consequences
of a theory that uses a feasible algorithm.
 
Charles University | Information system of Charles University | http://www.cuni.cz/UKEN-329.html