|
|
(Im)possibilty results in Proof Complexity and Arithmetic
Khaniki, Erfan ; Pudlák, Pavel (advisor) ; Buss, Samuel (referee) ; Kolodziejczyk, Leszek (referee)
Title: (Im)possibilty results in Proof Complexity and Arithmetic Author: Erfan Khaniki Department: Department of Algebra Supervisor: Prof. RNDr. Pavel Pudl'ak, DrSc Abstract: We study various problems in proof complexity, bounded arithmetic, and intuitionistic arithmetic. We focus on topics such as lower bounds for different proof systems, connections between proof complexity generators and models of arithmetic, jump operators in proof complexity, and the non-locality of certain Kripke models of Heyting arithmetic. Keywords: Proof complexity, Lower bounds, Bounded arithmetic, Independence, Heyt- ing arithmetic, Kripke models 1
|
|
|
Proof Systems: A Study on Form and Complexity
Jalali Keshavarz, Raheleh ; Pudlák, Pavel (advisor) ; Metcalfe, George (referee) ; Ramanayake, Revantha (referee)
Proof Systems: A Study on Form and Complexity This dissertation includes three parts. The first two parts are related to each other. In [2] and [1], Iemhoff introduced a connection between the existence of a terminating sequent calculus of a certain kind and the uniform inter- polation property of the super-intuitionistic logic that the calculus captures. In the second part, we will generalize this relationship to also cover the sub- structural setting on the one hand and a more powerful type of systems called semi-analytic calculi, on the other. To be more precise, we will show that any sufficiently strong substructural logic with a semi-analytic calculus has Craig interpolation property and in case that the calculus is also terminating, it has uniform interpolation. This relationship then leads to some concrete applications. On the positive side, it provides a uniform method to prove the uniform interpolation property for the logics FLe, FLew, CFLe, CFLew, IPC, CPC and some of their K and KD-type modal extensions. However, on the negative side the relationship finds its more interesting application to show that many sub-structural logics including Ln, Gn, BL, R and RMe , al- most all super-intutionistic logics (except at most seven of them) and almost all extensions of S4 (except thirty seven of them) do not...
|
|
|
Silné důkazové systémy
Mikle-Barát, Ondrej ; Krajíček, Jan (advisor) ; Pudlák, Pavel (referee)
R-OBDD is a new Cook-Reckhow propositional proof system based on combination of OBDD proof system and resolution proof system. R-OBDD has the strength of OBDD proof system - hard tautologies for resolution like PHPn or Tseitin contradictions have polynomially sized proofs in R-OBDD (R-OBDD p-simulates OBDD proof system as well as resolution). On the other hand, inference rules of R-OBDD are designed to be similar to inference rules of resolution, thus allowing to create a modified version of DPLL algorithm and possibly using heuristics used in various DPLL-like algorithms. This gives a possibility for a SAT solver more efficient than SAT solvers based on resolution proof system. We present design of a SAT solver, which is an adaptation of DPLL algorithm for the R-OBDD proof system. The algorithm is accompanied with proof of its correctness and we show that the run of the algorithm on an unsatisfiable formula can be transformed into tree-like refutation in the R-OBDD proof system.
|
|
|
NP vyhledávací problémy a redukce mezi nimi
Ševčíková, Renáta ; Krajíček, Jan (advisor) ; Pudlák, Pavel (referee)
NP search problems and reductions among them Renáta Ševčíková In the thesis we study the class of Total NP search problems. More attention is devoted to study the subclasses of Total NP search problems and reductions among them. We combine some known methods: the search trees and their relation to re- ductions, the Nullstellensatz refutation and the degree lower bound based on design to show that two classes of relativized NP search problems based on Mod-p counting principle and Mod-q counting principle, where p and q are different primes, are not reducible to each other. This thesis is finished by a new separation result for p = 2 and q = 3.
|
|
|
Těžké tautologie
Pich, Ján ; Krajíček, Jan (advisor) ; Pudlák, Pavel (referee)
We investigate the unprovability of NP$\not\subseteq$P/poly in various fragments of arithmetic. The unprovability is usually obtained by showing hardness of propositional formulas encoding superpolynomial circuit lower bounds. Firstly, we discuss few relevant techniques and known theorems. Namely, natural proofs, feasible interpolation, KPT theorem, iterability, gadget generators etc. Then we prove some original results. We show the unprovability of superpolynomial circuit lower bounds for systems admitting certain forms of feasible interpolation (modulo a hardness assumption) and for systems roughly described as tree-like Frege systems working with formulas using only a small fraction of variables of the statement that is supposed to be proved. These results are obtained by proving the hardness of the Nisan-Wigderson generators in corresponding proof systems.
|
|
| |
|
|
In the Light of Intuitionism: Two Investigations in Proof Theory
Akbartabatabai, Seyedamirhossein ; Pudlák, Pavel (advisor) ; Beckmann, Arnold (referee) ; Iemhoff, Rosalie (referee)
In the Light of Intuitionism: Two Investigations in Proof Theory This dissertation focuses on two specific interconnections between the clas- sical and the intuitionistic proof theory. In the first part, we will propose a formalization for Gödel's informal reading of the BHK interpretation, using the usual classical arithmetical proofs. His provability interpretation of the propositional intuitionistic logic, first appeared in [1], in which he introduced the modal system, S4, as a formalization of the intuitive concept of prov- ability and then translated IPC to S4 in a sound and complete manner. His work suggested the search for a concrete provability interpretation for the modal logic S4 which itself leads to a concrete provability interpretation for the intutionistic logic. In the first chapter of this work, we will try to solve this problem. For this purpose, we will generalize Solovay's provabil- ity interpretation of the modal logic GL to capture other modal logics such as K4, KD4 and S4. Then, using the mentioned Gödel's translation, we will propose a formalization for the BHK interpretation via classical proofs. As a consequence, it will be shown that the BHK interpretation is powerful enough to admit many different formalizations that surprisingly capture dif- ferent propositional logics, including...
|
|
| |
|
|
NP vyhledávací problémy
Jirotka, Tomáš ; Krajíček, Jan (advisor) ; Pudlák, Pavel (referee)
Title: NP search problems Author: Tomáš Jirotka Department: Department of Algebra Supervisor: Prof. RNDr. Jan Krajíček, DrSc. Abstract: The thesis summarizes known results in the field of NP search pro- blems. We discuss the complexity of integer factoring in detail, and we propose new results which place the problem in known classes and aim to separate it from PLS in some sense. Furthermore, we define several new search problems. Keywords: Computational complexity, TFNP, integer factorization. 1
|
|
| |
guest ::
RSS feed.