[Proof Complexity] new paper

[Pavel Pudlak]

My new paper "The canonical pairs of bounded depth Frege systems" is now 
on arXiv

http://arxiv.org/abs/1912.03013

Abstract: The canonical pair of a proof system $P$ is the pair of disjoint 
NP sets where one set is the set of all satisfiable CNF formulas and the 
other is the set of CNF formulas that have $P$-proofs bounded by some 
polynomial. We give a combinatorial characterization of the canonical 
pairs of depth~$d$ Frege systems. Our characterization is based on certain 
games, introduced in this article, that are parametrized by a number~$k$, 
also called the depth. We show that the canonical pair of a depth~$d$ 
Frege system is polynomially equivalent to the pair $(A_{d+2},B_{d+2})$ 
where $A_{d+2}$ (respectively, $B_{d+1}$) are depth {$d+1$} games in which 
Player~I (Player II)  has a positional winning strategy. Although this 
characterization is stated in terms of games, we will show that these 
combinatorial structures can be viewed as generalizations of monotone 
Boolean circuits. In particular, depth~1 games are essentially monotone 
Boolean circuits. Thus we get a generalization of the monotone feasible 
interpolation for Resolution, which is a property that enables one to 
reduce the task of proving lower bounds on the size of refutations to 
lower bounds on the size of monotone Boolean circuits. However, we do not 
have a method yet for proving lower bounds on the size of depth~$d$ games 
for $d>1$.


Any comments are welcome.

Pavel Pudlak