slideshow 3

Logic seminar

usually takes place each Monday at 16:00 in IM, rear building, ground floor
Chair: Pavel Pudlak, Neil Thapen, Jan Krajíček
More information on the old seminar web page. The programme is announced via the mailing list.

H-Coloring Dichotomy in Proof Complexity

Azza Gaysin
Charles University
Monday, 20. April 2020 - 13:30 to 15:00
The H-Coloring problem can be considered as an example of the computational problem from a huge class of constraint satisfaction problems (CSP): an H-Coloring of a graph G is just a homomorphism from G to H. The dichotomy theorem for H-Coloring was proved by Hell and Nešetřil (an analogous theorem for all CSPs was recently proved by Zhuk and Bulatov) and it says that for each H the problem is either p-time decidable or NP-complete. Since negations of unsatisfiable instances of CSP can be expressed as propositional tautologies, it seems to be natural to investigate the proof complexity of CSP.

We show that the decision algorithm in the p-time case of the H-Coloring can be formalized in a relatively weak theory and that the tautologies expressing the negative instances for such H have short proofs in propositional proof system R^*(log). We complement this upper bound result by a lower bound result for the special example of NP-complete case of the H-Coloring, using the... more

Reflection principles in the propositional calculus.

Pavel Pudlák
Tuesday, 14. April 2020 - 13:30 to 15:00
I will survey some results on the reflection principles for propositional proof systems, show a connection to the recent result on non-automatibility of Resolution and ask several problems.

** Location: **

On the proof complexity of Resolution over Polynomial Calculus

Erfan Khaniki
Institute of Mathematics
Monday, 30. March 2020 - 13:30 to 15:00
The refutation system Res_R(PC_d) is a natural extension of the Resolution refutation system such that it operates with disjunctions of degree d polynomials over ring R with boolean variables. For d=1, this system is called Res_R(lin). One of the important open problems in Proof Complexity is proving lower bounds for Res_R(lin) when R is a finite field such as F_2. Interestingly, Res_{F_2}(lin) is fairly strong, and there is no known nontrivial lower bound for it, but for Res^*_R(lin) (tree-like Res_R(lin)) we know exponential lower bounds for every finite field.

For the stronger systems Res_R(PC_d) and Res_R^*(PC_d) for d>1 on finite ring R, there is no known lower bounds. In this talk, we prove a size-width relation for Res_R(PC_d) and Res^*_R(PC_d) for every finite ring R. This relation is proved by a new idea to reduce the problem to the original Ben-Sasson and Wigderson size-width relation for Res and Res^* using extension variables. As a by product, we get the... more

Proof-theoretic analysis of some impredicative theories, Part 2

Fedor Pakhomov
Institute of Mathematics
Monday, 23. March 2020 - 13:30 to 15:00
In the field of ordinal analysis there is an important boundary between theories of predicative strength and essentially stronger impredicative theories. Calculation of proof-theoretic ordinals of impredicative theories requires considerably more advanced technique. This talk will be about relatively weak impredicative theories: theories of positive inductive definitions, Kripke-Platek set theory, and system of second-order arithmetic Pi^1_1-CA_0.  The key feature exhibiting by ordinal notation systems for this theories (in contrast with ordinal notations for predicative theories) is that they use larger ordinals to denote smaller ordinals. In the present talk I will discuss this ordinal notation systems and outline the method of proof-theoretic analysis of this systems based on operator-controlled derivation.