Intuicja za systemami dowodowymi

Próbuję zrozumieć artykuł na temat p-Optimal Proof Systems and Logic for PTIME . W artykule jest pojęcie nazywane systemami dowodowymi i nie rozumiem intencji:

$\Sigma = \{0,1\}$ ... Identyfikujemy problemy z podzbiorami w .$Q$$\Sigma^*$

Myślę, że intencją jest to, że kodujemy pewną strukturę w (np. Grafy bezkierunkowe), a podzbiory tych struktur są problemami (np. Wykresy płaskie).$\Sigma^*$

System dowodu na problem to funkcja zaskakująca obliczalna w czasie wielomianowym.$Q \subset \Sigma^*$$P:\Sigma^* \to Q$

Teraz można powiedzieć, że jest zbiorem wszystkich możliwych modeli w określonej strukturze (np. Wszystkich nieukierowanych grafów). Ale to nie ma sensu, ponieważ dlaczego przekierowane wykresy powinny być mapowane na podzbiorze? Może to być kodowane maszyny Turinga, ale to też nie ma sensu ...$\Sigma^*$

Jakieś pomysły?

Myśleć o $\Sigma^{*}$ kodowanie jakiegoś rodzaju obiektów oraz $Q$jako zbiór wszystkich obiektów spełniających określone właściwości. Myśleć o$P$ jako funkcja, która akceptuje (kodowanie) pary $(x, p)$ gdzie $x$ jest przedmiotem i $p$ jest rzekomym „dowodem” $x \in Q$. Funkcja$P$ to „sprawdzanie dowodu”: to weryfikuje $p$ faktycznie stanowi ważny dowód, że $x \in Q$. Jeśli tak, zwraca$x$, w przeciwnym razie zwraca domyślny element $Q$.

Załóżmy na przykład $\Sigma^{*}$ koduje wykresy i niech $Q$być zbiorem (kodowania) grafów hamiltonowskich. Możliwe$P$ jest to: dekodować wejście jako $(G, \ell)$ gdzie $G$ jest wykresem i $\ell$ to lista wierzchołków $G$; zweryfikuj to$\ell$ to cykl hamiltonowski w $G$; jeśli tak, to wróć$G$ w przeciwnym razie zwróć wykres w jednym punkcie.

Rozważono przypadek płaskich wykresów. Aby uzyskać odpowiedni$P$ potrzebujemy pojęcia sprawdzanego w wielu przypadkach dowodu planarności.

Ogólnie dane wejściowe do $P$ nie trzeba kodować pary $(x, p)$. Ważne jest to, że$P$ może wydobyć z informacji dwa fragmenty informacji: przedmiotowy przedmiot i domniemany dowód, że obiekt należy do $Q$. Weźmy na przykład jako$Q$zbiór wszystkich zdań możliwych do udowodnienia w jakiejś teorii pierwszego rzędu. Teraz$P$dekoduje swój wkład jako formalny dowód. Jeśli kodowanie jest nieprawidłowe, zwraca$\top$. Jeśli kodowanie reprezentuje prawidłowy dowód, zwraca oświadczenie, które zostało udowodnione przez dowód (prawdopodobnie jest to katalog główny drzewa dowodu lub ostatnia formuła w sekwencji instrukcji, w zależności od tego, jak sformalizujesz dowody).

Powinieneś pomyśleć o wejściu systemu dowodowego $P$ jako tekst dowodu $\pi$ elementu $q \in Q$. Jeśli tekst jest poprawny, to$P(\pi) = q$, Inaczej $P(\pi)$ jest naprawione $q_0 \in Q$. Chcemy$P$ być polytime, ponieważ oznacza to, że dowód jest łatwy do zweryfikowania.

Załóżmy na przykład $Q$ jest zbiorem tautologii zdań, i $P$jest dowolnym systemem sprawdzającym w stylu Hilberta, który składa się z zestawu linii , z których każda jest albo aksjomatem, albo wynika z poprzednich linii za pomocą reguły pochodnej (zwykle Modus Ponens). Jeśli dowód jest ważny, to$P$powinien wypisać ostatni wiersz w dowodzie. W przeciwnym razie wypisz jakieś stałe tautologie, takie jak$p \lor \lnot p$.

Wróć do pierwszego pytania $Q$jest kodowaniem wszystkich struktur określonego typu spełniających określone właściwości. Jednym z przykładów są tautologie. Innym przykładem jest zestaw wszystkich niekolorowych grafów, które mają system sprawdzania znany jako rachunek Hajósa.