Resolution over linear equations and multilinear proofs
type: Item
instance of: scholarly article
title: Resolution over linear equations and multilinear proofs
zbMATH Open document ID: 1161.03034
author: Ran Raz
author: Iddo Tzameret
published in: Annals of Pure and Applied Logic
publication date: 2008-11-12T00:00:00Z
review text: The paper studies propositional proof systems combining resolution with the ability to work with linear equations. The authors introduce a proof system R(lin), which is a refutation system operating with disjunctions of linear equations with integer coefficients (written in unary) whose main inference rule is a kind of subtraction rule generalizing the resolution rule. They also consider its subsystem R\(^0\)(lin), which places certain restrictions on allowed proof lines. R(lin) is shown to be implicationally complete. The ability of the system to count is demonstrated by providing polynomial-size R\(^0\)(lin)-proofs of the pigeonhole principle and mod-\(p\) versions of Tseitin graph tautologies for constant-degree graphs. The paper also gives polynomial-size R(lin)-proofs of the clique-coloring tautologies for certain parameters, using a simulation of Res(2). In the next section, the authors prove feasible interpolation for R\(^0\)(lin) using the interpolation theorem for semantic derivations by \textit{J. Krajíček} [J. Symb. Log. 62, No.~2, 457--486 (1997; Zbl 0891.03029)] by constructing protocols for the Karchmer-Wigderson game. Another variant of feasible interpolation is also used to prove lower bounds on R\(^0\)(lin)-proofs of the clique-coloring tautologies, giving a superpolynomial separation between R\(^0\)(lin) and R(lin). Finally, the authors consider the relation of R(lin) to other proof systems. It is shown that R(lin) is polynomially simulated by the PCR proof system of \textit{M. Alekhnovich} et al. [SIAM J. Comput. 31, No.~4, 1184--1211 (2002; Zbl 1004.03047)], and R\(^0\)(lin) is polynomially simulated by multilinear proofs with depth-3 formulas [\textit{R. Raz} and \textit{I. Tzameret}, Comput. Complexity 17, No.~3, 407--457 (2008)]. On the other hand, R(lin) polynomially simulates the R(CP\(^*\)) proof system of \textit{J. Krajíček} [J. Symb. Log. 63, No.~4, 1582--1596 (1998; Zbl 0930.03081)].
reviewed by: Emil Jeřábek
Mathematics Subject Classification ID: 03F20
zbMATH DE Number: 5365124
zbMATH Keywords: proof complexity
zbMATH Keywords: resolution
zbMATH Keywords: algebraic proof systems
zbMATH Keywords: multilinear proofs
zbMATH Keywords: cutting planes
zbMATH Keywords: feasible interpolation
MaRDI profile type: Publication
full work available at URL: j.apal.2008.04.001
OpenAlex ID: W1982672583
cites work: Space Complexity in Propositional Calculus
cites work: The monotone circuit complexity of Boolean functions
cites work: Q4726174
cites work: Lower bounds for the weak pigeonhole principle and random formulas beyond resolution
cites work: Lower bounds for cutting planes proofs with small coefficients
cites work: Linear gaps between degrees for the polynomial calculus modulo distinct primes
cites work: Q4218929
cites work: The relative efficiency of propositional proof systems
cites work: The intractability of resolution
cites work: Several notes on the power of Gomory-Chvátal cuts
cites work: Monotone Circuits for Connectivity Require Super-Logarithmic Depth
cites work: Improved Lower Bounds for Tree-Like Resolution over Linear Inequalities
cites work: Lower bounds to the size of constant-depth propositional proofs
cites work: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
cites work: Discretely ordered modules as a first-order extension of the cutting planes proof system
cites work: On the weak pigeonhole principle
cites work: An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams
cites work: Lower bounds for resolution and cutting plane proofs and monotone computations
cites work: Q3758729
cites work: Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic
cites work: Q4737899
cites work: Multi-linear formulas for permanent and determinant are of super-polynomial size
cites work: Q3002768
cites work: The strength of multilinear proofs
cites work: Depth-3 arithmetic circuits over fields of characteristic zero
cites work: Q5593816
cites work: Q4393484
DOI: 10.1016/J.APAL.2008.04.001
Recommended article: Lower Bounds for Splittings by Linear Combinations
Recommended article: The strength of multilinear proofs
Recommended article: Q3680268
Recommended article: Circular (yet sound) proofs
Recommended article: Several notes on the power of Gomory-Chvátal cuts
Recommended article: Randomized feasible interpolation and monotone circuits with a local oracle
Recommended article: On linear rewriting systems for Boolean logic and some applications to proof theory
Recommended article: Q4828877
Recommended article: Q4283225
Recommended article: A feasible interpolation for random resolution
description: scientific article; zbMATH DE number 5365124