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|složitost|dosvědčování
• Klíčová slova anglicky: formal theory|polynomial algorithm|complexity|witnessing
• Akademický rok vypsání: 2019/2020
• Typ práce: diplomová práce
• Jazyk práce: čeština
• Ústav: Katedra algebry (32-KA)
• Vedoucí / školitel: prof. RNDr. Jan Krajíček, DrSc.
• Řešitel: skrytý - zadáno a potvrzeno stud. odd.
• Datum přihlášení: 15.01.2020
• Datum zadání: 15.01.2020
• Datum potvrzení stud. oddělením: 11.02.2020
• Datum a čas obhajoby: 23.06.2021 09:00
• Datum odevzdání elektronické podoby: 21.05.2021
• Datum odevzdání tištěné podoby: 21.05.2021
• Datum proběhlé obhajoby: 23.06.2021
• Oponenti: doc. Mgr. Jan Šaroch, Ph.D.

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.