Seite parallel anzeigen





Schlussregeln

(Logik Einführung Kapitel 7.2.2)

Diese Seite nimmt Bezug auf

(Seite parallel anzeigen)
Liste überspringen
Zum Seitenanfang

Nun brauchen wir noch Regeln, die es uns erlauben, innerhalb unseres Systems Formeln mechanisch zu manipulieren um neue Formeln zu erhalten.

Die so genannten Transformations- oder Schlussregeln definieren (Ableitungs-)Regeln, wie bestehende Formeln zu neuen Formeln umgeformt werden dürfen.

Beispiel -

Betrachten wir wieder die Wumpus-Welt.

Haben wir z.B. die Formeln
  • WENN (NICHT Gestank(A,1))
    DANN (NICHT Wumpus(A,1)
    UND NICHT Wumpus(A,2)
    UND NICHT Wumpus(B,1))
  • NICHT GestankA1
wollen wir daraus automatisiert schließen können, dass
  • NICHT Wumpus(A,1) UND NICHT Wumpus(A,2) UND NICHT Wumpus(B,1)
Dies soll allgemein für jede Formel der Gestalt WENN..DANN gelten.

Da wir die Bedeutung der Aussagen verstehen, erscheint uns der Schluss klar. Ein Automat jedoch, der nur Symbole manipulieren kann benötigt hierfür jedoch eine Regel.

Also fügen wir unserem Kalkül folgende Schlussregel hinzu:
  • Haben wir eine Formel der Gestalt
    • WENN γ DANN δ
    wobei γ und δ beliebige Formeln sind
und ist
  • γ gegeben
können wir
  • δ ableiten

D.h.
  • "Haben wir eine WENN..DANN-Formel, und ist die Voraussetzung gegeben, so können wir den Schluss zu unserem Wissen hinzufügen"
Diese Regel ist in vielen Logiken enthalten und wird als "Modus Ponens" oder auch "Implikations-Elimination" bezeichnet.


Haben wir z.B. die Formel
  • NICHT Wumpus(A,2) UND NICHT Wumpus(B,1)
wollen wir auf jede einzelne Teilaussage schließen können, also z.B.
  • NICHT Wumpus(A,2)
Dies soll allgemein für alle UND-Verknüpften Formeln gelten.

Wieder erscheint es uns klar, dass, wenn die Gesamtaussage gilt, auch all ihre Teilaussagen gelten müssen - doch wieder müssen wir dies mit einer Schlussregel definieren:
  • Haben wir eine Formel der Gestalt
    • γ UND δ
    wobei γ und δ beliebige Formeln sind
können wir
  • γ ableiten
und
  • δ ableiten

D.h.
  • "Sind 2 Teilaussagen durch UND verbunden, so können wir jede dieser Teilaussagen zu unserem Wissen hinzufügen"
Auch diese Regel ist in vielen Logiken enthalten und wird als 'Und-Elimination' bezeichnet.


Haben wir z.B. die Formel
  • Wumpus(A,2) ODER Wumpus(B,1)
wissen aber bereits, dass eine dieser Teilaussage nicht gilt, also z.B.
  • NICHT Wumpus(A,2)
wollen wir auf die andere Teilaussage schließen können, also z.B.
  • Wumpus(B,1)
Dies soll allgemein für alle ODER-Verknüpften Formeln gelten.

Das Konzept erscheint uns klar, da wir die Bedeutung kennen: gilt eine Teilaussage nicht, muss die andere Teilaussage gelten - doch wieder müssen wir dies mit einer Schlussregel definieren:
  • Haben wir eine Formel der Gestalt
    • γ ODER δ
    wobei γ und δ beliebige Formeln sind
und
  • NICHT γ
können wir
  • δ ableiten

D.h.
  • "Sind 2 Teilaussagen durch ODER verbunden, und gilt eine dieser Teilaussagen nicht, so können wir die andere Teilaussage zu unserem Wissen hinzufügen"
Auch diese Regel ist in vielen Logiken enthalten und wird als 'Einfacher Widerspruch' bezeichnet.


So müssen wir nacheinander alle benötigten Regeln definieren, die es uns erlauben aus unserem Grundwissen und den zur Laufzeit generierten Informationen, weitere Schlüsse zu ziehen, und diese unserem Kalkül als Schlussregeln hinzufügen.
Den Transformationsregeln kommt natürlich keinerlei inhaltliche Bedeutung zu - sie sind ja rein formale Regeln, wie Zeichenketten umgeformt werden können.
Wir werden diese Regeln jedoch sinnvoller Weise so definieren, dass umgeformte Sätze auch semantisch aus den Ausgangssätzen folgen.