First-Order Reasoning and Efficient Semi-Algebraic Proofs

被引:1
作者
Part, Fedor [1 ,2 ]
Thapen, Neil [2 ]
Tzameret, Iddo [3 ]
机构
[1] Czech Acad Sci, JetBrains Res, Prague, Czech Republic
[2] Czech Acad Sci, Inst Math, Prague, Czech Republic
[3] Imperial Coll London, Dept Comp, London, England
来源
2021 36TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS) | 2021年
关键词
LOWER BOUNDS; COMPLEXITY; NULLSTELLENSATZ; SYSTEMS;
D O I
10.1109/LICS52264.2021.9470546
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Semi-algebraic proof systems such as sum-ofsquares (SoS) have attracted a lot of attention recently due to their relation to approximation algorithms [3]: constant degree semi-algebraic proofs lead to conjecturally optimal polynomial-time approximation algorithms for important NP-hard optimization problems (cf. [4]). Motivated by the need to allow a more streamlined and uniform framework for working with SoS proofs than the restrictive propositional level, we initiate a systematic first-order logical investigation into the kinds of reasoning possible in algebraic and semi-algebraic proof systems. Specifically, we develop first-order theories that capture in a precise manner constant degree algebraic and semi-algebraic proof systems: every statement of a certain form that is provable in our theories translates into a family of constant degree polynomial calculus or SoS refutations, respectively; and using a reflection principle, the converse also holds. This places algebraic and semi-algebraic proof systems in the established framework of bounded arithmetic, while providing theories corresponding to systems that vary quite substantially from the usual propositional-logic ones. We give examples of how our semi-algebraic theory proves statements such as the pigeonhole principle, we provide a separation between algebraic and semi-algebraic theories, and we describe initial attempts to go beyond these theories by introducing extensions that use the inequality symbol, identifying along the way which extensions lead outside the scope of constant degree SoS. Moreover, we prove new results for propositional proofs, and specifically extend Berkholz's [7] dynamic-by-static simulation of polynomial calculus (PC) by SoS to PC with the radical rule.
引用
收藏
页数:13
相关论文
共 32 条
[1]  
Alekseev Y, 2020, Arxiv, DOI arXiv:2010.05660
[2]  
[Anonymous], 1995, ENCY MATH ITS APPL
[3]  
Barak B, 2012, STOC'12: PROCEEDINGS OF THE 2012 ACM SYMPOSIUM ON THEORY OF COMPUTING, P307
[4]  
Barak Boaz, 2014, Sum of squares upper bounds, lower bounds, and open questions
[5]  
Beame P, 1996, P LOND MATH SOC, V73, P1
[6]  
Beckmann Arnold, ACM T COMPUT LOG, VI, pVI
[7]   The Relation between Polynomial Calculus, Sherali-Adams, and Sum-of-Squares Proofs [J].
Berkholz, Christoph .
35TH SYMPOSIUM ON THEORETICAL ASPECTS OF COMPUTER SCIENCE (STACS 2018), 2018, 96
[8]  
Buss SR, 2015, T AM MATH SOC, V367, P7517
[9]  
Buss Samuel R., 1986, BOUNDED ARITHMETIC, V3, pI
[10]  
Buss Sr, 1998, STUD LOGIC, V137, P1