(Im)possibilty results in Proof Complexity and Arithmetic
| Název práce v češtině: | Výsledky o (ne)možnostech v důkazové složitosti a aritmetice |
|---|---|
| Název v anglickém jazyce: | (Im)possibilty results in Proof Complexity and Arithmetic |
| Klíčová slova: | důkazová složitost|dolní odhady|omezenená aritmetika|nezávislost|Heytingova aritmetika|Kripkeho modely |
| Klíčová slova anglicky: | Proof complexity|Lower bounds|Bounded arithmetic|Independence|Heyting arithmetic|Kripke models |
| Akademický rok vypsání: | 2019/2020 |
| Typ práce: | disertační práce |
| Jazyk práce: | angličtina |
| Ústav: | Matematický ústav AV ČR, v.v.i. (32-MUAV) |
| Vedoucí / školitel: | prof. RNDr. Pavel Pudlák, DrSc. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 04.12.2019 |
| Datum zadání: | 04.12.2019 |
| Datum potvrzení stud. oddělením: | 04.12.2019 |
| Datum a čas obhajoby: | 06.11.2023 12:30 |
| Datum odevzdání elektronické podoby: | 22.08.2023 |
| Datum odevzdání tištěné podoby: | 23.08.2023 |
| Datum proběhlé obhajoby: | 06.11.2023 |
| Oponenti: | prof. Samuel Buss |
| Prof. Leszek Kolodziejczyk | |
| Zásady pro vypracování |
| Problems in propositional proof complexity:
1. It is a longstanding problem to prove that depth d+1 Frege systems are exponentially stronger than depth d Frege systems for DNF tautologies. Prove such a separation at least for some low level fragments. This problem is connected with the separation of relativized versions of theories in Buss's bounded arithmetic hierarchy. Recently a small progress has been achieved by separating slightly stronger theories than T^1_2 from T^2_2 using lower bounds on refutations in Random Resolution system. I may be also interesting to study the propositional proof systems associated with these intermediate theories. Methods to be used: The natural approach is to design and prove a special switching lemma for some well known tautologies that have been conjectured to separate these systems. For Res(log) and depth 2 Frege systems, it is not excluded that monotone interpolation can be used. 2. Prove lower bounds on bounded depth Frege systems with parity as unbounded width connective. This seems to be even more difficult; lower bounds are only known for very restricted subsystems. Prove lower bounds at least for some restricted system; in particular, it would be interesting to prove a lower bound for DAG-like refutations in Resolution with parities. Methods: 1. In Buss et al. [1] the problem was reduced to lower bounds on Nullstellensatz proofs with certain extension axioms. For Nulstellensatz, the standard lower bound method is based on the so called designs. Try to construct designs for Nullstellensatz refutations of some tautology, such as PHP, with at least some limited set of extension axioms. 2. Another method, developed by Krajicek [2], is based on forcing. It would be interesting to get at least some partial results based on forcing. 3. For some weak subsystems, in particular resolution with Parities, feasible interpolation may work. This requires to prove lower bounds on certain DAG-like communication protocols. 2. Problems in communication complexity. As mentioned above, lower bounds for certain DAG-like protocols may help us prove lower bounds for some proof systems. Prove new lower bounds for DAG-like communication protocols. Methods: Use methods by which lower bounds on monotone Boolean circuits are proved. There are two: Razborov's approximation method and, more recent one, based on hardness amplification using gadgets. 3. Problems in bounded arithmetic. 1. Separate fragments of relativized bounded arithmetic hierarchy. Methods: The standard approach is based on lower bounds on bounded depth Frege proof systems as mentioned above. A model-theoretical approach was proposed in [3]. 2. Find an example of an algorithm such that its correctness is provable in some fragment of bounded arithmetic, but there is no algorithm for the same problem whose correctness is provable in a weaker fragment. Methods: It will be necessary to use some plausible unproven conjectures, either from computational complexity, or from bounded arithmetic. 3. Problems in circuit complexity. 1. AC^0 cardinality: This problem is proposed in [4]. 2. Unconditional Lower Bound for MCSP: This problem is proposed in [5]. |
| Seznam odborné literatury |
| [1] S.R. Buss, R. Impagliazzo, J. Krajíček, P. Pudlák, A. Razborov and J. Sgall,
Proof Complexity in Algebraic Systems and Constant Depth Frege Systems with Modular Counting, Computational Complexity 6, 256-298 (1995/1996), [2] J. Krajíček, Forcing with random variables and proof complexity, London Mathematical Society Lecture Note Series, No.382, Cambridge University Press, (2011) [3] P. Pudlák, Superexponential computations in exponential domain, Extended abstract of a lecture at JAF, Seville 11.6.2007. [4] J. Krajíček, Open problems, http://www.karlin.mff.cuni.cz/~krajicek/problemy.html [5] Lower Bounds in Computational Complexity, https://www.dropbox.com/sh/jz4w4njo62hh2td/AAAq6AiqZr9UEDb0ExjFSwWDa?dl=0&preview=Lower+Bounds+-+Open+Problems.pdf |