Questions tagged [proof-complexity]

Proof complexity is the field aiming to understand and analyse the computational resources that are required to prove or refute statements.

5 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
5 votes
0 answers
259 views

Is there a program for theory of incompleteness in NP?

Motivated by Suresh's post, Techniques for showing that problem is in hardness limbo, it seems that there might be an underlying theory that explains why some of these problems can not be complete for ...
Mohammad Al-Turkistany's user avatar
3 votes
0 answers
59 views

Explicit tautologies requiring lots/few uses of modus ponens in minimal proofs

I am interested in minimal length proofs of tautologies in propositional logic. For concreteness, let's fix a particular Frege system $F$ (i.e., sound and complete set of axioms and deduction rules ...
Sprotte's user avatar
  • 1,065
3 votes
0 answers
129 views

Lengths of proofs and quasilinear time

Length of proofs depends not only on the theory but also on its axiomatization. Once an axiomatization is fixed, typical proof systems are equivalent up to a polynomial factor. But what if we care ...
Dmytro Taranovsky's user avatar
3 votes
0 answers
253 views

Oracle separating FIP for bounded-depth Frege from FIP for Frege (and hardness conditions on DDH)

Is there an oracle such that in the relativized world, bd-Frege (bounded depth Frege propositional proof system) has FIP (feasible interpolation property) but Frege does not have FIP? Such an oracle ...
Kaveh's user avatar
  • 5,362
0 votes
0 answers
82 views

1-degree SOS proof refutes Linear Programming

I am trying to understand Sums-of-Squares proof systems. A degree $d$ Sums-of-Squares refutation for a set of polynomial equations $P = \{p_1(x) = 0, ..., p_m(x) = 0\}$ is defined as $\sum_{i=1}^m g_i(...
Tom Keaton's user avatar