Logika dla informatyków/Ćwiczenia 10

Ćwiczenie 1

Uzupełnić brakujące dowody w tej części.

Ćwiczenie 2

Pokazać, że dla PDL nie zachodzi twierdzenie o dedukcji.

Ćwiczenie 3

Rozszerzmy zbiór programów poprzez dodanie spójnika programotwórczego $\cap$, interpretowanego w strukturach Kripkego jako przecięcie teoriomnogościowe relacji. Niech PDL${}_{\cap }$ oznacza logikę zdaniową dla tak poszerzonych programów. Pokazać, że PDL${}_{\cap }$ nie ma własności małego modelu, tzn. że istnieje spełnialna formuła, która nie jest spełniona w żadnej skończonej strukturze Kripkego.

Ćwiczenie 4

Udowodnić, że spełnialność formuł logiki PDL${}_{\cap }$ jest nierozstrzygalna. Wskazówka: zakodować problem istnienia pokrycia płytkami płaszczyzny $\omega \times \omega$, w którym to pokryciu pewien ustalony kolor występuje nieskończenie często.