Logika dla informatyków/Ćwiczenia 10: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
mNie podano opisu zmian |
m Zastępowanie tekstu – „\displaystyle ” na „” |
||
| Linia 9: | Linia 9: | ||
{{Cwiczenie|3|| | {{Cwiczenie|3|| | ||
Rozszerzmy zbiór programów poprzez dodanie spójnika | Rozszerzmy zbiór programów poprzez dodanie spójnika | ||
programotwórczego <math> | programotwórczego <math>\cap</math>, interpretowanego w strukturach Kripkego jako | ||
przecięcie teoriomnogościowe relacji. | przecięcie teoriomnogościowe relacji. | ||
Niech PDL<math> | Niech PDL<math>_\cap</math> oznacza logikę | ||
zdaniową dla tak poszerzonych programów. Pokazać, że PDL<math> | zdaniową dla tak poszerzonych programów. Pokazać, że PDL<math>_\cap</math> nie ma | ||
własności małego modelu, tzn. że istnieje spełnialna formuła, która | 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. | nie jest spełniona w żadnej skończonej strukturze Kripkego. | ||
| Linia 18: | Linia 18: | ||
{{Cwiczenie|4|| | {{Cwiczenie|4|| | ||
Udowodnić, że spełnialność formuł logiki PDL<math> | Udowodnić, że spełnialność formuł logiki PDL<math>_\cap</math> jest | ||
nierozstrzygalna. | nierozstrzygalna. | ||
''Wskazówka:'' Zakodować problem "domina" (pokrycia płaszczyzny płytkami). | ''Wskazówka:'' Zakodować problem "domina" (pokrycia płaszczyzny płytkami). | ||
<!--zakodować problem istnienia pokrycia płytkami | <!--zakodować problem istnienia pokrycia płytkami | ||
płaszczyzny <math> | płaszczyzny <math>\omega\times\omega</math>, w którym to pokryciu pewien ustalony kolor | ||
występuje nieskończenie często.--> | występuje nieskończenie często.--> | ||
}} | }} | ||
Aktualna wersja na dzień 08:49, 28 sie 2023
Ć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).
