Characterizing propositional proofs as noncommutative formulas
From MaRDI portal
Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Classical propositional logic (03B05) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Complexity of proofs (03F20) Complexity of computation (including implicit computational complexity) (03D15)
Abstract: Does every Boolean tautology have a short propositional-calculus proof? Here, a propositional calculus (i.e. Frege) proof is a proof starting from a set of axioms and deriving new Boolean formulas using a set of fixed sound derivation rules. Establishing any super-polynomial size lower bound on Frege proofs (in terms of the size of the formula proved) is a major open problem in proof complexity, and among a handful of fundamental hardness questions in complexity theory by and large. Non-commutative arithmetic formulas, on the other hand, constitute a quite weak computational model, for which exponential-size lower bounds were shown already back in 1991 by Nisan [Nis91] who used a particularly transparent argument. In this work we show that Frege lower bounds in fact follow from corresponding size lower bounds on non-commutative formulas computing certain polynomials (and that such lower bounds on non-commutative formulas must exist, unless NP=coNP). More precisely, we demonstrate a natural association between tautologies to non-commutative polynomials , such that: if has a polynomial-size Frege proof then has a polynomial-size non-commutative arithmetic formula; and conversely, when is a DNF, if has a polynomial-size non-commutative arithmetic formula over then has a Frege proof of quasi-polynomial size.
Recommendations
Cites work
- scientific article; zbMATH DE number 5845490 (Why is no real title available?)
- scientific article; zbMATH DE number 4008289 (Why is no real title available?)
- scientific article; zbMATH DE number 3651744 (Why is no real title available?)
- scientific article; zbMATH DE number 3461412 (Why is no real title available?)
- scientific article; zbMATH DE number 3583767 (Why is no real title available?)
- scientific article; zbMATH DE number 1256733 (Why is no real title available?)
- scientific article; zbMATH DE number 1059248 (Why is no real title available?)
- scientific article; zbMATH DE number 1559592 (Why is no real title available?)
- scientific article; zbMATH DE number 806744 (Why is no real title available?)
- scientific article; zbMATH DE number 819737 (Why is no real title available?)
- scientific article; zbMATH DE number 1390276 (Why is no real title available?)
- Algebraic proof systems over formulas.
- Algebraic proofs over noncommutative formulas
- An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams
- An exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle
- Circuit complexity, proof complexity, and polynomial identity testing. The ideal proof system
- Deterministic polynomial identity testing in non-commutative models
- Dual weak pigeonhole principle, pseudo-surjective functions, and provability of circuit lower bounds
- Exponential lower bounds for the pigeonhole principle
- Fast Probabilistic Algorithms for Verification of Polynomial Identities
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Logical foundations of proof complexity
- Lower Bounds on Hilbert's Nullstellensatz and Propositional Proofs
- Lower bounds on the size of bounded depth circuits over a complete basis with logical addition
- Monotone simulations of non-monotone proofs.
- Multi-linear formulas for permanent and determinant are of super-polynomial size
- Non-commutative arithmetic circuits with division
- On Interpolation and Automatization for Frege Systems
- Principles and Practice of Constraint Programming – CP 2004
- Proof complexity in algebraic systems and bounded depth Frege systems with modular counting
- Pseudorandom Generators in Propositional Proof Complexity
- Pseudorandom generators hard for \(k\)-DNF resolution and polynomial calculus resolution
- Quasipolynomial size Frege proofs of Frankl's theorem on the trace of sets
- Resolution over linear equations and multilinear proofs
- Separation of multilinear circuit and formula size
- Short Proofs for the Determinant Identities
- Tensor-rank and lower bounds for arithmetic formulas
- The Parallel Evaluation of General Arithmetic Expressions
- The relative efficiency of propositional proof systems
- The strength of multilinear proofs
- Uniform, integral and efficient proofs for the determinant identities
- Unsolvable systems of equations and proof complexity
- Untersuchungen über das logische Schliessen. II
- Witnessing matrix identities and proof complexity
Cited in
(10)- Semialgebraic proofs, IPS lower bounds, and the -conjecture: can a natural number be negative?
- scientific article; zbMATH DE number 6829288 (Why is no real title available?)
- Proof complexity lower bounds from algebraic circuit complexity
- Formal proofs of operator identities by a single formal computation
- Circuit complexity, proof complexity, and polynomial identity testing. The ideal proof system
- Algebraic proofs over noncommutative formulas
- Algebraic proofs over noncommutative formulas
- Towards PNP from extended Frege lower bounds
- scientific article; zbMATH DE number 7471587 (Why is no real title available?)
- scientific article; zbMATH DE number 786497 (Why is no real title available?)
This page was built for publication: Characterizing propositional proofs as noncommutative formulas
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4577770)
