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 underlying ... 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 the weak deduction ... 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 of all disjoint k-tuples of ... 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 or ... 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. Specifically ... more >>>