On the automatizability of polynomial calculus

DOI10.1007/s00224-009-9195-5zbMath1211.03025OpenAlexW2153159703WikidataQ61732588 ScholiaQ61732588MaRDI QIDQ1959382

Massimo Lauria, Nicola Galesi

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

zbMATH Keywords

polynomial calculusproof complexityautomatizabilitydegree lower bound

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity of proofs (03F20)

Related Items (4)

Towards NP-P via proof complexity and search ⋮ A Framework for Space Complexity in Algebraic Proof Systems ⋮ Short Proofs Are Hard to Find ⋮ Another look at degree lower bounds for polynomial calculus

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

This page was built for publication: On the automatizability of polynomial calculus