Hoare: Vollständigkeit < Formale Sprachen < Theoretische Inform. < Hochschule < Informatik < Vorhilfe
|
| Status: |
(Frage) überfällig  | | Datum: | 20:15 Mo 15.10.2007 | | Autor: | Aeolus |
| Aufgabe | aus einem Skript:
Der Hoare-Kalkül ist relativ vollständig. Das heisst:
Eine Aussage {A} b {C} ist gültig genau dann, wenn sie herleitbar ist. Zusätzlich gilt aber, dass man Aussagen dieser Art nicht formal auf Gültigkeit prüfen kann. |
Wieso kann man das nicht formal prüfen? Wenn etwas gültig ist, kann man es doch auch herleiten, und eine Herleitung aus den Regeln ist doch eine formale Überprüfung?
Ich habe zwei mögliche Erklärungen, die aber mehr oder weniger geraten sind:
1. Aus der Herleitbarkeit folgt nicht zwangsläufig, dass man es tatsächlich mit einem Beweissystem herleiten kann (Gödelscher Unvollständigkeitssatz).
2. Man kann nur gültige Aussagen durch Herleitung prüfen, es ist also semi-entscheidbar, ob eine Aussage gültig ist. Wenn sie nicht gültig ist, lässt sich nicht ermitteln, ob sie tatsächlich nicht herleitbar ist.
Leider finde ich dazu kaum Material im Web, deshalb hoffe ich, dass mir hier jemand weiterhelfen kann!
Danke!
Aeolus
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig  | | Datum: | 20:20 Fr 19.10.2007 | | Autor: | matux |
$MATUXTEXT(ueberfaellige_frage)
|
|
|
|
