21
votes
Accepted
Algebraic equivalent of SAT?
This is standard and widely used in computer science theory.
There are many references that use boolean polynomials with False -> 0 and True -> 1, or in other words, a polynomial over GF(2) used ...
- 11.1k
19
votes
Graph theoretic restriction to Proofs in Proof Complexity Theory
The most natural restriction on the proof DAG is that it be a tree – that is, any "lemma" (intermediate conclusion) is not used more than once. This property is called being "tree-like". General ...
- 14.2k
14
votes
Accepted
Lower Bounds for Frege and Extended Frege
1, 2, 4) The best known lower bounds on extended Frege are the same as for Frege: linear number of lines, and quadratic size. This applies e.g. to the tautologies $\neg^{2n}\top$ (basically, any ...
- 15.4k
11
votes
Algebraic equivalent of SAT?
I think what you are asking about is also known as "polynomial calculus" in proof complexity and SAT solving. It was introduced in [1, 2] to investigate whether coNP can be separated from NP ...
- 10.6k
9
votes
Are there any propositional proof systems which are not Cook-Reckhow proof systems?
Natural examples of propositional proof systems that do not fall under this definition are algebraic proof systems where the lines in the proof are arbitrary polynomials (not necessarily fully ...
- 4,531
8
votes
Graph theoretic restriction to Proofs in Proof Complexity Theory
Müller and Szeider study Resolution proofs where the proof DAG has bounded tree-width or bounded path-width (for suitable extensions of these graph complexity measures to directed graphs.)
They show ...
- 4,531
7
votes
Accepted
Resolution augmented with the rule of symmetry or the rule of extension
First, ER p-simulates SR: for example, ER is p-equivalent to the extended Frege proof system (EF) which is p-equivalent to the substitution Frege proof system (SF), and it is easy to see that SF p-...
- 15.4k
6
votes
Accepted
Document references describing weaknesses for cutting planes and algebraic proof system?
For each of these proof systems we know that there are some formulas where the shortest proof needs to have exponential length. Some of the earliest examples are an exponential lower bound for the ...
- 186
6
votes
Accepted
Axioms of Minimum Size Resolution Refutations
With the caveat that I am posting this quickly in a sleep-deprived state, I think the answer is "no" to all three questions.
Take the pigeonhole principle formulas PHP^m_n for m pigeons and n holes. ...
- 484
6
votes
Accepted
Is there any work relating type systems and Cook-Reckhow proof systems?
Cook-Reckhow propositional proof systems are nonunifrom.
E.g. the computational complexity counterpart to
the class of polynomial-size $\mathsf{Extended Frege}$ proofs is
the nonuniform complexity ...
- 21.3k
6
votes
On the (Cook) definition of a propositional proof system
$f$ is not a prover, it's a proof-checker. $w$ is the proof. And the polynomial is a polynomial of the length of the proof, which could be much larger than the length of the thing being proved. If you ...
- 50.5k
6
votes
Graph theoretic restriction to Proofs in Proof Complexity Theory
For strong enough proof systems the graph representation of a proof in the system seems less consequential, since (as Joshua Grochow already commented), DAG-like and tree-like Frege proofs are ...
- 1,889
4
votes
On the difference between propositional proof system and polynomially-bounded proof system
In Cook-Reckhow propositional proof systems
proof checkers have to run in polynomial time
w.r.t. the size of their input.
The size of the input is the size of the proof.
This is generally not a ...
- 21.3k
4
votes
Accepted
Is there a relation between the techniques used by Dan Willard, versus those of Brown and Palsberg, to exclude diagonalization?
I'll defer if someone more knowledgeable on the subject arrives, but I think the answer is that they are not the same.
Willard's work is about building theories that avoid the typical formulation of ...
- 816
3
votes
Construct proof systems for common algorithmic task, like equivalence of regular expressions
You have a non-deterministic algorithm deciding the problem.
If you want to think of it as a proof system for $EQUIV$, then
the proof of $(u,v) \in EQUIVE$ is just the string
representing the ...
- 21.3k
3
votes
IPS upper bound for subset sum axiom
First, Kaveh is correct that the verification for IPS is randomized, so all it would show is $\mathsf{NP} \subseteq \mathsf{coAM}$ (not $\mathsf{NP} = \mathsf{coNP}$). However, this alone would still ...
- 36.3k
3
votes
Natural NP-complete problems with "large" witnesses
As for your first question, Allender states (in Amplifying Lower Bounds by Means of Self-Reducibility) that no natural NP-complete problem is known to lie outside of NTIME(n). This means that all ...
- 20.7k
2
votes
Are there any propositional proof systems which are not Cook-Reckhow proof systems?
Assume that you have an algorithm $A$ which satisfies soundness and completeness. You can define a new proof checker which is sound, complete, and runs in polynomial time: it checks if a given $\pi$ ...
- 21.3k
2
votes
IPS upper bound for subset sum axiom
I think what you are missing is probably the complexity of the proof verification algorithm for IPS.
It is generally true that if we have a Cook-Reckhow proof system and have short proofs for a coNP-...
- 21.3k
2
votes
Construct proof systems for common algorithmic task, like equivalence of regular expressions
Kaveh's response exemplifies well the Cook-Reckhow notion of an abstract proof system. Nonetheless, for comparison, I point to a recent preprint of mine and Damien Pous:
A cut-free cyclic proof ...
- 121
2
votes
Accepted
In regards to the tautologies of a polynomially-bounded propositional proof system
Your question is like asking what is the class of formulas for the problem SAT?
In the definition of SAT it is fixed to some fixed class,
say those based on $\{\lnot, \land, \lor\}$
but it doesn't ...
- 21.3k
2
votes
Accepted
Proof of SPFA's worst-case complexity?
Here's the algorithm (from the wikipedia page) then a proof of the time bound:
...
- 9,380
1
vote
Accepted
Eliminating tautological axioms in tree-like $k$-DNF resolution
Since I could not find a proof in the literature, I wrote a short note containing the proof.
- 4,531
1
vote
Accepted
Is mathematical proof itself NP-hard?
Here is a link to some lecture notes that answer my question - http://www.cs.cornell.edu/~sabhar/publications/iaspcmi-proofcomplexity00.pdf
Proof complexity is a vast field of mathematics.
- 119
1
vote
Resolution vs Nondeterministic Search Problems
If I understood correctly the question, the so-called Buss-Pudlak game provides a simple transformation from a proof system to such a decision tree (see Buss-Pudlak '94 http://math.cas.cz/%7Epudlak/...
- 1,889
1
vote
Natural NP-complete problems with "large" witnesses
Consider the following variant of the MAXCLIQUE problem.
Instance: A circuit $C$ with $2n$ input bits, and of polynomially bounded size in $n$. This circuit implicitly determines a graph on $2^n$ ...
- 10.8k
Only top scored, non community-wiki answers of a minimum length are eligible