SW wykład 11 - Slajd4

<<powrót do strony wykładu

Poprawność systemu dowodzenia Hoare'a Dowód Dowód, c.d. Problem z pełnością Uogólnienie TINY${}_A$ TINY${}_A$ Ekspresywność Relatywna pełność logiki Hoare'a Rozszerzenia Ograniczenia

Drugą pożądaną własnością systemów dowodzenia jest ich pełność: możliwość pokazania w tym systemie wszystkich stwierdzeń, które są semantycznie prawdziwe.

Taka pełność "w sensie absolutnym" dla naszego rachunku dowodzenia dla logiki Hoare'a nie może zachodzić. Co więcej, z analizy faktu, że własność stopu dla odpowiednio bogatej klasy instrukcji nie jest rozstrzygalna, a jej negacja jest wyrażalna jako stwierdzenie o częściowej poprawności instrukcji tej klasy względem odpowiednich warunków początkowych i końcowych, wywodzi się, że nie może istniej w pełni formalny, skończony system reguł dowodzenia, który byłby poprawny i pełny.

Jeśli jednak dodamy do naszego systemu dowodzenia "wyrocznię", która poda nam w razie potrzeby dowolną niezbędną formułę pierwszego rzędu prawdziwą w naszym modelu liczb całkowitych, tak jak omawialiśmy to powyżej, to otrzymany system okaże się pełny dla dowodzenia stwierdzeń o częściowej poprawności instrukcji naszego języka TINY względem warunków wstępnego i końcowego danych jako formuły pierwszego rzędu. Nie jest to jednak wynik łatwy, a jego pełniejsze zrozumienie wymaga oderwania się w pewnym sensie od obliczeń dotyczących tylko liczb całkowitych.