On the automatizability of polynomial calculus

DOI10.1007/s00224-009-9195-5zbMath1211.03025WikidataQ61732588 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 calculus; proof complexity; automatizability; degree lower bound

Mathematics Subject Classification ID

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

Towards NP-P via proof complexity and search, A Framework for Space Complexity in Algebraic Proof Systems

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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