Künstliche Intelligenz und Prolog
Copyright © 2020 Jiri Kriz, www.nosco.ch

7Logik

Prädikatenlogik 1. Ordnung (1. Stufe) gilt in der AI als der wichtigste Formalismus für die Wissens­repräsentation. Probleme werden durch logische Aussagen formuliert und durch Beweismethoden gelöst ("ausgeführt"). Prädikatenlogik ist aber nicht effizient genug ausführbar und bringt noch weitere Probleme mit sich, z.B. Konsistenz der Axiome (A, ¬ A), keine Manipulation der Funktoren, etc..

Horn Klauseln sind eine echte Teilmenge der Prädikatenlogik 1. Ordnung. Sie erlauben z.B. nicht die direkte Darstellung der Disjunktion. Sie sind effizient ausführbar und garantieren Konsistenz. Sie stellen einen universellen Berechnungs­formalismus dar.

Prolog basiert auf Horn Klauseln. Die Syntax von Prolog ist diejenige der Horn Klauseln. Pure Prolog ist semantisch identisch mit Horn Klauseln mit der Ausnahme der Vollständigkeit. D ie Prolog-Beweisstrategie führt dazu, dass (Pure) Prolog im Unterschied zu Horn Klauseln im allgemeinen nicht vollständig ist. Das heisst, das Prolog eine Aussage unter Umständen nicht beweist und terminiert nicht (z.B. im Falle einer Linksrekursion), obwohl die Aussage logisch aus den Programmklauseln folgt. Dieses unerwünschte Verhalten muss der Prolog Programmierer durch eine richtige Reihenfolge der Klauseln vermeiden. Pure Prolog ist korrekt. Das heisst: falls ein Prolog-Beweis terminiert, dann ist er garantiert richtig - die bewiesene Aussage ist eine logische Folgerung der Prolog Datenbank. Das volle Prolog beinhaltet zusätzlich nichtlogische und meta-logische Elemente, die keine Entsprechung in der Logik 1. Ordnung haben.

7.1Prädikaten­logik 1. Ordnung

Syntax

Variablen
A, B, X, Y2, ... (unendlich viele)
Konstanten
a, b, x, y1, ...
Funktionen
f/i, g/j, h/k, .... (Funktions­name / Arität)
Verknüpfungs­operatoren
∧ (und), ∨ (oder), ¬ (not),
⇒ (Implikation nach rechts),
⇐ (Implikation nach links),
⇔ (Äquivalenz)
Quantoren
∀ (für alle),
∃ (es existiert ein)
Term
Variable
Konstante
f( t1, .., tn), f: Funktion, ti: Terme
Formel (logische Aussage)
atomar, d.h. p( t1, ..., tn), p: Prädikat, ti: Terme
zusammen­gesetzt aus anderen Formeln mit Verknüpfungs­operatoren: P ∧ Q, ¬ P, ...
quantifiziert: ∀ X. P, ∃ X. P (X: Variable, P: Formel)
Variablen:A, B, X, Y2, ... (unendlich viele)
Konstanten:a, b, x, y1, ...
Funktionen:f/i, g/j, h/k, .... (Funktionsame / Arität)
Prädikate:p/i, q/j, r/k, .... (Prädikatenname / Arität)
Verknüpfungs­operatoren:∧ (und), ∨ (oder), ¬ (not),
⇒ (Implikation nach rechts),
⇐ (Implikation nach links),
⇔ (Äquivalenz)
Quantoren:∀ (für alle),
∃ (es existiert ein)
Term:Variable
Konstante
f( t1, .., tn), f: Funktion, ti: Terme
Formel (logische Aussage):atomar, d.h. p( t1, ..., tn), p: Prädikat, ti: Terme
zusammengesetzt aus anderen Formeln mit Verknüpfungsoperatoren: P ∧ Q, ¬ P, ...
quantifiziert: ∀ X. P, ∃ X. P (X: Variable, P: Formel)

Terme bezeichnen Objekte (sind Namen von Objekten). Logischen Aussagen werden Wahrheitswerte true oder false zugeordnet.

Semantik (Bedeutung)

