On the automatizability of polynomial calculus
From MaRDI portal
Publication:1959382
DOI10.1007/s00224-009-9195-5zbMath1211.03025WikidataQ61732588 ScholiaQ61732588MaRDI QIDQ1959382
Publication date: 6 October 2010
Published in: Theory of Computing Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00224-009-9195-5
03B35: Mechanization of proofs and logical operations
68Q17: Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
03F20: Complexity of proofs
Related Items
Short Proofs Are Hard to Find, Towards NP-P via proof complexity and search, Another look at degree lower bounds for polynomial calculus, A Framework for Space Complexity in Algebraic Proof Systems
Cites Work
- The intractability of resolution
- Lower bounds for the polynomial calculus
- On reducibility and symmetry of disjoint NP pairs.
- Lower bounds for polynomial calculus in the case of nonbinomial ideals.
- Non-automatizability of bounded-depth Frege proofs
- On the automatizability of resolution and related propositional proof systems
- An exponential separation between the parity principle and the pigeonhole principle
- Lower bounds for the polynomial calculus and the Gröbner basis algorithm
- Optimality of size-degree tradeoffs for polynomial calculus
- Resolution Is Not Automatizable Unless W[P Is Tractable]
- Short proofs are narrow—resolution made simple
- On Interpolation and Automatization for Frege Systems
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item