Quadratsummen-Beweissystem

Kürzlich habe ich mehrere Artikel über arxiv gesehen, die sich auf ein Beweissystem beziehen, das als Quadratsumme bezeichnet wird.

Kann jemand erklären, was ein Quadratsummenbeweis ist und warum solche Beweise wichtig / interessant sind?

In welcher Beziehung stehen sie zu anderen algebraischen Beweissystemen? Sind sie für Lassere eine Art Doppelgänger?

Das unter dem Namen Positivstellensatz-Widerlegungen von Grigoriev und Vorobjov eingeführte grundlegende Quadratsummen-Beweissystem ist ein „statisches“ Beweissystem, um zu zeigen, dass ein Satz von Polynomgleichungen und Ungleichungen wobei f 1 , … , f k , h 1 , …

$$S=\{f_1=0,\dots,f_k=0,h_1\ge0,\dots,h_m\ge0\},$$ hat keine gemeinsame Lösung in R n : Eine Widerlegung von S wird durch die Polynome g i und e I , j gegeben, so dass - 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}$ (AnstellevonRkönnte man mit jedem wirklich geschlossenen Feld arbeiten.) Stengles Positivstellensatz garantiert, dassSgenau dann eine Widerlegung hat, wenn es keine Lösung gibt. Das Hauptmaßfür dieKomplexität ist hier derGradder Widerlegung, dh das Maximum der Gesamtgrade der Polynome, die unter den Summenzeichen in(∗) auftreten, d.H. Gifiunde2I,j∏i∈Ihich. $$\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$

Wie üblich bei den algebraischen Beweis Systemen kann man betrachten es auch als Widerlegung System für unerfüllbar Boolesche Formeln durch in einschließlich S die Axiome x 2 i - x i für jede Variable x i und Übersetzung von φ durch Polynom Ungleichheiten.$\phi$$S$$x_i^2-x_i$$x_i$$\phi$

Weitere Informationen zur Geschichte und Entwicklung von SOS-Systemen finden Sie unter http://arxiv.org/abs/1211.1958 .

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

Die Inferenzregeln sind:

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$

Es gibt gute Verbindungen mit semidefiniten Programmier- und Approximationsalgorithmen.

Weitere Informationen finden Sie in Albert Atserias 'jüngstem Vortrag beim BIRS-Workshop Theoretische Grundlagen des angewandten SAT-Lösens :

• Albert Atserias , Mini-Tutorial zu semi-algebraischen Beweissystemen ( Folien ), 2014