[MaLo] Schlussregeln beweißen

[FoSAP] Formale Systeme, Automaten, Prozesse
[BuK] Berechenbarkeit und Komplexität
[MaLo] Mathematische Logik

Schlussregeln beweißen

Beitragvon Matthew » 20.07.12 18:21

Hallo,

ist es möglich und ausreichend die Schlussregelbeweiße wie z.B. in der aktuellen Probeklausur allein durch Anwendung der 8 Schlussregeln der VL zu beweißen?
D.h. eine Sequenz wird so lange abgeleitet bis die Zielsequenz erreicht wird...oder eben nicht.

Grüße
Matthias
Matthew
 
Beiträge: 37
Registriert: 14.07.09 23:14

Re: Schlussregeln beweißen

Beitragvon Imrahil » 20.07.12 20:47

Wenn sie korrekt sind, kannst du sie auch mit den Schlussregeln beweisen. Allerdings war zumindest in den Übungen immer die Aufgabenstellung, sie semantisch zu beweisen.
Imrahil
 
Beiträge: 29
Registriert: 17.04.11 07:50
Studiengang: Informatik (B.Sc.)
Studiert seit: SS 11
Anwendungsfach: BWL

Re: Schlussregeln beweißen

Beitragvon Matthew » 21.07.12 15:23

Semantisch beweißen heißt dann die Korrektheit zeigen richtig? (auch invers korrekt)?

Was ich jetzt dazu gefunden habe ist:
Beweiss Korrektheit: Es wird angenommen, dass die Prämissen gültig sind. Nun muss gezeigt werden, dass die Konklussion gültig ist.
Beweiss inverse Korrektheit: Es wird angenommen, dass die Konklussion gültig ist. Nun muss gezeigt werden, dass die Prämissen gültig sind.

Beweiss Korrektheit:
Bei einer Wiederlegung muss man dann einfach ein Gegenbeispiel finden und die Formelmengen und Formeln passend belegen.

Bei einem Korrktheitsbeweiß muss man das Antezedenz (linke Seite von =>) mit einer Interpretation I belegen, sodass I |= Antezedenz.
Dann werden alle möglichen Fälle abgeleitet, sodass das Antezedenz immer noch Modell für jede Formel bleibt und zeigt mit Hilfe der Prämissen, dass dies weiter eine gültige Sequenz ist.
Stimmt das soweit?

Beweiss invers Korrektheit
Man setzt I |= Antezedenz und die Formel des Sukzedenz auf falsch und schreibt am Ende hin "und es folgt aus der Gültigkeit der Konklussion I |= v wobei v die Formelmenge auf Seiten des Sukzedenz ist"


Kann das jemand so als Herangehensweise bestätigen?
Matthew
 
Beiträge: 37
Registriert: 14.07.09 23:14


Zurück zu Theoretische Informatik