Interpretation ist eine Abbildung der abstrakten logischen Symbole auf "konkrete" Weltobjekte. Sie ist gegeben durch:

  1. Vorgabe einer beliebige Menge D der "konkreten" Objekte (Domain)
  2. Vorgabe einer Abbildung der logischen Grundobjekte auf D und {true, false}:
    Konstante c → c' ∈ D
    Funktion f/n → f': Dn -> D
    Prädikat p/n → p': Dn -> {true, false}
    Variable X → beliebiges (nicht spezifiziertes) d ∈ D
  3. Aus der Abbildung der logischen Grundobjekte unter 2) ergibt sich automatisch die Abbildung für alle logischen Objekte nach der folgenden Vorschrift:
    • Term f( t1, ..., tn) → f'( t1', ... tn')
    • Prädikat p( t1, ...tn) → p'( t1', ..., tn') {true, false}
    • Formel → true oder false
      gemäss der Semantik der Verknüpfungs­operatoren und Quantoren (s. Tabelle unten)

Semantik der Verknüpfungs­operatoren:

P ¬ P
true false
false true
P Q P ∧ Q P ∨ Q
true true true true
truefalsefalsetrue
falsetruefalsetrue
falsefalsefalsefalse
PQP ⇒ QP ⇔ Q
truetruetruetrue
truefalsefalsefalse
falsetruetruefalse
falsefalsetruetrue
P Q ¬ P P ∧ Q P ∨ Q P ⇒ Q P ⇔ Q
truetruefalsetruetruetruetrue
truefalsefalsefalsetruefalsefalse
falsetruetruefalsetruetruefalse
falsefalsetruefalsefalsetruetrue

Semantik der Quantoren:

∀X.p(X) = true
genau wenn p(X)=true, für alle X ∈ D (sonst ∀ X. p(X) = false)
∃X.p(X) = true
genau wenn mindestens ein d ∈ D existiert, sodass p(d) = true (sonst ∃ X.p(X) = false)

Der Wert einer Formel (true oder false) heisst der Wahrheitswert der Formel. Er hängt von der Interpretation ab. Bezeichnung:

FI = true
Wahrheitswert der Formel F in der Interpretation I ist true (F ist wahr in I)
FI = false
Wahrheitswert der Formel F in der Interpretation I ist false (F ist falsch in I)

Eine Formel F ist:

Eine Formel F impliziert logisch eine Formel G (G folgt logisch aus F), wenn alle Modelle von F auch Modelle von G sind. D.h. sobald FI = true in einer Interpretation I, so auch GI = true. Notation F |= G. Sinngemäss kann F eine Menge von Formeln sein. Beispiel: P |= P ∨ Q.

Eine Inferenz (Ableitungsregel) ist eine Abbildung: Formeln → Formel, die zur Herleitung neuer Formeln aus bestehenden Formeln dient. Notation: F |- G. Beispiel. { P, P ⇒ Q} |- Q (Modus Ponens).

Eine Beweismethode (proof method) ist eine Menge von Inferenzen. Eine Beweismethode ist korrekt (sound, correct) , wenn die abgeleiteten Formeln auch logische Folgerungen der ursprünglichen Formeln sind, d.h. wenn gilt: falls F |- G, dann F |= G.

Eine Beweismethode ist vollständig> (complete) , wenn alle logische Folgerungen bewiesen werden können, d.h. wenn gilt: falls F |= G, dann F |- G. Bei einer korrekten und vollständigen Beweismethode (z.B. Resolution) gilt: F |- G ist äquivalent zu F |= G.

7.2Prädikaten­logik für Problemlösung

Problem

Gegeben:Formel P1 ∧ P2 ∧ . . .∧ Pn
Gesucht:Formel Q
Problem­lösung in Logik:Ist die Formel "P1 ∧ P2 ∧ . . .∧ Pn ⇒ Q" gültig?
Für welche Werte der Variablen?

Unentscheidbarkeit (Church 1936)

Es gibt keinen Algorithmus, der die Gültigkeit einer beliebigen logischen Formel entscheidet.

Partielle Entscheidbarkeit

Es gibt Algorithmen, die die Gültigkeit beliebiger gültiger logischen Formel beweisen. Bei nicht gültigen Formeln müssen solche Algorithmen nicht terminieren. Beispiel. Resolution.

Resolutionsalgorithmus (Robinson 1965)

Der Resolutionsalgorithmus entscheidet (partiell), ob eine Formel in Klauselform gültig ist. Es gilt:

F = true in allen I,
genau wenn ¬ F = false in allen I,
genau wenn ¬ F' = false in allen I,

wobei F' die Klauselform von F ist. F hat die Form:

F = (P1 ∧ P2 ∧ . . .∧ Pn ⇒ Q) = ¬ P1 ∨ . . .∨ ¬ Pn ∨ Q, also
¬ F = P1 ∧ P2 ∧ . . .∧ Pn ∧ ¬ Q .

