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 7 von 102.4

Resolution: Beweisen durch Widerspruch

Die Idee der Resolution

Resolution ist eines der wichtigsten automatischen Beweisverfahren für Logik. Sie arbeitet auf Formeln in KNF und versucht, aus WB ∧ ¬Q einen Widerspruch herzuleiten.

Eine einfache Resolutionsregel lautet:

Resolutionsregel

(A ∨ B), (¬B ∨ C) ⟹ (A ∨ C)

B und ¬B sind komplementär. Sie werden entfernt, die übrigen Literale werden vereinigt.

Die abgeleitete Klausel heißt Resolvente.

Allgemeine Form

Allgemeine Resolution

(A₁ ∨ ... ∨ Aₘ ∨ B), (¬B ∨ C₁ ∨ ... ∨ Cₙ) ⟹ (A₁ ∨ ... ∨ Aₘ ∨ C₁ ∨ ... ∨ Cₙ)

Ein komplementäres Literalpaar wird gelöscht. Alle übrigen Literale bilden die neue Klausel.

Wenn am Ende die leere Klausel entsteht, wurde ein Widerspruch gefunden.

Leere Klausel

□

Die leere Klausel bedeutet: Diese Klauselmenge ist unerfüllbar.

Resolution als verallgemeinerter Modus Ponens

Der Modus Ponens ist die vertraute Regel:

Modus Ponens

A, A → B ⟹ B

Wenn A gilt und aus A B folgt, dann gilt B.

In Klauselform kann A → B als ¬A ∨ B geschrieben werden.

1. A
2. ¬A ∨ B

Resolution:
Res(1,2): B

Man sieht: Resolution kann den Modus Ponens nachbilden, ist aber allgemeiner.

Warum Widerspruchsbeweis?

Um zu zeigen, dass Q aus WB folgt, beweisen wir nicht direkt Q. Wir fügen die negierte Anfrage ¬Q zur Wissensbasis hinzu. Wenn daraus ein Widerspruch folgt, kann ¬Q nicht stimmen.

Resolution-Beweis

WB ⊨ Q ⇔ WB ∧ ¬Q ist unerfüllbar

Resolution sucht dann syntaktisch nach der leeren Klausel.

Mini-Rätsel: Newcastle, Paris, Spanien

Ein klassisches Logikrätsel zeigt, wie Formalisierung, KNF und Resolution zusammenspielen. Wir benutzen:

Variablen

S = Wir fahren nach Spanien. N = Wir kommen aus Newcastle. P = Wir haben in Paris angehalten.

Die Aussagen der Familie werden in Aussagevariablen übersetzt.

Nach der Formalisierung und Umformung erhält man eine Wissensbasis in KNF:

WB ≡ (S ∨ N)₁ ∧ (¬S)₂ ∧ (P ∨ N)₃ ∧ (¬N ∨ P)₄

Jetzt kann Resolution neue Klauseln ableiten:

Res(1,2): (N)₅
Res(3,4): (P)₆
Res(1,4): (S ∨ P)₇

Daraus sieht man: Die Familie kommt aus Newcastle und hat in Paris angehalten. Zusätzlich ist ¬S bereits als Klausel vorhanden: Sie fährt nicht nach Spanien.

NOVA beweist

NOVA fragt: Warum ist die Formalisierung oft schwieriger als der eigentliche Beweis?

Weil natürliche Sprache mehrdeutig ist. Wenn die Variablen oder Regeln falsch gewählt werden, beweist der Kalkül sauber das Falsche.

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...