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|složitost|dosvědčování |
English key words: | formal theory|polynomial algorithm|complexity|witnessing |
Academic year of topic announcement: | 2019/2020 |
Thesis type: | diploma thesis |
Thesis language: | čeština |
Department: | Department of Algebra (32-KA) |
Supervisor: | prof. RNDr. Jan Krajíček, DrSc. |
Author: | hidden - assigned and confirmed by the Study Dept. |
Date of registration: | 15.01.2020 |
Date of assignment: | 15.01.2020 |
Confirmed by Study dept. on: | 11.02.2020 |
Date and time of defence: | 23.06.2021 09:00 |
Date of electronic submission: | 21.05.2021 |
Date of submission of printed version: | 21.05.2021 |
Date of proceeded defence: | 23.06.2021 |
Opponents: | doc. Mgr. Jan Šaroch, Ph.D. |
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. |