Original title: Dosvědčování existenčních vět
Translated title: Witnessing of existential statements
Authors: Kolář, Jan ; Krajíček, Jan (advisor) ; Šaroch, Jan (referee)
Document type: Master’s theses
Year: 2021
Language: cze
Abstract: [cze] [eng]
Tato práce formuluje a dokazuje dosvědčovací větu pro tvrzení dokazatelná v teorii SPV tvaru ∀x∃yA(x, y), kde A odpovídá relaci rozhodnutelné v polynomiálním čase. Teo- rií SPV se zde rozumí rozšíření teorie TPV (univerzální teorie N0 v jazyce reprezentujícím polynomiální algoritmy) o přidané axiomy zajišťující existenci minima lineárního uspořá- dání definovaného polynomiální relací na počátečním úseku. Jelikož tyto přidané axiomy nejsou univerzální sentence, vyžaduje teorie SPV netriviální použití dosvědčovacích vět Herbrandovy a KPT, které mají přímé použití pouze pro teorie univerzální. Na základě dokázané dosvědčovací věty je odvozen NP vyhledávací problém charakterizující složitost nalezení y pro zadané x tak, aby platilo A(x, y). Část práce je věnována argumentům podporujícím domněnku, že teorie SPV je ostře silnější než TPV . 1 The thesis formulates and proves a witnessing theorem for SPV -provable formulas in the form ∀x∃yA(x, y) where A corresponds to a polynomial time decidable relation. By SPV we understand an extension of the theory TPV (the universal theory of N in the language representing polynomial algorithms) by additional axioms ensuring the existence of a minimum of a linear ordering defined by a polynomial time decidable relation on an initial segment. As these additional axioms are not universal sentences, the theory SPV requires nontrivial use of witnessing Herbrand's and KPT theorems which have direct application only for universal theories. Based on the proven witnessing theorem, we derive a NP search problem characterizing complexity of finding y for a given x such that A(x, y). A part of the thesis is dedicated to arguments supporting the conjecture that SPV is strictly stronger than TPV . 1
Keywords: formal theory|polynomial algorithm|complexity|witnessing; formální teorie|polynomiální algoritmus|složitost|dosvědčování

Institution: Charles University Faculties (theses) (web)
Document availability information: Available in the Charles University Digital Repository.
Original record: http://hdl.handle.net/20.500.11956/127452

Permalink: http://www.nusl.cz/ntk/nusl-448344


The record appears in these collections:
Universities and colleges > Public universities > Charles University > Charles University Faculties (theses)
Academic theses (ETDs) > Master’s theses