First-order reasoning and efficient semi-algebraic proofs

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F25%3A00598223" target="_blank" >RIV/67985840:_____/25:00598223 - isvavai.cz</a>

Result on the web

<a href="https://doi.org/10.1016/j.apal.2024.103496" target="_blank" >https://doi.org/10.1016/j.apal.2024.103496</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1016/j.apal.2024.103496" target="_blank" >10.1016/j.apal.2024.103496</a>

Result language

angličtina

Original language name

First-order reasoning and efficient semi-algebraic proofs

Original language description

Semi-algebraic proof systems such as sum-of-squares (SoS) have attracted a lot of attention due to their relation to approximation algorithms: constant degree semi-algebraic proofs lead to conjecturally optimal polynomial-time approximation algorithms for important NP-hard optimization problems. 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 dynamic-by-static simulation of polynomial calculus (PC) by SoS to PC with the radical rule.

Czech name

—

Czech description

—

Type

J_imp - Article in a specialist periodical, which is included in the Web of Science database

CEP classification

—

OECD FORD branch

10101 - Pure mathematics

Project

<a href="/en/project/GA23-04825S" target="_blank" >GA23-04825S: Logic and unsatisfiability</a><br>

Continuities

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year

2025

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Name of the periodical

Annals of Pure and Applied Logic

ISSN

0168-0072

e-ISSN

1873-2461

Volume of the periodical

176

Issue of the periodical within the volume

1

Country of publishing house

NL - THE KINGDOM OF THE NETHERLANDS

Number of pages

36

Pages from-to

103496

UT code for WoS article

001282125600001

EID of the result in the Scopus database

2-s2.0-85199721877