Proof Complexity of Modal Resolution

Journal of Automated Reasoning - We investigate the proof complexity of modal resolution systems developed by Nalon and Dixon (J Algorithms 62(3–4):117–134, 2007) and Nalon et al. (in:...     

Tuples of Disjoint $\mathsf{NP}$ -Sets

Disjoint -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 -pairs to disjoint k-tuples of -sets for k≥2. We define subclasses of the class of all disjoint k-tuples of -sets. These subclasses are associated with a propositional proof system and possess complete tuples which are defined from the proof system. In our main result we show that complete disjoint -pairs exist if and only if complete disjoint k-tuples of -sets exist for all k≥2. Further, this is equivalent to the existence of a propositional proof system in which the disjointness of all k-tuples is shortly provable. We also show that a strengthening of this conditions characterizes the existence of optimal proof systems. An extended abstract of this paper appeared in the proceedings of the conference CSR 2006 (Lecture Notes in Computer Science 3967, 80–91, 2006). Supported by DFG grant KO 1053/5-1.     

A lower bound for the pigeonhole principle in tree-like Resolution by asymmetric Prover-Delayer games

In this note we show that the asymmetric Prover-Delayer game developed in Beyersdorff et al. (2010) [2] 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 ²Ω(nlogn) for the pigeonhole principle in tree-like Resolution. This gives a new and simpler proof of the same lower bound established by Iwama and Miyazaki (1999) [7] and Dantchev and Riis (2001) [5].     

The complexity of propositional implication

The question whether a set of formulae Γ implies a formula φ is fundamental. The present paper studies the complexity of the above implication problem for propositional formulae that are built from a systematically restricted set of Boolean connectives. We give a complete complexity-theoretic classification for all sets of Boolean functions in the meaning of Post's lattice and show that the implication problem is efficiently solvable only if the connectives are definable using the constants {0,1} and only one of {∧,∨,⊕}. The problem remains coNP-complete in all other cases. We also consider the restriction of Γ to singletons which makes the problem strictly easier in some cases.     

Proof systems that take advice

One of the starting points of propositional proof complexity is the seminal paper by Cook and Reckhow [J. Symbolic Logic, 1979], 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 Kraj?´?ek [J. Symbolic Logic, 2007] have recently started the investigation of proof systems which are computed by poly-time functions using advice.In this paper we concentrate on three fundamental questions regarding this new model. First, we investigate whether a given language L admits a polynomially bounded proof system with advice. Depending on the complexity of the underlying language L and the amount and type of the advice used by the proof system, we obtain different characterizations for this problem. In particular, we show that this question is tightly linked with the question whether L has small nondeterministic instance complexity.The second question concerns the existence of optimal proof systems with advice. For propositional proof systems, Cook and Kraj?´?ek gave a surprising positive answer which we extend to all languages.These results show that providing proof systems with advice yields a more powerful model, but this model is also less directly applicable in practice. Our third question therefore asks whether the usage of advice in propositional proof systems can be simplified or even eliminated. While in principle, the advice can be very complex, we show that propositional proof systems with logarithmic advice are also computable in poly-time with access to a sparse NP-oracle. Employing a recent technique of Buhrman and Hitchcock [CCC, 2008] we also manage to transfer the advice from the proof to the proven formula, which leads to a more practical computational model.     

Lower Bound Techniques for QBF Expansion

Theory of Computing Systems - We propose some general techniques for proving lower bounds in expansion-based QBF proof systems. We present them in a framework centred on natural properties of...     

The Deduction Theorem for Strong Propositional Proof Systems

This paper focuses on the deduction theorem for propositional logic. We define and investigate different deduction properties and show that the presence of these deduction properties for strong proof systems is powerful enough to characterize the existence of optimal and even polynomially bounded proof systems. We also exhibit a similar, but apparently weaker condition that implies the existence of complete disjoint NP\mathsf{NP} -pairs. In particular, this yields a sufficient condition for the completeness of the canonical pair of Frege systems and provides a general framework for the search for complete NP\mathsf{NP} -pairs.