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).

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.

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.

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}.

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

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)\)?

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)))]\)

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):

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

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)\)?

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.