All reports by Author Jan Krajicek:

__
TR23-030
| 21st March 2023
__

Jan Krajicek#### A proof complexity conjecture and the Incompleteness theorem

__
TR23-007
| 3rd February 2023
__

Jan Krajicek#### Extended Nullstellensatz proof systems

__
TR22-120
| 24th August 2022
__

Jan Krajicek#### On the existence of strong proof complexity generators

Revisions: 1
,
Comments: 1

__
TR21-053
| 13th April 2021
__

Jan Krajicek#### Information in propositional proofs and algorithmic proof search

__
TR19-077
| 30th May 2019
__

Jan Bydzovsky, Igor Carboni Oliveira, Jan Krajicek#### Consistency of circuit lower bounds with bounded theories

__
TR16-071
| 1st May 2016
__

Jan Krajicek, Igor Carboni Oliveira#### Unprovability of circuit upper bounds in Cook's theory PV

__
TR13-156
| 15th November 2013
__

Jan Krajicek#### A reduction of proof complexity to computational complexity for $AC^0[p]$ Frege systems

Revisions: 2

__
TR10-054
| 30th March 2010
__

Jan Krajicek#### On the proof complexity of the Nisan-Wigderson generator based on a hard $NP \cap coNP$ function

Jan Krajicek

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 >>>

Jan Krajicek

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 >>>

Jan Krajicek

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 >>>

Jan Krajicek

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 >>>

Jan Bydzovsky, Igor Carboni Oliveira, Jan Krajicek

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 >>>

Jan Krajicek, Igor Carboni Oliveira

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.

more >>>Jan Krajicek

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 >>>

Jan Krajicek

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 >>>