2
$\begingroup$

Satisfiability is the fundamental NP-complete problem. Cook-Reckhow theorem states that the existence of a propositional proof system that admits polynomial size proofs for all tautologies implies that NP=coNP. In principle, every NP-complete problem can encode Satisfiability problem. It seems to me that we should be able systematically generate a proof system from any NP-complete problem. The aim is that this may give new insights into proving proof complexity lower bounds. I am looking for references.

$\endgroup$
  • 5
    $\begingroup$ The Cook and Reckhow paper actually defines the notion of a proof system for an arbitrary language $L$, not just for TAUT: a proof system for $L$ is a polynomial-time function from some $\Sigma^*$ onto $L$. $\endgroup$ – Emil Jeřábek Mar 24 at 19:15
  • 2
    $\begingroup$ An NP-complete problem only gives us only a potential set of theorems, with a proof system that is trivially polynomially bounded, viz. its NP witnesses. For something interesting to happen, we need a co-NP complete problem as the set of theorems, for which proof systems can then be investigated. There are some proof systems studied for co-NP complete problems other than UNSAT or TAUT, e.g. the Hajos calculus for non-k-colorability. $\endgroup$ – Jan Johannsen Mar 25 at 9:12
  • $\begingroup$ @JanJohannsen Hajos calculus for non-k-colorability is interesting. I would be interested in techniques that generate proof systems from other coNP-complete problems. $\endgroup$ – Mohammad Al-Turkistany Mar 25 at 10:22
  • 1
    $\begingroup$ The proof systems cannot simply be "generated", it requires an original idea to come up with one. Just as e.g. Resolution is not just "generated" from the set UNSAT. $\endgroup$ – Jan Johannsen Mar 25 at 10:41
  • 2
    $\begingroup$ @JanJohannsen however, a correct deterministic algorithm for an NP problem has a natural proof system associated to it : the trace of the computation. Now, the trick is to clean that from a given algorithm to make something easily understandable. $\endgroup$ – holf Mar 25 at 14:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.