Aussagenlogik

Jetzt beginnt der mathematische Teil der KI-Grundlagen. Aussagenlogik ist eine formale Sprache, mit der wir einfache Aussagen präzise beschreiben, verknüpfen und automatisch auswerten können. Sie ist ein Fundament für symbolische KI, automatische Beweiser, Expertensysteme, digitale Schaltungsprüfung und später auch für stärkere Logiken wie die Prädikatenlogik.

Wichtig ist der rote Faden: Wir starten nicht direkt mit Beweisen. Zuerst klären wir, welche Formeln überhaupt erlaubt sind. Dann geben wir diesen Formeln Bedeutung. Danach schauen wir, wie aus Wissen neues Wissen folgt. Erst dann kommen Normalformen, Resolution, Hornklauseln und Komplexität.

Abschnitt 6 von 102.3

KNF: Formeln in Beweiser-Form bringen

Warum Normalformen?

Automatische Beweisverfahren sollen nicht mit beliebig wilden Formeln kämpfen müssen. Deshalb bringt man Formeln oft zuerst in eine standardisierte Form. Für Resolution ist die wichtigste Form die konjunktive Normalform, kurz KNF.

KNF

K₁ ∧ K₂ ∧ ... ∧ Kₘ

Eine KNF ist eine Konjunktion von Klauseln.

Klausel

L₁ ∨ L₂ ∨ ... ∨ Lₙ

Eine Klausel ist eine Disjunktion von Literalen.

Literal

A oder ¬A

Ein Literal ist eine Variable oder eine negierte Variable.

Beispiel einer KNF

KNF

(A ∨ B ∨ ¬C) ∧ (A ∨ B) ∧ (¬B ∨ ¬C)

Das ist eine Konjunktion von drei Klauseln. Jede Klausel ist ein Oder von Literalen.

Die KNF sieht auf den ersten Blick technischer aus als normale Formeln. Dafür ist sie maschinenfreundlich: Ein Beweiser kann Klauseln vergleichen, komplementäre Literale finden und Resolution anwenden.

Jede Formel kann in KNF transformiert werden

Aussagenlogik verliert dadurch keine Ausdruckskraft. Jede aussagenlogische Formel lässt sich in eine semantisch äquivalente KNF bringen.

Satz

Jede aussagenlogische Formel lässt sich in eine äquivalente KNF transformieren.

Die Formel sieht danach anders aus, hat aber unter allen Belegungen denselben Wahrheitswert.

Schritt-für-Schritt-Beispiel

Wir bringen die Formel A ∨ B → C ∧ D in KNF. Dazu nutzen wir die Äquivalenzen aus der Aussagenlogik.

A ∨ B → C ∧ D
≡ ¬(A ∨ B) ∨ (C ∧ D)                         Implikation auflösen
≡ (¬A ∧ ¬B) ∨ (C ∧ D)                         De Morgan
≡ (¬A ∨ (C ∧ D)) ∧ (¬B ∨ (C ∧ D))             Distributivgesetz
≡ (¬A ∨ C) ∧ (¬A ∨ D) ∧ (¬B ∨ C) ∧ (¬B ∨ D)   Distributivgesetz + Assoziativität

Am Ende steht ein Und von Oder-Klauseln. Genau das ist KNF.

Zwischenfrage

NOVA fragt: Warum wirkt KNF komplizierter, ist aber für Maschinen einfacher?

Weil alle Formeln in dieselbe Struktur gebracht werden: Klauseln aus Literalen. Darauf kann ein Beweisverfahren systematisch arbeiten.

NOVA wird geladen...

NOVA Energie-Log

RTX-Verbrauch

NOVA schätzt hier, wie viel GPU-Energie deine Bildanalyse- und CUDA-Läufe bisher ungefähr verbraucht haben.

Lade Energie-Daten...