Logika dla informatyków/Ćwiczenia 10: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Nie podano opisu zmian |
Nie 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 istnienia pokrycia płytkami | ''Wskazówka:'' Zakodować problem ,,domina'' (pokrycia p³aszczyzny p³ytkami). | ||
<!--zakodować problem istnienia pokrycia płytkami | |||
płaszczyzny <math>\displaystyle \omega\times\omega</math>, w którym to pokryciu pewien ustalony kolor | płaszczyzny <math>\displaystyle \omega\times\omega</math>, w którym to pokryciu pewien ustalony kolor | ||
występuje nieskończenie często. | występuje nieskończenie często.--> | ||
}} | }} | ||
Wersja z 23:09, 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).
