<p>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. </p>

CC BY-SA 4.0
2020-03-24T19:15:29.657Z
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
CC BY-SA 4.0
2020-03-25T09:12:02.020Z
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
CC BY-SA 4.0
2020-03-25T10:22:16.860Z
@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
CC BY-SA 4.0
2020-03-25T10:41:43.223Z
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
CC BY-SA 4.0
2020-03-25T14:37:01.963Z
@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
<cc.complexity-theory><reference-request><proof-complexity>
Proof systems induced by NP-complete problems
Mohammad Al-Turkistany
# Proof systems induced by NP-complete problems

(Asked by: username_0 on 2020-03-24)

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.

**Tags:** cc.complexity-theory, reference-request, proof-complexity

> **Comments:**
> **username_1**: 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$.  
> **username_2**: 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.  
> **username_0**: @JanJohannsen   Hajos calculus for non-k-colorability is interesting. I would be interested in techniques that generate proof systems from other coNP-complete problems.  
> **username_2**: 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.  
> **username_3**: @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.  

---

## 0 answers

