# 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.

21 questions
Filter by
Sorted by
Tagged with
1 vote
82 views

### Hardness of a Hybrid problem combining knapsack and scheduling

I am trying to prove whether the following problem is NP-hard or not: Items with a certain length arrive in a fixed sequence and must be assigned to one of two containers which are constrained in ...
580 views

### MIP*=RE theorem and its impact on logic and proof theory

In the monumental paper MIP*=RE five authors, Zhengfeng Ji, Anand Natarajan, Thomas Vidick, John Wright, and Henry Yuen, managed to show that two complexity classes: RE and MIP* do in fact coincide. ...
• 9,210
82 views

• 103
237 views

### Oracle queries asked in parallel

Definition: Assume that $\phi(q)$ is of the form $\exists y \leq 2^{p(n)} \varphi(q,y)$, where $p$ is a polynomial and $n = |q|$ (i.e. $n$ is the length of the binary representation of $q$). Then a ...
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 ...
134 views

### Results where complexity bounds implies finite number of test cases

We have all been there, when a formula works for the first 30 parameters, but it is not sufficient for a proof. My question is where one can actually just check a finite number of cases, to conclude ...
• 15.5k
1k views

### Finite versions of Godel' s incompleteness

Assume you have some notion of proof complexity: for instance, at the basic level, the length of a proof, or the number of symbols used, take your pick (there are more involved measures, but for sake ...
• 7,563
574 views

### Measure of progress towards a proof

Can one define some measure of progress towards a proof of a statement? I'm not sure if it's even possible for general first order logic statements so let's restrict ourselves to propositional ...
• 31
713 views

### Proof system with same complexity as "informal mathematics"?

The Completeness Theorem in first-order logic states that any mathematical validity is derivable from axioms. Hence, any informal mathematical proof (which is rigorous) can be translated into a formal ...
• 3,397
619 views

### Proof systems and their hierarchy

Why ZFC is placed in top of the proof system hierarchy? How it can p-simulate other systems?
• 41
252 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 ...
• 5,342