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