Wykres teoretyczne ograniczenie do dowodów w teorii złożoności dowodu

Złożoność dowodu jest najbardziej podstawowym obszarem teorii złożoności obliczeniowej. Ostatecznym celem tego obszaru jest udowodnienie , co oznacza, że ​​żaden z proverów nie może dać dowodu na niezadowolenie danej formuły wejściowej. $NP\neq coNP$

Wykres jest jednym z formalnych modeli dowodów. Moje pytanie dotyczy dalszego ograniczenia tego modelu.

Dowód jest reprezentowany jako DAG. Węzły z wachlarzem 0 mają etykiety aksjomatyczne. Unikalny węzeł z rozwinięciem 0 odpowiada „fałszowi”. Dla danych wejściowych reguł dedukcji każdy węzeł, który ma zarówno stopień, jak i stopień, ma etykietę reprezentującą propozycję.

Moje pytanie brzmi:

Czy istnieją systemy dowodowe i powiązane badania w przypadku, gdy klasa DAG-ów jest ograniczona? Artykuły, ankiety i notatki z wykładów są mile widziane.

Czy systemy dowód, które były wcześniej badane, takie jak Nullstellensatz, Resolution, LS, AC0 Frege, RES (k), Caluculus wielomianowy i płaszczyzny cięcia, mają jakąś teoretyczną charakterystykę graficzną?

Najbardziej naturalnym ograniczeniem dowodu DAG jest to, że jest to drzewo - to znaczy, że żaden „lemat” (wniosek pośredni) nie jest używany więcej niż jeden raz. Ta właściwość nazywa się „drzewiasta”. Ogólna rozdzielczość jest wykładniczo silniejsza niż rozdzielczość drzewiasta, jak pokazują na przykład Ben-Sasson, Impagliazzo i Wigderson . Pomysł ten został również rozważony w przypadku innych systemów dowodowych - po prostu wyszukaj „drzewopodobny X”, gdzie X jest interesującym systemem dowodowym. W szczególnym przypadku rozwiązania można wziąć pod uwagę inne ograniczenia. Zobacz na przykład artykuł Alekhnovicha, Johannsena, Pitassi i Urquharta dotyczący regularnego rozwiązywania problemów.

Rozdzielczość podobna do drzewa jest szczególnie ważna, ponieważ tradycyjne implementacje DPLL odpowiadają odrzuceniom podobnym do drzewa. Technika uczenia się klauzul, która jest ważna w praktyce, odpowiada dopuszczeniu ogólnych DAG. Dlatego też struktura dowodu DAG jest silnie zależna od algorytmu go generującego.

Badania Müllera i Szeidera Dowody rozdzielczości, w których dowód DAG ograniczył szerokość drzewa lub ograniczoną szerokość ścieżki (dla odpowiednich rozszerzeń miar złożoności wykresu na wykresach ukierunkowanych).

Pokazują, że szerokość ścieżki DAG jest zasadniczo taka sama jak złożoność przestrzeni dowodu i definiują ogólne pojęcie przestrzeni dowodu, która jest równoważna szerokości drzewa.

W przypadku wystarczająco silnych systemów dowodowych przedstawienie graficzne dowodu w systemie wydaje się mniej istotne, ponieważ (jak już skomentował Joshua Grochow), dowody podobne do DAG i drzewiastych Fregów są wielomianowo równoważne ( dowód na ten fakt znajduje się w monografii Krajicka z 1995 r. ).

W przypadku słabszych systemów dowodowych, takich jak rozdzielczość, drzewiaste jest wykładniczo słabsze niż dowody podobne do DAG (jak opisano powyżej Yuval Filmus).

Beckmann i Buss [1] (zgodnie z Beckmannem [2] ) rozważali ograniczenie wysokości (równoważnie głębokości) wykresu próbnego dowodów głębokości Frege'a o stałej głębokości i zbadali związek między DAG, wielkością drzewa i wysokością stałej głębokości Dowody Frege. (Zwróć uwagę na rozróżnienie między ograniczaniem głębokości wykresu próbnego a ograniczaniem głębokości obwodu pojawiającego się w linii próbnej).

Mogą istnieć również rozróżnienia między dowodami Nullstellensatz (i rachunkiem wielomianowym) podobnym do drzewa i DAG, których obecnie nie pamiętam.