Arbeitsweise	Grundlagen Unifikation Backtracking Resolution Pfad: Startseite / Fächer / Informatik / Prolog / Arbeitsweise / Grundlagen
Autor: mk 22.05.2008 17:40:36 796	Grundlagen

Grundlegende Definitionen

Es sei Φ = {A, A→B, B→C} eine Menge von aussagenlogischen Formeln. Die Formel A ist eine elementare oder atomare Aussage, die Formel A→B eine zusammengesetzte Aussage.

Eine Interpretation ordnet jeder atomaren Aussage (aussagenlogischer Variable) einen Wahrheitswert zu, z.B. für Φ : A = 1, B = 0 , C = 0. Eine Interpretation, die alle Formeln einer Menge Φ wahr macht, heißt Modell von Φ.

Eine Formel φ ist eine semantische Folgerung aus Φ, wenn jede Interpretation, die Φ wahr macht, auch φ wahr macht. Man schreibt dann Φ ⊧ φ und sagt auch φ folgt aus Φ .

Achtung: Diese Seite enthält logische Symbole aus dem Unicode-Zeichensatz, die der Internet-Explorer nicht darstellen kann. Er zeigt dann nur ein Quadrat.

Wahrheitstabellen

Folgt φ = A→C aus obigem Φ?

Das Programm zur Ermittlung von Wahrheitstabellen von Christian Gottschall liefert:

  A B C  |  ((A & (A -> B)) & (B -> C)) -> (A -> C)
  -------+-----------------------------------------
  1 1 1  |      1     1     1     1     *1     1      Achtung: Rote Junktoren werden metasprachlich benutzt.
  1 1 0  |      1     1     0     0     *1     0      Sollte man die Sprachebenen nicht besser trennen?
  1 0 1  |      0     0     0     1     *1     1
  1 0 0  |      0     0     0     1     *1     0
  0 1 1  |      0     1     0     1     *1     1
  0 1 0  |      0     1     0     0     *1     1
  0 0 1  |      0     1     0     1     *1     1
  0 0 0  |      0     1     0     1     *1     1

Wahrheitstabellen sind eine sichere Methode, logische Aussagen zu überprüfen. Warum gibt man sich nicht damit zufrieden? Die Antwort liegt in dem exponentiellen Aufwand. n Eingangsvariablen erfordern 2ⁿ Zeilen. So ergeben nur 20 Variablen bereits 2²⁰ = 1 048 576 Zeilen. Obiges Beispiel zeigt, dass unter Umständen auch sehr viele Spalten zu berechnen sind.

Aufgabe

Folgt φ = A→C auch aus Φ = {A→B, B→C}?

Inferenzregeln

Schlussregeln wie der modus ponens oder der modus tollens erlauben es, ganz 'mechanisch', z.B. φ = C aus obigem Φ semantisch zu folgern.

Definition

φ ist aus Φ ableitbar, in Zeichen Φ ⊦ φ , wenn eine endliche Folge von Inferenzschritten existiert, sodass man von Φ zu φ gelangt.

Zusammenhang zwischen 'ableitbar' und 'semantisch folgerbar'

Ein brauchbares Beweisverfahren soll nun zwei wichtige Bedingungen erfüllen:

• Korrektheit: Falls Φ ⊦ φ gilt, so gilt auch Φ ⊧ φ. Was 'maschinell' hergeleitet wurde, sollte auch logisch korrekt sein.
• Vollständigkeit: Falls Φ ⊧ φ gilt, so gilt auch Φ ⊦ φ. Was logisch folgerbar ist, sollte auch 'maschinell' herleitbar sein.

Unvollständigkeit von modus ponens und modus tollens

So schön die Inferenzregeln modus ponens und modus tollens auch sind, selbst so einfache Dinge wie die Ableitung von φ = A∨B aus Φ ={A, B} sind nicht möglich. Natürlich könnte man weitere Inferenzregeln hinzunehmen, um die Lücken zu flicken. Was bleibt ist die Frage der Auswahl der jeweils 'richtigen' Regel. Ideal wäre es mit einer einzigen Regel auszukommen.

Aufgabe

Schreibe einen modus-ponens-Beweiser, der z.B. aus der Eingabe

{AvB,B,C,~A&D,B->D,C&D,A}

die Ausgabe

D

herleitet.

'Steinbruch'

Es gilt:

• A∧B ≡ ¬(A→¬B)
• A∨B ≡ ¬A→B

Man kann also '∧' und '∨' durch '→' und '¬' ausdrücken.

lokal