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.

Some consequences of cryptographical conjectures for S^1_2 and EF

Raheleh Jalali
Institute of Mathematics
Monday, 2. November 2015 - 13:30 to 15:00
We present a paper by J. Krajicek and P. Pudlak from 1995. We show that if the RSA cryptosystem is secure, then \Delta^b_1 interpolation does not hold for S^1_2. Furthermore, we show that if factoring and discrete logarithm are in P/poly, then a certain \Pi^b_1 extension of S^1_2 does not admit \Delta^b_1 interpolation. At last, as a corollary we obtain that the feasible interpolation theorem fails for Extended Frege proof systems, if RSA is secure.

Consistency of circuit evaluation, extended resolution and total NP search problems

Jan Krajíček
Monday, 26. October 2015 - 13:30 to 15:00
We consider sets Γ(n,s,k) of narrow clauses expressing that no definition of a size s circuit with n inputs is refutable in resolution R in k steps. We show that every CNF shortly refutable in Extended R, ER, can be easily reduced to an instance of Γ(0,s,k) (with s,k depending on the size of the ER-refutation) and, in particular, that Γ(0,s,k) when interpreted as a relativized NP search problem is complete among all such problems provably total in the bounded arithmetic theory V^1_1. We use the ideas of implicit proofs to define from Γ(0,s,k) a non-relativized NP search problem iΓ and we show that it is complete among all such problems provably total in bounded arithmetic theory V^1_2. The reductions are definable in S12. We indicate how similar results can be proved for some other propositional proof systems and bounded arithmetic theories and how the construction can be used to define specific random unsatisfiable formulas, and we formulate two open problems about them.

Lower bounds on semantic cutting planes

Pavel Hrubeš
Institute of Mathematics, ASCR
Monday, 19. October 2015 - 13:30 to 15:00
Cutting Planes is a refutation system which certifies unsatisfiability of a set of linear inequalities. Typically, it is defined as using the addition rule and rounding rule. We consider the semantic version of the system, where every sound inference with a constant number of premises is allowed. We observe that the semantic system has feasible interpolation via monotone real circuits - a fact previously established for syntactic cutting planes by P. Pudlak. Nevertheless, we show that the semantic system is strictly stronger than the syntactic. Joint work with Y. Filmus and M. Lauria.

Bounded Arithmetic and Propositional Inconsistency Search Functions

Samuel R. Buss
University of California, San Diego
Monday, 27. July 2015 - 13:30
We discuss the strength of fragments of second order bounded arithmetic in defining total NP search (TFNP) problems based on consistency of Frege and extended Frege proofs. This gives new examples of problems that are many-one complete for the second order theories U-1-2 and V-1-2 with proof theoretic strength characterized by polynomial space computation and exponential time computation. (Joint work with Arnold Beckmann.) The talk will begin with a review of the relevant theories of bounded arithmetic, and of the Frege and extended Frege proof systems. It might also cover recent results on propositional proofs of the pigeonhole principle and the Kneser-Lovasz theorem.