Given a sound first-order p-time theory $T$ capable of formalizing syntax of
first-order logic we define a p-time function $g_T$ that stretches all inputs by one
bit and we use its properties to show that $T$ must be incomplete. We leave it as an
open problem whether ... more >>>

For a finite set $\cal F$ of polynomials over a fixed finite prime field of size $p$ containing all polynomials $x^2 - x$, a Nullstellensatz proof of the unsolvability of the system
$$
f = 0\ ,\ \mbox{ all } f \in {\cal F}
$$
is a linear combination ... more >>>

The working conjecture from K'04 that there is a proof complexity generator hard for all
proof systems can be equivalently formulated (for p-time generators) without a reference to proof complexity notions
as follows:
\begin{itemize}
\item There exist a p-time function $g$ extending each input by one bit such that its ... more >>>

We study from the proof complexity perspective the (informal) proof search problem:
Is there an optimal way to search for propositional proofs?
We note that for any fixed proof system there exists a time-optimal proof search algorithm. Using classical proof complexity results about reflection principles we prove that a time-optimal ... more >>>

Proving that there are problems in $P^{NP}$ that require boolean circuits of super-linear size is a major frontier in complexity theory. While such lower bounds are known for larger complexity classes, existing results only show that the corresponding problems are hard on infinitely many input lengths. For instance, proving almost-everywhere ... more >>>

We establish unconditionally that for every integer $k \geq 1$ there is a language $L \in P$ such that it is consistent with Cook's theory PV that $L \notin SIZE(n^k)$. Our argument is non-constructive and does not provide an explicit description of this language.

We give a general reduction of lengths-of-proofs lower bounds for
constant depth Frege systems in DeMorgan language augmented by
a connective counting modulo a prime $p$
(the so called $AC^0[p]$ Frege systems)
to computational complexity
lower bounds for search tasks involving search trees branching upon
values of linear maps on ... more >>>

Let $g$ be a map defined as the Nisan-Wigderson generator
but based on an $NP \cap coNP$-function $f$. Any string $b$ outside the range of
$g$ determines a propositional tautology $\tau(g)_b$ expressing this
fact. Razborov \cite{Raz03} has conjectured that if $f$ is hard on average for
P/poly then these ... more >>>