Algebraic proofs over noncommutative formulas

DOI10.1007/978-3-642-13562-0_7zbMATH Open1284.03262arXiv1004.2159OpenAlexW2163168463MaRDI QIDQ3569064FDOQ3569064

Authors: Iddo Tzameret 

Publication date: 17 June 2010

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Abstract: We study possible formulations of algebraic propositional proof systems operating with noncommutative formulas. We observe that a simple formulation gives rise to systems at least as strong as Frege---yielding a semantic way to define a Cook-Reckhow (i.e., polynomially verifiable) algebraic analog of Frege proofs, different from that given in [BIKPRS96,GH03]. We then turn to an apparently weaker system, namely, polynomial calculus (PC) where polynomials are written as ordered formulas (PC over ordered formulas, for short): an ordered polynomial is a noncommutative polynomial in which the order of products in every monomial respects a fixed linear order on variables; an algebraic formula is ordered if the polynomial computed by each of its subformulas is ordered. We show that PC over ordered formulas is strictly stronger than resolution, polynomial calculus and polynomial calculus with resolution (PCR) and admits polynomial-size refutations for the pigeonhole principle and the Tseitin's formulas. We conclude by proposing an approach for establishing lower bounds on PC over ordered formulas proofs, and related systems, based on properties of lower bounds on noncommutative formulas. The motivation behind this work is developing techniques incorporating rank arguments (similar to those used in algebraic circuit complexity) for establishing lower bounds on propositional proofs.

Full work available at URL: https://arxiv.org/abs/1004.2159

Recommendations

• Algebraic proofs over noncommutative formulas
• Characterizing propositional proofs as noncommutative formulas
• Algebraic proof systems over formulas.
• scientific article; zbMATH DE number 6829288
• Lower bounds for the polynomial calculus

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity of proofs (03F20)

Cited In (3)

• Characterizing propositional proofs as noncommutative formulas
• Algebraic proofs over noncommutative formulas
• Algebraic proof systems over formulas.

This page was built for publication: Algebraic proofs over noncommutative formulas

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3569064)