Usual time and place: Thursday 10.40 - 12.10,
Dept. of Algebra, Karlin
Program
in anti-chronological order:
14.December at 12.2o (note different day/time)
We shall have a double seminar this time:
1) Petra Kurinova
A polynomial algorithm for the binary
Post Correspondence Problem
The Post Correspondence Problem is undecidable in general
but it is in the computational complexity class P
in the binary case. I shall talk about a p-time
algorithm for the problem.
2) Alena Peterova
Lower bounds for resolution using
Razborov's approximation method
One method for proving lower bounds on the length of resolution
and cutting plane proofs is to reduce them to monotone circuits
(Krajicek; Pudlak). Then, the Razborov's approximation method is
used to prove exponential lower bound on the size of monotone
circuits. Our goal is to apply the approximation method on the
resolution proofs directly.
8.December at 10.4o
Jan Pich
Provability of circuit lower bounds in Bounded Arithmetics
Interesting circuit lower bounds like SAT$\notin$ P/poly could be
unprovable in strong fragments of Bounded Arithmetic. This possibility is
reflected in Razborov's conjecture about NW-generators. We will discuss it and
show that NW-generators are hard for a tree-like version of Frege working with
formulas built on a fraction of variables of the statement that is supposed to
be proven.
Another way how to obtain the unprovability result for strong theories (under a
hardness assumption) is to prove that proofs of circuit lower bounds in these
systems are NP-natural. It can be shown that in all sufficiently strong proof
systems admitting a feasible disjunction property circuit lower bounds are
already NP-natural. We will present the argument in the context
of intuitionistic Bounded Arithmetics.
The intuitionistic part is joint work with Kaveh Ghasemloo.
1.December at 10.4o
Yuval Filmus
Interpolating Cutting Plane(s) using games
Cutting Plane(s) is a refutation proof system coming
in two flavors, syntactic and semantic. Interpolation
theorems have been proved for the semantic version with
small coefficients (Krajicek; Pitassi et al.) and for
the (unrestricted) syntactic version (Pudlak).
The former theorems construct monotone boolean circuits,
the latter monotone real circuits.
For both types of circuits there are strong lower bounds,
which in turn imply strong lower bounds on the size of CP
refutations of the clique/coclique dichotomy.
We rephrase the constructions of Krajicek and Pitassi et al.
in terms of a two-player game which translates to a monotone
boolean circuit. A random version of the game translates
to a monotone real circuit.
We had hoped that the more advanced version of the game
would enable us to prove an interpolation theorem for
unrestricted semantic CP. However, at this stage it stands
as an open problem.
Joint work with Toni Pitassi.
24.November at 10.40
Alexander V. Smal
Optimal algorithms, acceptors and proof systems
The existence of optimal objects, such as algorithms,
acceptors or proof systems, is a major open question
in complexity theory. There is a bunch of results that
relate existence of one optimal object to another.
This talk will give a short survey on results about
such an optimal objects and related open problems.
18.November (Friday) at 13.3o-45
(note atypical day and hour!)
Anupam Das
The Relative Complexity of Deep Inference Proof Systems
Deep inference proof systems, broadly construed, are an extension of
regular inference systems by allowing inference rules to operate
arbitrarily deep inside a formula, rather than on just the main
connective. Clearly this can allow for a speedup in size of proofs, but
there are many questions open regarding the significance of this
speedup, especially for its cut-free tree-like systems. In this talk I
will talk through recent results connecting the complexity of deep
inference proofs to more traditional systems. In particular I will pose
(and briefly discuss) the problem of finding a lower bound for cut-free
tree-like deep inference, which remains open.
10.November: no seminar
3.November
There will be two seminars:
1) Kaveh Ghasemloo (morning)
Subsystems of TV^0 and sub-exponential size bounded depth Frege proofs
We study subsystems of $TV^0$ where string induction axiom is restricted to
sublinear size strings and show how first-order proofs of bounded formulas in
these theories translate to subexponential size bounded-depth Frege proofs. We
also show that string induction for size $n^{1/d}$ strings contains $VNC^1$ by
formalizing the well-known fact that $NC^1$ circuits have sub-exponential size
bounded-depth circuits. As a corollary we obtain an alternative proof of
[FPS'11] that subexponential size bounded-depth Frege simulates Frege.
This is joint work with Phuong Nguyen and Steve Cook.
[FPS'11]: Yuval Filmus, Toniann Pitassi, Rahul Santhanam, "Exponential lower
bounds for AC^0-Frege imply polynomial Frege lower bounds", ICALP 2011.
2)
Sebastian Muller (afternoon, 13.3o)
Short Proofs by short Cuts
We study polylogarithmic cuts of models of the bounded
arithmetic V^0. We will see that any polylog cut N of
a $V^0$ model M is a model of $VNC^1$. This is due to the
fact that N-strings can be represented as numbers in M
and we can thus use a stronger form of induction to prove
a $VNC^1$-complete problem. As a corollary we obtain
a modeltheoretic proof of a uniform version of the result from
[FPS11] that bounded-depth Frege subexponentially simulates Frege.
27.October
Dai Le
Formalizing the Goldreich-Levin theorem
The Goldreich-Levin theorem is one of the most fundamental theorems of
cryptography. The theorem shows how to construct a hardcore predicate
from any one-way function. I will discuss our progress on how to extend
Emil Jerabek's approximate counting framework to formalize this theorem
within the theory VPV + the surjective weak pigeonhole principle for
polytime functions.
The work is joint with Wesley George and Stephen Cook.
20.October
Luke Friedman
continues from 13.October
13.October
Luke Friedman
Kolmogorov Complexity, Circuits, and the Strength of Logical
Theories of Arithmetic
Can complexity classes be characterized in terms of efficient
reducibility to the (undecidable) set of Kolmogorov-random strings?
Although this might seem improbable, a series of papers has recently
provided evidence that this may be the case. In particular, it is
known that there is a class of problems C defined in terms of
polynomial-time truth-table reducibility to R_K (the set of
Kolmogorov-random strings) that lies between BPP and PSPACE. In this
talk, we investigate improving this upper bound from PSPACE to (PSPACE
intersect P/poly)
More precisely, we present a collection of true statements in the
language of arithmetic, (each provable in ZF)
and show that if these statements can be proved in certain extensions
of Peano arithmetic, then BPP \subseteq C \subseteq (PSPACE intersect
\Ppoly)
We conjecture that C is equal to P, and discuss the
possibility this might be an avenue for trying to prove the equality of
BPP and P.
Joint with Eric Allender, George Davie, Sam Hopkins, and Iddo Tzameret
6.October
Jan Krajicek
On possibilities to extend feasible interpolation
to stronger proof systems
The feasible interpolation idea, known facts,
chain feasible interpolation, feasible disjunction property,
and various problems.