Seite parallel anzeigen
Semantisches Prüfverfahren für die Gültigkeit eines Schlusses
(Aussagenlogik Kapitel 7.1.4)Diese Seite nimmt Bezug auf
(Seite parallel anzeigen)
- Aussagenlogik: Evaluierung einer Formel unter einer Interpretation
- Aussagenlogik: Der aussagenlogische Schluss
- Aussagenlogik: Die Monotonieeigenschaft
- Logik Einführung: Gültigkeit
- Logik Einführung: Erfüllbarkeit
- Logik Einführung: Zusammenhänge
- Aussagenlogik: Interpretationsfunktion
Wir können die Evaluierung einer Formel unter einer Interpretation dazu nutzen, die Frage nach der Gültigkeit eines Schlusses zu beantworten:
Diese direkte, semantische Methode ist ein reines Entscheidungsverfahren. Jede gültige Formel wird als gültig erkannt - jede widerlegbare als widerlegbar.
Zu bemerken ist, dass mit jedem Verfahren, das die Gültigkeit einer Formel bestimmt, auch die Erfüllbarkeit einer Formel γ geprüft werden kann, indem !γ geprüft wird: γ ist erfüllbar gdw. !γ nicht gültig ist.
Leider ist dieses Verfahren nicht sehr effizient: Hat eine Formel m Variablen, müssen im schlimmsten Fall 2m Interpretationen geprüft werden! In weiterer Folge wollen wir uns damit auseinander setzen, wie wir die Frage nach der Gültigkeit eines Schlusses mittels logischer Inferenzmethoden beantworten können.
- Wie wir gesehen haben können wir (auf Grund des Deduktionstheorems) die Frage nach der Gültigkeit eines Schlusses Γ|=γ auf die nach der Gültigkeit einer Formel δ reduzieren.
-
Da eine Formel genau dann gültig ist, wenn sie alle Interpretationen erfüllen, können wir sie unter allen möglichen Interpretationen evaluieren:
- evaluiert sie unter einer Interpretation zu falsch, so ist die Formel (und somit auch der Schluss) nicht gültig;
- evaluiert sie unter allen Interpretationen zu wahr, so ist die Formel (und somit auch der Schluss) gültig.
Diese direkte, semantische Methode ist ein reines Entscheidungsverfahren. Jede gültige Formel wird als gültig erkannt - jede widerlegbare als widerlegbar.
Zu bemerken ist, dass mit jedem Verfahren, das die Gültigkeit einer Formel bestimmt, auch die Erfüllbarkeit einer Formel γ geprüft werden kann, indem !γ geprüft wird: γ ist erfüllbar gdw. !γ nicht gültig ist.
Leider ist dieses Verfahren nicht sehr effizient: Hat eine Formel m Variablen, müssen im schlimmsten Fall 2m Interpretationen geprüft werden! In weiterer Folge wollen wir uns damit auseinander setzen, wie wir die Frage nach der Gültigkeit eines Schlusses mittels logischer Inferenzmethoden beantworten können.
- zurück zu Das Widerlegungstheorem - der indirekte Beweis
- zum Seitenanfang
- weiter zu
