Système de preuve de somme des carrés

Récemment, j'ai vu plusieurs articles sur arxiv qui se réfèrent à un système de preuve appelé somme des carrés.

Quelqu'un peut-il expliquer ce qu'est une preuve de somme des carrés et pourquoi ces preuves sont importantes / intéressantes?

Comment sont-ils liés à d'autres systèmes de preuve algébriques? S'agit-il d'une sorte de dualité avec Lassere?

Le système de preuve de somme des carrés de base, introduit sous le nom de réfutations Positivstellensatz par Grigoriev et Vorobjov , est un système de preuve «statique» pour montrer qu'un ensemble d'équations et d'inéquations polynomiales où f 1 , … , f k , h 1 , …

$$S=\{f_1=0,\dots,f_k=0,h_1\ge0,\dots,h_m\ge0\},$$ , n'a pas de solution commune dans R n : une réfutation de S est donnée par les polynômes g i et e I , j tels que - 1 = k ∑ i = 1 g i f i + ∑ I ⊆ { 1 , … , m } ∑ j e 2 $f_1,\dots,f_k,h_1,\dots,h_m\in\mathbb R[x_1,\dots,x_n]$$\mathbb R^n$$S$$g_i$$e_{I,j}$ (On pourrait travailler avec n'importe quel champ fermé réel à la place deR.) Le Positivstellensatz de Stengle garantit queSa une réfutation si et seulement s'il n'a pas de solution. La principale mesure de complexité ici est ledegréde la réfutation, qui est le maximum des degrés totaux des polynômes qui apparaissent sous les signes de somme dans(∗), c'est-à-diregifiete2I,j∏i∈Ihi. $$\tag{$*$}-1=\sum_{i=1}^kg_if_i+\sum_{I\subseteq\{1,\dots,m\}}\sum_je_{I,j}^2\prod_{i\in I}h_i.$$ $\mathbb R$$S$$(*)$$g_if_i$$e_{I,j}^2\prod_{i\in I}h_i$

Comme d'habitude avec les systèmes de preuve algébriques, on peut également le considérer comme un système de réfutation pour les formules booléennes insatisfaisantes en incluant dans S les axiomes x 2 i - x i pour chaque variable x i , et une traduction de ϕ par les inégalités polynomiales.$\phi$$S$$x_i^2-x_i$$x_i$$\phi$

Plus d'informations sur l'histoire et le développement des systèmes SOS sont disponibles sur http://arxiv.org/abs/1211.1958 .

$p(\vec{x}) \geq 0$$p(\vec{x})$$\vec{x}$

Les règles d'inférence sont les suivantes:

1. $\over x^2-x \geq 0$
2. $\over x-x^2 \geq 0$
3. $\over p(\vec{x})^2\geq 0$
4. $p(\vec{x}) \geq 0 \over p(\vec{x})x \geq 0$
5. $p(\vec{x}) \geq 0 \over p(\vec{x})(1-x) \geq 0$
6. $p_1(\vec{x}) \geq 0, \cdots, p_m(\vec{x}) \geq 0 \over \sum_{i=1}^m c_ip_i(\vec{x}) \geq 0$$c_1, \cdots, c_m \in \mathbb{R}^+$

$p(\vec{x})^2\geq 0$

Il existe de bonnes connexions avec des algorithmes de programmation et d'approximation semi-définis.

Pour en savoir plus, consultez la récente conférence d' Albert Atserias à l'atelier BIRS Fondements théoriques de la résolution SAT appliquée :

• Albert Atserias , Mini-Tutorial on Semi-Algebraic Proof Systems ( slides ), 2014