Resolution ist ein Beweis durch Widerspruch (refutation): die Folgerung Q wird negiert und ein Widerspruch zwischen ¬ Q und den Annahmen Pi wird bewiesen.

Klauselform

Eine Formel in Klauselform hat die Gestalt

F' = C1 ∧ C2 ∧ ... ∧ Cn, wobei
jedes C = L1 ∨ L2 ∨ ... ∨ Lm (natürlich mit verschiedenen Lj).

Ci heissen Klauseln. Lj sind Literale, d.h. atomare Formeln oder Negationen atomarer For-meln. Alle Variablen in der Klauselform werden implizit universell quantifiziert.

Jede logische Formel F kann in eine Klauselform F' algorithmisch transformiert werden. F und F' sind im allgemeinen nicht logisch äquivalent, aber haben die gleiche Erfüllbarkeit. Der interessanteste Schritt in dieser Transformation ist die Elimination der existentiell quantifizierten Variablen. Dies geschieht durch die Einführung der Skolem Konstanten und Funktionen (Skolemisierung).

Beispiel:

∃ X. p( X) → p( s1)
∀ X. ∃ Y. p( X, Y) → p( X, s2( X))

s1 ist eine neue "Skolem" Konstante, (resp. . s2( X) ist eine neue "Skolem" Funktion) - Objekte, die sonst nirgends vorkommen.

Resolution

Resolution ist eine Inferenzregel, die aus zwei Klausel eine neue Klausel (sog. Resolvente) ableitet.

  1. Resolution für variablenfreie Klauseln:
    C1 = A ∨ B1
    C2 = ¬ A ∨ B2 B1 ∨ B2 (Resolvente R)
    C1 ∧ C2 ist widersprüchlich, genau wenn C1 ∧ C2 ∧ R widersprüchlich ist.
  2. Resolution für Klauseln mit Variablen:
    C1 = A ∨ B1
    C2 = ¬ A' ∨ B2 B1' ∨ B2' (Resolvente R')
    A unifiziert mit A' durch Variablensubstitution S. Analog, B unifiziert mit B' durch die gleiche Variablensubstitution S. C1 ∧ C2 ist widersprüchlich, genau wenn C1' ∧ C2' ∧ R' widersprüchlich ist.
  3. Faktorisierung (factoring)
    Faktorisierung leitet aus einer Klausel eine einfachere Klausel ab.
    A ∨ ¬ A ∨ B B (ohne Variablen)
    A ∨ ¬ A' ∨ B B' (mit Variablen)

Resolutionsalgorithmus

Input:

Folge von Klauseln C1, C2, ..., Cn.
Jede Klausel Ci ist eine Menge von Literalen Lj.

Output:

Falls der Algorithmus terminiert, dann ist C1 ∧ C2 ∧ ... ∧ Cn widersprüchlich.

Algorithmus:

k:= n;
REPEAT
 faktorisiere Klausel, falls möglich;
 wähle Ci, Cj, i ≤ n, j ≤ n,
 sodass A Ci, ¬ A' Cj, und A unifiziert mit A' ;
 k:= k + 1;
 Ck := (Ci' - {A}) + (Cj' - {A'});  (+, -: Mengenoperationen)
UNTIL Ck = {};

Der Algorithmus hat einen exponentiellen Rechenaufwand.

7.3Horn Klauseln

Horn Klauseln sind Klauseln mit höchstens einem positivem Literal:

  1. A ∨ ¬ B1 ∨ . . . ∨ ¬ Bn
  2. ¬ B1 ∨ . . . ∨ ¬ Bn

Die Klausel (1) ist äquivalent zu:

Nicht jede logische Formel kann in Konjunktion von Horn Klausel transformiert werden, z.B. A ∨ B. Die Problemlösung mit Horn Klauseln ("logic programming" im engen Sinne) bedeutet:

Eine wichtige Resolutionsstrategie für Horn Klauseln (mit einem Goal) ist die SLD-Resolution (S = Selector Function, L = Linear, D = Definite Clauses).

Die SLD-Resolution ist korrekt und vollständig für Horn Klauseln.

Prolog benutzt die SLD-Resolution mit left-to-right Selektion und mit einer zusätzlichen Festlegung: Die Programm Klauseln werden in der festen Reihenfolge von oben nach unten für die Resolution versucht (top-down). Die so entstandene depth-first Strategie ist noch korrekt aber nicht mehr vollständig: beweisbare Formeln werden unter Umständen nicht bewiesen, da der Prolog Beweiser nicht terminieren muss (nicht abbrechende Linksrekursion).