Logika dla informatyków/Ćwiczenia 10: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Nie podano opisu zmian |
mNie podano opisu zmian |
||
| Linia 20: | Linia 20: | ||
Udowodnić, że spełnialność formuł logiki PDL<math>\displaystyle _\cap</math> jest | Udowodnić, że spełnialność formuł logiki PDL<math>\displaystyle _\cap</math> jest | ||
nierozstrzygalna. | nierozstrzygalna. | ||
''Wskazówka:'' Zakodować problem | ''Wskazówka:'' Zakodować problem "domina" (pokrycia płaszczyzny płytkami). | ||
<!--zakodować problem istnienia pokrycia płytkami | <!--zakodować problem istnienia pokrycia płytkami | ||
Wersja z 23:10, 30 paź 2006
Ć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 , interpretowanego w strukturach Kripkego jako przecięcie teoriomnogościowe relacji. Niech PDL oznacza logikę zdaniową dla tak poszerzonych programów. Pokazać, że PDL 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 jest nierozstrzygalna. Wskazówka: Zakodować problem "domina" (pokrycia płaszczyzny płytkami).
