Resolution over linear equations and multilinear proofs (Q952492)

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)].