Seite parallel anzeigen
Der logische Beweis
(Logik Einführung Kapitel 7.2)Diese Seite nimmt Bezug auf
(Seite parallel anzeigen)
- Logik Einführung: Syntax
- Logik Einführung: Semantik
- Logik Einführung: Der logische Schluss
Die logische Inferenz (oder auch Ableitung) ist das syntaktische Pendant der logischen Konsequenz.
Innerhalb einer Ableitung werden Formeln
In diesem Kapitel wollen wir definieren, was ein logische Schluss ist. Auf die Definition der Schlussregeln und Axiome wird in den nächsten Kapiteln näher eingegangen.
D.h.:
Innerhalb einer Ableitung werden Formeln
- mechanisch
- nach festgelegten Regeln (die so genannten "Schlussregeln")
- unter eventueller Miteinbeziehung vorgegebener Formeln (die so genannten "Axiome")
In diesem Kapitel wollen wir definieren, was ein logische Schluss ist. Auf die Definition der Schlussregeln und Axiome wird in den nächsten Kapiteln näher eingegangen.
Beispiel - Die Nadel im Heuhaufen: logischer Beweis
Suchen wir die Nadel im Heuhaufen, besteht der logische Beweis darin, dass wir nach irgendeiner Methode so lange Halme abtragen, bis wir die Nadel finden.
Wir sagen eine Formel γ lässt sich aus einer Menge von Formeln Γ ableiten, wenn γ das Ergebnis einer endlichen Abfolge von Anwendungen von Umformungsregeln unter eventueller Miteinbeziehung bestimmter anderer Formeln (die Grundvoraussetzungen ausdrücken) auf Γ ist.
Γ bezeichnen wir als Annahmen oder Prämissen,
γ als Konklusion,
die Umformungsregeln als Schlussregeln,
und die Grundvoraussetzungen als Axiome.
Die Abfolge der Regeln bezeichnen wir als Beweis (oder auch Ableitung).
Führen wir den Ableitungsoperator |-- ein,
schreiben wir Γ|--γ
wenn γ aus Γ ableitbar ist.
Γ bezeichnen wir als Annahmen oder Prämissen,
γ als Konklusion,
die Umformungsregeln als Schlussregeln,
und die Grundvoraussetzungen als Axiome.
Die Abfolge der Regeln bezeichnen wir als Beweis (oder auch Ableitung).
Führen wir den Ableitungsoperator |-- ein,
schreiben wir Γ|--γ
wenn γ aus Γ ableitbar ist.
D.h.:
- Haben wir eine Formelmenge Γ
- wenden wir die Umformungsregeln auf diesen endlich oft an, wobei wir bei jedem Schritt Grundvoraussetzungen hinzunehmen können
- und kommen so zum Ergebnis γ
- sagen wir γ lässt sich aus Γ ableiten
- und schreiben Γ|--γ
Beispiel - Logischer Beweis: Wumpus-Welt
Lösen wir das das Beispiel aus dem Kapitel "Der logische Schluss" syntaktisch.
Angenommen, wir wissen, dass
Prämisse NICHT Gestank(A,1) Axiom WENN (NICHT Gestank(A,1))
DANN (NICHT Wumpus(A,1)
UND NICHT Wumpus(A,2)
UND NICHT Wumpus(B,1))
Nehmen wir weiters an, wir haben eine Schlussregel 1, die besagt, dassund ist
- haben wir eine Formel der Gestalt
wobei γ und δ beliebige Formeln sind
- WENN γ DANN δ
können wir
- γ gegeben
- δ ableiten
Dann können wir in Schritt 1 unserer Inferenz aus der Prämisse unter Miteinbeziehung des Axiomesableiten.
Wissen 1 NICHT Wumpus(A,1) UND NICHT Wumpus(A,2) UND NICHT Wumpus(B,1)
Angenommen, wir haben eine weitere Regel, Schlussregel 2, die besagt, dasskönnen wir
- haben wir eine Formel der Gestalt
- γ UND δ
und
- γ ableiten
- δ ableiten
Dann können wir in Schritt 2 unserer Inferenz aus dem Wissen 1ableiten.
Wissen 2 NICHT Wumpus(A,1) Wissen 3 NICHT Wumpus(A,2) Wissen 4 NICHT Wumpus(B,1)
D.h.
- NICHT Gestank(A,1) |-- NICHT Wumpus(A,2)
So können wir aus der Wahrnehmung und den Grundvoraussetzungen (Spielregeln) automatisiert (ohne jegliches Wissen darüber, was Wumpus oder Gestank bedeuten) darauf schließen, dass sich der Wumpus nicht auf Feld [A,2] befinden kann.
Die Schritte 1 und 2 bezeichnen wir als Beweis, und sagen 'NICHT Wumpus(A,2)' lässt sich aus 'NICHT Gestank(A,1)' ableiten.
Haben wir die Spielregeln nicht als Axiome innerhalb unserer Logik definiert, müssen wir das Axiom als weitere Prämisse hinzufügen, und erhalten
- {
NICHT Gestank(A,1),
WENN (NICHT Gestank(A,1)) DANN (NICHT Wumpus(A,1) UND NICHT Wumpus(A,2) UND NICHT Wumpus(B,1))
} |-- NICHT Wumpus(A,2)
- zurück zu Der logische Schluss
- zum Seitenanfang
- weiter zu
