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.
22
questions
1
vote
0
answers
98
views
Effortless automated proofs for "simple" formulae?
From small cases to all of them. This is in the spirit of 15 theorem see https://en.wikipedia.org/wiki/15_and_290_theorems
EXAMPLE : Suppose you have the following problem: P(a)
For any fixed non ...
- 1,306
1
vote
2
answers
88
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 ...
- 21
6
votes
2
answers
939
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,240
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(...
9
votes
4
answers
2k
views
Computational complexity theoretic incompleteness: is that a thing?
Has anyone done research in an area that I have not heard of but that I want to call "Computational complexity theoretic incompleteness", which would mean not absolute incompleteness in the ...
- 193
3
votes
1
answer
83
views
Does extended Frege p-simulate circuit Frege with substitutions?
Consider propositional logic.
Frege systems are textbook-style proof systems, with a finite set of logically sound axioms and rules. However you can generalise each axiom/rule with substitutions, ...
- 33
3
votes
1
answer
1k
views
When do you get to the point of writing proofs that need to be so complicated that verifying the details becomes a great burden on others?
Keyword here is need, many people thought I meant this intentionally rather than as an inevitability. I recently reread the article on Fukaya's work at Quanta and looked into the situation a bit more ...
- 745
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 ...
- 1,065
5
votes
3
answers
606
views
Zero-knowledge proof for $P \ne NP$?
In computational complexity, $P \ne NP$ is a widely believed conjecture. Suppose that someone discovered a proof for it. He wants to publish a proof that he correctly proved the conjecture. I am aware ...
- 2,961
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 ...
- 6,365
10
votes
1
answer
849
views
Is there good reference for proof complexity?
I am asking if there are some good or standard references for proof complexity theory? I didn't find references when I search in internet. Thanks!
- 781
12
votes
2
answers
2k
views
Connections between Complexity Theory & Set Theory
Inspired by Joshua Grochow and Iddo Tzameret's answers in a post on http://cstheory.stackexchange.com , I would like to get more references on possible connections between complexity theory and set ...
10
votes
2
answers
612
views
Bounded Arithmetic vs Complexity Theory
In this post, when I talk about bounded arithmetic theories,
I mean the theories of arithmetic according to "Logical Foundations of Proof Complexity", which capture the complexity classes between $AC^...
- 103
7
votes
1
answer
247
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 ...
5
votes
0
answers
260
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 ...
- 2,961