33 citations · 176 across the 16 of their papers we have counts for
17 papers
On proof complexity generators
Jan Krajicek
Motivated by the theory of proof complexity generators we consider the following search problem $\mbox{DD}_P$ determined by a propositional proof system : given a -pr…
Extended Nullstellensatz proof systems
Jan Krajicek
For a finite set of polynomials over fixed finite prime field of size containing all polynomials a Nullstellensatz proof of the unsolvability of the system $…
On the existence of strong proof complexity generators
Jan Krajicek
Cook and Reckhow 1979 pointed out that NP is not closed under complementation iff there is no propositional proof system that admits polynomial size proofs of all tautologies. Theo…
Information in propositional proofs and algorithmic proof search
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 sys…
Small circuits and dual weak PHP in the universal theory of p-time algorithms
Jan Krajicek
We prove, under a computational complexity hypothesis, that it is consistent with the true universal theory of p-time algorithms that a specific p-time function extending bits…
A limitation on the KPT interpolation
Jan Krajíček
We prove a limitation on a variant of the KPT theorem proposed for propositional proof systems by Pich and Santhanam (2020), for all proof systems that prove the disjointness of tw…
The Cook-Reckhow definition
Jan Krajicek
The Cook-Reckhow 1979 paper defined the area of research we now call Proof Complexity. There were earlier papers which contributed to the subject as we understand it today, the mos…
Consistency of circuit lower bounds with bounded theories
Jan Bydzovsky, Jan Krajicek, Igor C. Oliveira
Proving that there are problems in that require boolean circuits of super-linear size is a major frontier in complexity theory. While such lower bounds are…
On monotone circuits with local oracles and clique lower bounds
Jan Krajicek, Igor C. Oliveira
We investigate monotone circuits with local oracles [K., 2016], i.e., circuits containing additional inputs that can perform unstructured computations on the i…
Randomized feasible interpolation and monotone circuits with a local oracle
Jan Krajicek
We generalize the feasible interpolation theorem for semantic derivations from K.(1997) by allowing randomized protocols (protocols in the sense of K.(1997). We also introduce an e…
Unprovability of circuit upper bounds in Cook's theory PV
Jan Krajicek, Igor C. Oliveira
We establish unconditionally that for every integer there is a language $L \in \mbox{P}$ such that it is consistent with Cook's theory PV that . Our…
A feasible interpolation for random resolution
Jan Krajicek
Random resolution, defined by Buss, Kolodziejczyk and Thapen (JSL, 2014), is a sound propositional proof system that extends the resolution proof system by the possibility to augme…
Consistency of circuit evaluation, extended resolution and total NP search problems
Jan Krajicek
We consider sets of narrow clauses expressing that no definition of a size circuit with inputs is refutable in resolution R in steps. We show that every CNF…
Expansions of pseudofinite structures and circuit and proof complexity
Jan Krajicek
I shall describe a general model-theoretic task to construct expansions of pseudofinite structures and discuss several examples of particular relevance to computational complexity.…
A reduction of proof complexity to computational complexity for Frege systems
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 (the so ca…
On the computational complexity of finding hard tautologies
Jan Krajicek
It is well-known (cf. K.-Pudlák 1989) that a polynomial time algorithm finding tautologies hard for a propositional proof system exists iff is not optimal. Such an algorith…
A saturation property of structures obtained by forcing with a compact family of random variables
Jan Krajicek
A method how to construct Boolean-valued models of some fragments of arithmetic was developed in Krajicek (2011), with the intended applications in bounded arithmetic and proof com…