A general framework for parameterized proof complexity was introduced by Dantchev, Martin, and Szeider (FOCS'07). In that framework the parameterized version of any proof system is not fpt-bounded for some technical reasons, but we remark that this question becomes much more interesting if we restrict ourselves to those parameterized contradictions ... more >>>

In this note we show that the asymmetric Prover-Delayer game developed by Beyersdorff, Galesi, and Lauria (ECCC TR10-059) for Parameterized Resolution is also applicable to other tree-like proof systems. In particular, we use this asymmetric Prover-Delayer game to show a lower bound of the form $2^{\Omega(n\log n)}$ for the pigeonhole ... more >>>

Parameterized Resolution and, moreover, a general framework for parameterized proof complexity was introduced by Dantchev, Martin, and Szeider (FOCS'07). In that paper, Dantchev et al. show a complexity gap in tree-like Parameterized Resolution for propositional formulas arising from translations of first-order principles.
We broadly investigate Parameterized Resolution obtaining the following ... more >>>

One of the starting points of propositional proof complexity is the seminal paper by Cook and Reckhow (JSL 79), where they defined
propositional proof systems as poly-time computable functions which have all propositional tautologies as their range. Motivated by provability consequences in bounded arithmetic, Cook and Krajicek (JSL 07) have ... more >>>

In this paper we investigate the following two questions:

Q1: Do there exist optimal proof systems for a given language L?
Q2: Do there exist complete problems for a given promise class C?

For concrete languages L (such as TAUT or SAT and concrete promise classes C (such as NP ... more >>>

Motivated by strong Karp-Lipton collapse results in bounded arithmetic, Cook and Krajicek have recently introduced the notion of propositional proof systems with advice.
In this paper we investigate the following question: Do there exist polynomially bounded proof systems with advice for arbitrary languages?
Depending on the complexity of the ... more >>>

In this paper we ask the question whether the extended Frege proof
system EF satisfies a weak version of the deduction theorem. We
prove that if this is the case, then complete disjoint NP-pairs
exist. On the other hand, if EF is an optimal proof system, then
more >>>

Disjoint NP-pairs are a well studied complexity theoretic concept with
important applications in cryptography and propositional proof
complexity.

In this paper we introduce a natural generalization of the notion of
disjoint NP-pairs to disjoint k-tuples of NP-sets for k>1.
We define subclasses of the class ... more >>>

For a proof system P we introduce the complexity class DNPP(P)
of all disjoint NP-pairs for which the disjointness of the pair is
efficiently provable in the proof system P.
We exhibit structural properties of proof systems which make the
previously defined canonical NP-pairs of these proof systems hard ... more >>>

We investigate the class of disjoint NP-pairs under different reductions.
The structure of this class is intimately linked to the simulation order
of propositional proof systems, and we make use of the relationship between
propositional proof systems and theories of bounded arithmetic as the main
tool of our analysis.
more >>>