# Questions tagged [proof-complexity]

propositional proof systems and corresponding bounded arithmetic theories

66 questions
Filter by
Sorted by
Tagged with
98 views

### Is there a relation between the techniques used by Dan Willard, versus those of Brown and Palsberg, to exclude diagonalization?

This question extends my inquiry from a previous post . Dan Willard's Self-Justifying Axiom Systems/Self-Verifying Theories  and Brown and Palsberg's self-interpreter for F-Omega  both employ ...
116 views

### Boolean logic: What is the name of this trick to replace explicit negations by implications?

Consider a Boolean circuit $C$ composed of some finite set of input variables $A_1,\ldots, A_n$ and the connectives $\lor\land\neg\rightarrow$ (with $X\rightarrow Y=\neg X\lor Y$) (update: assume that ...
91 views

### Algorithmically determining proof complexity for Frege systems?

I apologize if this falls wildly short of research level - I am just learning the very basics of proof complexity and lack any real logic background. Let $F$ be a Frege proof system (a finite complete ...
113 views

### Proof of SPFA's worst-case complexity?

I am trying to prove the worst-case asymptotic time complexity of the Shortest Path Faster Algorithm (SPFA). I know the complexity is the same as the "original" Bellman-Ford (BF) algorithm, ...
371 views

### Examples of simulations in proof complexity that are not p-simulations

I am writing a paper on the complexity of some unorthodox proof systems, where I have two systems $P$ and $Q$ such that $P$ simulates $Q$ in the sense of it being possible to translate a $Q$-proof ...
111 views

### Asymptotic complexity lower bounds of proof checking

This paper on universal search mentions (on pp. 6-7) that proof checking can be done in $O(n^2)$ where $n$ is the length of the proof. Is this optimal? I don't want to specify the problem too ...
160 views

### Is mathematical proof itself NP-hard?

At the 8:00 mark of this video, he claims that proving things is itself an NP problem. I'm looking for more insight into this. Could someone help explain this concept to me and also provide a link to ...
115 views

### Proof systems induced by NP-complete problems

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 ...
126 views

### Have the proofs in Buss's "On Goedel’s Theorems on Lengths of Proofs" been formalized (mechanically checked)?

The paper On Gödel's theorems on lengths of proofs I: Number of lines and speedup for arithmetics contains quite interesting results on proof length. But some of the details are still, to me, a bit ...
190 views

### Document references describing weaknesses for cutting planes and algebraic proof system?

Here, Fortnow says (section 4.3): Since then complexity theorists have shown similar weaknesses in a number of other proof systems including cutting planes, algebraic proof systems based on ...
141 views

### Eliminating tautological axioms in tree-like $k$-DNF resolution

The propositional proof system $k$-DNF-resolution, a.k.a. $Res(k)$, is a generalization of propositional resolution, where the lines in a proof are $k$-DNF formulas, i.e., disjunctions of $k$-terms of ...
101 views

### Axioms of Minimum Size Resolution Refutations

Let $\phi$ be an unsatisfiable CNF formula and let $\Pi$ be a resolution refutation of $\phi$ of minimum size. Let $\psi$ be the subformula of $\phi$ containing the clauses that actually appear as ...
247 views

1k views

### Automated theorem proving via unsupervised approaches

This question Where and how did computers help prove a theorem? considers some automated theorem proving successes. However they seem to be mostly supervised approaches, such as with the 4 color graph ...
371 views

### Proof Complexity and Circuit Lower bound for coNP

I have two questions (1)Circuit lower bound for coNP TAUT is a set of formulae such that any formula in TAUT is satisfied for all boolean assignments. UnSAT is the complement problem of SAT. It is ...
Let $R(f)$ and $ER(f)$ be the minimum-size for unsat proofs of $f$ in Resolution and Extended Resolution respectively. What's the best bound we have on $D=\min_f (R(f)-ER(f))$ where $f$ belongs to a ...
### Graph problems with good characterization but not known to be in $P$
A decision problem has good characterization if it is in $NP \cap coNP$. Many natural graph problems have good characterizations. For instance, Kuratuwski's Theorem gives good characterization of ...