SW wykład 12 - Slajd24: Różnice pomiędzy wersjami
Nie podano opisu zmian |
mNie podano opisu zmian |
||
| (Nie pokazano 1 pośredniej wersji utworzonej przez tego samego użytkownika) | |||
| Linia 5: | Linia 5: | ||
Nie będziemy tu podawać pełnego systemu dowodzenia dla logiki | Nie będziemy tu podawać pełnego systemu dowodzenia dla logiki | ||
naszkicowanej na po przednim slajdzie --- nie jest to zadanie | naszkicowanej na po przednim slajdzie --- nie jest to zadanie | ||
trywialne. System taki zawiera oczywiście zwykłe reguły dla spójników | trywialne. System taki zawiera oczywiście zwykłe reguły logiki | ||
i kwantyfikatorów | pierwszego rzędu dla spójników i kwantyfikatorów. | ||
Do tego dodać należy szereg | |||
reguł (lub aksjomatów) wiążących modalności i spójniki zdaniowe --- | reguł (lub aksjomatów) wiążących modalności i spójniki zdaniowe --- | ||
jak pierwsze trzy aksjomaty podane na slajdzie. I w końcu, niezbędne | jak pierwsze trzy aksjomaty podane na slajdzie. I w końcu, niezbędne | ||
| Linia 14: | Linia 15: | ||
Najtrudniejsze, jak zwykle, są reguły dla modalności wyznaczonych | Najtrudniejsze, jak zwykle, są reguły dla modalności wyznaczonych | ||
przez instrukcje pętli: na ogół wymagają one nieskończonej liczby | przez instrukcje pętli: na ogół wymagają one nieskończonej liczby | ||
przesłanek | przesłanek i dopiero system z takimi nieskończonymi regułami może | ||
okazać się pełny. | okazać się pełny. | ||
Aktualna wersja na dzień 09:21, 17 paź 2006
Zadanie programistyczne Przykład Problemy z logiką Hoare'a Poprawność całkowita Poprawność całkowita, c.d. Poprawność całkowita, c.d. Reguła dla pętli Poprawność systemu dowodzenia dla Tiny Pełność systemu dowodzenia dla Tiny Przykład Uogólnienie Poprawność i pełność Relacje dobrze ufundowane Dowodzenie poprawności całkowitej Przykład Przykład Kolejny problem Binarne warunki końcowe Warunki poprawności Reguły dowodzenia Reguły dowodzenia, c.d. Przykład Logika algorytmiczna System dowodzenia
Nie będziemy tu podawać pełnego systemu dowodzenia dla logiki naszkicowanej na po przednim slajdzie --- nie jest to zadanie trywialne. System taki zawiera oczywiście zwykłe reguły logiki pierwszego rzędu dla spójników i kwantyfikatorów. Do tego dodać należy szereg reguł (lub aksjomatów) wiążących modalności i spójniki zdaniowe --- jak pierwsze trzy aksjomaty podane na slajdzie. I w końcu, niezbędne są reguły (lub aksjomaty) mówiące o semantyce instrukcji wyznaczających rozważane modalności --- jak ostatni z podanych aksjomatów, ujmujący niejako semantykę instrukcji złożonej. Najtrudniejsze, jak zwykle, są reguły dla modalności wyznaczonych przez instrukcje pętli: na ogół wymagają one nieskończonej liczby przesłanek i dopiero system z takimi nieskończonymi regułami może okazać się pełny.
