# Proof systems induced by NP-complete problems

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.

• 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$. – Emil Jeřábek Mar 24 at 19:15
• 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. – Jan Johannsen Mar 25 at 9:12
• @JanJohannsen Hajos calculus for non-k-colorability is interesting. I would be interested in techniques that generate proof systems from other coNP-complete problems. – Mohammad Al-Turkistany Mar 25 at 10:22
• 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. – Jan Johannsen Mar 25 at 10:41
• @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. – holf Mar 25 at 14:37