Original title: Metody odhadů složitosti důkazů ve výrokové logice
Translated title: Methods of proving lower bounds in propositional logic
Authors: Peterová, Alena ; Pudlák, Pavel (advisor) ; Krajíček, Jan (referee)
Document type: Master’s theses
Year: 2013
Language: cze
Abstract: [cze] [eng]
V této práci se věnujeme složitosti důkazových systémů pro výrokovou logiku. Nejprve ukážeme exponenciální dolní odhad na složitost rezoluce přímou aplikací Razborovovy aproximační metody, která byla dosud používána pouze pro odhady na velikost monotónních obvodů. Následně použijeme aproximační metodu i pro nový důkaz exponenciálního dolního odhadu na složitost náhodných rezolučních důkazů. To by mělo mít další využití při separování různých teorií v omezené aritmetice. V obou případech využijeme problém z teorie grafů zvaný Broken Mosquito Screens. Na závěr vyslovíme hypotézu, že aproximační metoda bude mít využití i v silnějších důkazových systémech, jako například Cutting Planes. Powered by TCPDF (www.tcpdf.org) In the present work, we study the propositional proof complexity. First, we prove an exponential lower bound on the complexity of resolution applying directly Razborov's approximation method, which was previously used only for bounds on the size of monotone circuits. Next, we use the approximation method for a new proof of an exponential lower bound on the complexity of random resolution refutations. That should have further applications in separating some theories in bounded arithmetic. In both cases, we use a problem from the graph theory called Broken Mosquito Screens. Finally, we state a conjecture that the approximation method is applicable even for stronger propositional proof systems, for example Cutting Plane Proofs. Powered by TCPDF (www.tcpdf.org)
Keywords: approximation method; Broken Mosquito Screens; proof complexity; Resolution; aproximační metoda; Broken Mosquito Screens; důkazová složitost; Rezoluce

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/52080

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


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