Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 1004.2159

Algebraic Proofs over Noncommutative Formulas

Iddo Tzameret
View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

cs.CC

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Iddo Tzameret. 2010-08-01. Algebraic Proofs over Noncommutative Formulas. https://arxiv.org/abs/1004.2159

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Explicit unbalanced 1-expanders with small degree and right size

An explicit graph is given with left size $N$, left degree $\widetilde O(\log^2 N)$, right size $(1+o(1))K$ and $1$-expansion up to~$K$, meaning that every left subset of size $K' \le K$ has at least $K'$ neighbors. Let $\C(x)$ be the minimal length of a program that prints~$x$ (i.e., the central concept in Kolmogorov complexity). The $1$-expander is used to obtain an algorithm that on input $x$ computes in time $\poly(|x|)$ a list with $\widetilde O(|x|^3)$ programs such that at least 1 program prints $x$ and has length $\C(x) + O(1)$. This improves on the $O(|x|^{6+\eps})$ upper bound in~\cite{zim:c:shortlistshortproof} and is close to the $Ω(|x|^2)$ lower bound from~\cite[theorem 4]{bmvz:j:shortlist}. In the companion paper ``Online matching games in bipartite expanders: applications to data structures," the $1$-expander is used to obtain dynamic dictionaries in which the query operation has non-adaptive memory access.

cs.CC↗
arXiv2026

Gap Entropy and Almost Instance-Wise Optimal Best-Arm Identification

In the best-arm identification problem, we are given $n$ stochastic arms with unknown means and wish to identify the arm with the largest mean with probability at least $1-δ$, using as few samples as possible. We consider independent Gaussian rewards with unit variance and means in $[0,1]$. Chen and Li [2016] conjectured that the instance-wise sample complexity of this problem is characterized by the gap entropy, up to an additive term arising from the two-arm problem. In this paper, we resolve their gap-entropy and almost instance-wise optimality conjectures. For an instance $I$, let $Δ_{[i]}$ be the gap between the largest and the $i$-th largest mean, let $H(I)=\sum_{i=2}^{n}Δ_{[i]}^{-2}$, and let Ent$(I)$ denote the entropy of the normalized complexities of its dyadic gap groups. For every $0<δ<0.1$, we show that the order-oblivious instance-wise lower bound is $ Θ (H(I)[\log(1/δ)+Ent(I)]). $ We also give a single $δ$-correct algorithm with expected sample complexity $ O ( H(I)[\log(1/δ)+Ent(I)] +D\log(e+\log(e+D))),D=Δ_{[2]}^{-2}, $ without prior knowledge of the gaps. Our lower bound removes the dyadic-gap and monotonicity restrictions of previous work, and our upper bound removes the additional polylogarithmic factor multiplying the two-arm term. Thus, a single algorithm attains the instance-wise lower bound up to an additive two-arm term. The main theorems have been formalized and proved in Lean 4.

cs.CC↗