Resolution over linear equations and multilinear proofs (Q952492): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/j.apal.2008.04.001 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W1982672583 / rank | |||
Normal rank |
Revision as of 03:08, 20 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Resolution over linear equations and multilinear proofs |
scientific article |
Statements
Resolution over linear equations and multilinear proofs (English)
0 references
12 November 2008
0 references
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)].
0 references
proof complexity
0 references
resolution
0 references
algebraic proof systems
0 references
multilinear proofs
0 references
cutting planes
0 references
feasible interpolation
0 references