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 8 von 102.5

Hornklauseln und das Skifahren-Beispiel

Warum Hornklauseln so wichtig sind

Eine allgemeine KNF-Klausel kann mehrere positive und negative Literale enthalten. Für viele regelbasierte Systeme ist aber eine besondere Form wichtig: Hornklauseln.

Hornklausel

Eine Klausel mit höchstens einem positiven Literal.

Dadurch lässt sie sich oft klar als Wenn-dann-Regel lesen.

Regelform

A₁ ∧ ... ∧ Aₘ → B

Wenn alle Voraussetzungen A₁ bis Aₘ gelten, dann folgt B.

Fakt

Eine Hornklausel mit nur einem positiven Literal kann als Fakt gelesen werden.

Skifahren als Wissensbasis

Jetzt kommt das wichtige Beispiel, das im KI-Kontext besonders gut zeigt, wie Regeln und Fakten zusammenarbeiten. Die Wissensbasis enthält:

1. Wetter_schön
2. Schneefall
3. Schneefall → Schnee
4. Wetter_schön ∧ Schnee → Skifahren

Frage:

Anfrage

Gilt Skifahren?

Kann aus den Fakten und Regeln hergeleitet werden, dass Skifahren folgt?

Forward Chaining: von Fakten zur Anfrage

Beim Forward Chaining startet der Beweis bei den Fakten. Alles, was aus bekannten Fakten und Regeln folgt, wird nach und nach hinzugefügt.

Fakten:
1. Wetter_schön
2. Schneefall

Regel:
3. Schneefall → Schnee

Modus Ponens:
MP(2,3): Schnee₅

Regel:
4. Wetter_schön ∧ Schnee → Skifahren

Modus Ponens:
MP(1,5,4): Skifahren₆

Ergebnis: Skifahren ist bewiesen.

Backward Chaining: von der Anfrage zurück zu den Fakten

Beim Backward Chaining startet man mit dem Ziel und fragt: Was müsste gelten, damit dieses Ziel bewiesen ist?

Ziel:

Ziel

Skifahren

Wir wollen zeigen, dass Skifahren folgt.

Die Regel Wetter_schön ∧ Schnee → Skifahren sagt: Um Skifahren zu beweisen, müssen wir Wetter_schön und Schnee beweisen.

Wetter_schön ist ein Fakt. Schnee folgt aus Schneefall. Schneefall ist ebenfalls ein Fakt. Damit ist das Ziel bewiesen.

Ziel: Skifahren

Skifahren braucht:
- Wetter_schön
- Schnee

Wetter_schön ist Fakt.
Schnee braucht:
- Schneefall

Schneefall ist Fakt.

Also:
Skifahren ist beweisbar.

SLD-Resolution in der Idee

In der Logikprogrammierung, besonders bei Prolog, wird eine spezielle Form der Resolution verwendet: SLD-Resolution. Sie arbeitet zielgerichtet rückwärts mit Teilzielen.

Für unser Skifahren-Beispiel ergänzt man die negierte Anfrage:

1. Wetter_schön
2. Schneefall
3. Schneefall → Schnee
4. Wetter_schön ∧ Schnee → Skifahren
5. Skifahren → f

Dann arbeitet die Resolution rückwärts:

Res(5,4): Wetter_schön ∧ Schnee → f
Res(...,1): Schnee → f
Res(...,3): Schneefall → f
Res(...,2): □

Die leere Klausel zeigt den Widerspruch. Also folgt Skifahren aus der Wissensbasis.

Zwischenfrage

NOVA fragt: Warum sind Hornklauseln für KI-Systeme so praktisch?

Weil sie wie klare Regeln lesbar sind: Wenn Voraussetzungen gelten, dann folgt genau ein Kopf. Das macht Suche und Erklärung einfacher.

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