Stasys Jukna

In a semantic resolution proof we operate with clauses only

but allow {\em arbitrary} rules of inference:

C_1 C_2 ... C_m

__________________

C

Consistency is the only requirement. We prove a very simple

exponential lower bound for the size ...
more >>>

Albert Atserias, Maria Luisa Bonet

Having good algorithms to verify tautologies as efficiently as possible

is of prime interest in different fields of computer science.

In this paper we present an algorithm for finding Resolution refutations

based on finding tree-like Res(k) refutations. The algorithm is based on

the one of Beame and Pitassi \cite{BP96} ...
more >>>

Josh Buresh-Oppenheim, Paul Beame, Ran Raz, Ashish Sabharwal

We prove a quasi-polynomial lower bound on the size of bounded-depth

Frege proofs of the pigeonhole principle $PHP^{m}_n$ where

$m= (1+1/{\polylog n})n$.

This lower bound qualitatively matches the known quasi-polynomial-size

bounded-depth Frege proofs for these principles.

Our technique, which uses a switching lemma argument like other lower bounds

for ...
more >>>

Dmitry Sokolov

One of the major open problems in proof complexity is to prove lower bounds on $AC_0[p]$-Frege proof

systems. As a step toward this goal Impagliazzo, Mouli and Pitassi in a recent paper suggested to prove

lower bounds on the size for Polynomial Calculus over the $\{\pm 1\}$ basis. In this ...
more >>>

Ilario Bonacina, Maria Luisa Bonet

The propositional proof system Sherali-Adams (SA) has polynomial-size proofs of the pigeonhole principle (PHP). Similarly, the Nullstellensatz (NS) proof system has polynomial size proofs of the bijective (i.e. both functional and onto) pigeonhole principle (ofPHP). We characterize the strength of these algebraic proof systems in terms of Boolean proof systems ... more >>>

Johan HÃ¥stad

We study Frege proofs for the one-to-one graph Pigeon Hole Principle

defined on the $n\times n$ grid where $n$ is odd.

We are interested in the case where each formula

in the proof is a depth $d$ formula in the basis given by

$\land$, $\lor$, and $\neg$. We prove that ...
more >>>