Egzamin 2011/2012

Zadanie 1 (15 punktów)

Napisać formułę \(\varphi(x,y)\) w języku arytmetyki taką, że \((\mathfrak{N},x:r,y:k)\models \varphi\) wtw w ćwierćkole \(\{(x,y)\in \mathbb{R}^2~:~x,y\geq 0,~x^2+y^2\leq r\}\) na płaszczyźnie euklidesowej jest dokładnie \(k\) punktów kratowych (tzn. punktów o obu współrzędnych całkowitych).

Rozwiązanie

Wykorzystamy formułę \(\chi\), definiującą funkcję \(\beta\) Goedla, aby powiedzieć, że istnieje ciąg \(y\) parami różnych par liczb naturalnych \((u,v)\) spełniających \(u^2+v^2\leq x\) i że każda para liczb spełniająca ten warunek w tym ciągu występuje.

\(\exists t\exists p
[\forall i(i\le y-1\to(\exists u\exists v\chi(t,p,2*i,u)\land\chi(t,p,2*1+1,v)\land u*u+v*v\leq x)\land\)
\((\forall u\forall u(u*u+v*v\leq x\to\exists! i(i\le y-1\land \chi(t,p,2*i,u)\land\chi(t,p,2*1+1,v))]\).

Zadanie 2 (15 punktów)

W pewnej bazie danych znajduje się dwukolumnowa tabela \(R\), zawierająca w sobie relację liniowego porządku na wszystkich elementach dziedziny aktywnej tej bazy danych. Dane jest także wyrażenie \(E\) algebry relacji

\(R\setminus (\pi_{1,4}(\sigma_{2=3}(R\times R)\setminus(\sigma_{1=2}(R\times R)\cup\sigma_{3=4}(R\times R)))).\)

Zaprojektować algorytm obliczający \([\![E]\!]\), którego złożoność czasowa wynosi \(O(n)\), gdzie \(n=|R|.\) Można korzystać z tablicy haszującej dla elementów dziedziny aktywnej, o dostępie w czasie jednostkowym i zapewniającej brak kolizji.

Rozwiązanie

Wyrażenie \(E\) opisuje sumę relacji bezpośredniego następnika na dziedzinie aktywnej i relacji identycznościowej na dziedzinie aktywnej, zgodnie z porządkiem zadanym przez \(R\). Obliczenie relacji identycznościowej jest banalne, problemem jest tylko następnik.

Jeśli \(|R|=n\), to rozmiar dziedziny aktywnej wynosi \(m=O(\sqrt{n})\).

W celu obliczenia następnika można użyć tablicy haszującej \(T\), używając ją do zliczania ile razy każdy z elementów dziedziny aktywnej występuje po lewej stronie par w relacji \(R\). Wymaga to liniowego przejścia \(R\) w czasie \(O(n)\). Po zakończeniu tego procesu można \(T\) posortować po wartościach zliczeń w czasie \(O(m\log m)=O(n)\) i wypisać pary kolejnych elementów, albo wykorzystać \(T\) do rozstrzygania w czasie stałym o porządku par poszczególnych elementów (przez porównanie ich zliczeń w \(T\)), co pozwala po prostu posortować dziedzinę aktywną.

Zadanie 3 (15 punktów)

Rozważamy logikę LTL nad skończonymi strukturami-słowami.
Jak wiadomo z tw. Gabbaya, każde zdanie \(\varphi\) logiki LTL można wyrazić równoważnie w postaci zdania będącego boolowską kombinacją zdań czasu przyszłego i zdań czasu przeszłego.

Podać przykład zdania \(\varphi\) logiki LTL którego nie można wyrazić równoważnie w postaci koniunkcji jednego zdania czasu przyszłego i jednego zdania czasu przeszłego.

Rozwiązanie

Roważmy zdanie \(\varphi=Yp\lor Xp\).

Przypuśćmy, że \(\varphi\) jest równoważne formule \(\alpha\land\beta\), gdzie \(\alpha\) jest czasu przeszłego a \(\beta\) jest czasu przyszłego. Rozważmy teraz dwa modele o trzech stanach, zapisane jako ciągi prawdziwości \(p\) w kolejnych stanach. Te modele to \(100\) i \(001\). W obu stan środkowy oznaczmy \(*\).

Mamy zatem \((100,*)\models\varphi\) i \((001,*)\models\varphi\).

Ponieważ \(varphi\) jest równoważne \(\alpha\land\beta\), to \((100,*)\models\beta\) i \((001,*)\models\alpha\).

Zatem \((000,*)\models\beta\) bo \(\beta\) jest czasu przyszłego a \(000\) różni się od \(100\) tylko w przeszłości względem \(*\)
oraz \((000,*)\models\alpha\) bo \(\alpha\) jest czasu przeszłego a \(000\) różni się od \(001\) tylko w przyszłości względem \(*\).

Stąd \((000,*)\models\alpha\land\beta\) wbrew założeniu, że ta formuła jest równoważna \(Yp\lor Xp\).

Zadanie 4 (15 punktów: 5 za podpunkt 1 i 10 za podpunkt 2)

Zajmujemy się skończonymi grafami nieskierowanymi. W obu podpunktach należy napisać zdanie \(\varphi\) logiki drugiego rzędu takie, że dla każdego grafu \(\mathfrak{G}\) zachodzi

\(\mathfrak{G}\models\varphi\) wtw \(\mathfrak{G}\) jest spójny}.

\(\varphi\) ma mieć postać \(\forall R\varphi',\) gdzie \(\varphi'\) jest formułą pierwszego rzędu.
\(\varphi\) ma mieć postać \(\exists R\varphi',\) gdzie \(\varphi'\) jest formułą pierwszego rzędu.

Rozwiązanie

Niech \(E\) to relacja krawędzi.

Wyrażamy Dla każdego podziału \(\mathfrak{G}\) na dwa niepuste podzbiory, istnieje krawędź łacząca wierzchołek w jednej z tych części z wierzchołkiem w drugiej części.
\(\forall R((\exists x\exists y R(x)\land\lnot R(y)) \to(\exists x\exists y R(x)\land\lnot R(y)\land E(x,y)))\)
Najpierw napiszemy zdanie postaci \(\forall x\forall y \exists R\varphi\) wyrażające spójność. Będzie ono formalizowało
\(\forall x\forall y \) istnieje ścieżka od \(x\) do \(y\).
Ma ono postać

\(\forall x\forall y \exists R(x=y\lor \) "\(R\) jest liniowym porządkiem, \(x\) jest pierwszy w tym porządku, między każdymi dwoma kolejnymi wierchołkami \(z,t\) położonymi pomiędzy \(x\) i \(y\) jest krawędź").

\(\forall x\forall y \exists R\varphi(x=y\lor\)
\( ((\forall u R(u,u))\land(\forall u\forall v R(u,v)\lor R(v,u))\land(\forall u\forall v (R(u,v)\land R(v,u))\to u=v)\land(\forall u \forall v\forall w (R(u,v)\land R(v,w))\to R(u,w)))\land\)
\((\forall z R(x,z))\land \)
\( \forall z\forall t [[R(z,y)\land R(t,y)\land(\forall u ((R(z,u)\land R(u,t)))\to(u=z\lor u=t))]\to E(z,t)]\)

Teraz mając zdanie \(\forall x\forall y \exists R\varphi\) przerabiamy je na żądaną postać przez zamianę \(R\) z dwuargumentowego na czteroargumentowy:

\(\exists R\forall x\forall y \varphi[R(x,y,*,*)/R(*,*)]\), co ma ten efekt, że nowa relacja \(R\) dla każdego wyboru \(x,y\) ma w sobie zapisany odpowiedni porządek, opisujący ścieżkę od \(x\) do \(y\).

TEST

1. Niech dla zdania \(\varphi\) logiki pierwszego rzędu

\({spec}(\varphi)=\{n\in\mathbb{N}_+\) istnieje \(\mathfrak{A}\) o mocy \(n\) takie, że \(\mathfrak{A}\models\varphi\}.\)

Czy następujący problem jest rozstrzygalny:
Dane: Dwa zdania \(\varphi,\psi\) logiki pierwszego rzędu.
Pytanie: Czy \(spec(\varphi)=spec(\psi)\)?

Odpowiedź

NIE, bo gdyby był, to można by sprawdzać czy dane zdanie \(\varphi\) ma skończony model pytając czy \(spec(\varphi)=spec(\bot)\). Tymczasem jest to niemożliwe na mocy tw. Trachtenbrota.

2. Czy następująca formuła logiki drugiego rzędu SO jest jest tautologią?

\([\forall R \exists Q_1 \exists Q_2 \forall x \forall y (R(x,y) \leftrightarrow
(Q_1(x) \land Q_2(y)))]\)

\(\to\)

\([\exists Q_1 \exists Q_2 \forall R \forall x \forall y ((R(x,y) \leftrightarrow
Q_1(x,y)) \lor (R(x,y) \leftrightarrow Q_2(x,y)))]\)

Odpowiedź

TAK.

Zdanie w pierwszej linijce orzeka, że każda relacja dwuargumentowa (czyli zbiór par elementów) jest produktem kartezjańskim dwóch zbiorów elementów. Jest to możliwe wtedy i tylko wtedy gdy uniwersum modelu ma dokładnie jeden element.

W takim model z kolei istnieją dwie relacje dwuragumentowe (a konkretnie pusta i pełna) takie, że każda relacja relacja dwuargumentowa jest jedną z nich (bo innych na uniwersum jednoelementowym nie ma).

3. Czy gracz II ma strategię wygrywającą w grze Ehrenfeuchta-Fra\"{\i}ss\'ego o 4 rundach \(G_4(\mathfrak{A},\mathfrak{B}),\) gdzie \(\mathfrak{A}\) i \(\mathfrak{B}\) są poniższymi grafami nieskierowanymi (\(\mathfrak{A}\) po lewej, \(\mathfrak{B}\) po prawej):

   *      *      *      *                        *      *      *    
   |      |      |      |                        |      |      |    
 *-*-*  *-*-*  *-*-*  *-*-*                    *-*-*  *-*-*  *-*-*  
   |      |      |      |                        |      |      |    
   *      *      *      *                        *      *      *

Odpowiedź

NIE. Oto strategia dla gracza I: w trzech ruchach kolejno zaznacza centra krzyży po prawej stronie, po czym w czwartym zaznacza dowolny element tego krzyża po lewej, w którym gracz II nie zaznaczył dotąd żadnego elementu.

4. Ustalamy alfabet \(A_k\) i rozpatrujemy modele-słowa postaci \(\mathfrak{A}(w)\) dla słów \(w\in A_k^+.\) Niech dla zdania \(\varphi\) logiki monadycznej drugiego rzędu MSO
\(\bar{spec}(\varphi)=\{n\in\mathbb{N}_+ :\) istnieje \(w\in A_k^n\) takie, że \(\mathfrak{A}(w)\models\varphi\}.\)

Czy dla każdego zdania \(\varphi\) w MSO istnieje zdanie \(\psi\) w MSO takie, że \(\mathbb{N}_+\setminus\bar{spec}(\varphi)=\bar{spec}(\psi)\)?

Odpowiedź

TAK. Wystarczy wziąć zdanie \(\lnot \exists X_1\ldots\exists X_k\varphi\), gdzie \(X_1\ldots X_k\) to wszystkie relacje unarne w sygnaturze \(\varphi\).

5. Czy w logice LTL da się wyrazić formułą następującą własność modelu-słowa \(\mathfrak{A}(w)\):
jest dokładnie tyle samo stanów w których zmienna zdaniowa \(p\) jest prawdziwa i stanów w których zmienna zdaniowa \(p\) jest fałszywa.

Odpowiedź

NIE. Opisana własnośc nie jest regularna, więc nie da się jej wyrazić nawet w logice MSO (tw. Buchi-Elgota), a tym bardziej w FO, która jest równoważna LTL (tw. Kampa).