7Logik
Prädikatenlogik 1. Ordnung (1. Stufe) gilt in der AI als der wichtigste Formalismus für die Wissensreprä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 Berechnungsformalismus 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ädikatenlogik 1. Ordnung
Syntax
- Variablen
- A, B, X, Y2, ... (unendlich viele)
- Konstanten
- a, b, x, y1, ...
- Funktionen
- f/i, g/j, h/k, .... (Funktionsname / Arität)
- Verknüpfungsoperatoren
- ∧ (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)
| 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üpfungsoperatoren: | ∧ (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:
- Vorgabe einer beliebige Menge D der "konkreten" Objekte (Domain)
- 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 - 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üpfungsoperatoren und Quantoren (s. Tabelle unten)
Semantik der Verknüpfungsoperatoren:
| P | ¬ P | ||
|---|---|---|---|
| true | false | ||
| false | true | ||
| P | Q | P ∧ Q | P ∨ Q |
| true | true | true | true |
| true | false | false | true |
| false | true | false | true |
| false | false | false | false |
| P | Q | P ⇒ Q | P ⇔ Q |
| true | true | true | true |
| true | false | false | false |
| false | true | true | false |
| false | false | true | true |
| P | Q | ¬ P | P ∧ Q | P ∨ Q | P ⇒ Q | P ⇔ Q |
|---|---|---|---|---|---|---|
| true | true | false | true | true | true | true |
| true | false | false | false | true | false | false |
| false | true | true | false | true | true | false |
| false | false | true | false | false | true | true |
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:
-
erfüllbar
(konsistent),
(satisfiable,
consistent):
es existiert eine Interpretation I, sodass FI = true (I heisst Modell von F)
Beispiel: p ∧ q = true in der Interpretation I = { p -> true, q -> true} - gültig (valid):
FI = true in allen Interpretationen (F ist "wahr")
Beispiel: p( X) ∨ ¬ p( X) = true - widersprüchlich
(unerfüllbar,
inkonsistent),
(unsatisfiable,
inconsistent):
es existiert keine Interpretation I, sodass FI = true (F ist nicht erfüllbar), d.h.
FI = false in allen Interpretationen
Beispiel: p( X) ∧ ¬ p( X) = false
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ädikatenlogik für Problemlösung
Problem
| Gegeben: | Formel P1 ∧ P2 ∧ . . .∧ Pn |
| Gesucht: | Formel Q |
| Problemlö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.
- 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. - 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. - 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:
- A ∨ ¬ B1 ∨ . . . ∨ ¬ Bn
- ¬ B1 ∨ . . . ∨ ¬ Bn
Die Klausel (1) ist äquivalent zu:
- A ⇐ B1 ∧ B2 ∧ . . . ∧ Bn.
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:
- Darstellung des Bekannten durch Fakten (Klausel (1) mit n = 0) und Regeln (Klauseln (1)). Diese Horn Klauseln, die genau ein positives Literal haben, heissen auch Definite Clauses. Diese Klauseln werden auch Programmklauseln genannt (Pi). Sie spielen die Rolle der Axiome des Problems.
- Darstellung des Gesuchten als G = G1 ∧ G2 ∧ . . . ∧ Gm. (G = Goal).
- Beweis der Formel
P1 ∧ P2 ∧ . . .∧ Pn ⇒ G
durch Resolution. Die Formel wird negiert zu:
P1 ∧ P2 ∧ . . .∧ Pn ∧ ¬ G
und durch Widerspruch bewiesen. Es ist:
¬ G = ¬ G1 ∨ . . . ∨ ¬ Gn,
d.h. ¬ G ist eine Horn Klausel vom Typ (2).
Eine wichtige Resolutionsstrategie für Horn Klauseln (mit einem Goal) ist die SLD-Resolution (S = Selector Function, L = Linear, D = Definite Clauses).
- Linear:
Starte mit der Resolvente R0 := ¬ G. In jedem Resolutionsschritt i bilde die Resolvente Ri zwischen einem früheren Rj, j < i, und einer "anderen Klausel" C. - Definite:
Die "andere Klausel" C ist eine Programm Klausel und dies ist eine definite Clause. (Wäre es keine definite Clause, so würde das Verfahren Input-Strategie heissen). - Selector Function:
Das Literal in der Goal Klausel wird für die Resolution nach einer festen Auswahlregel gewählt (z.B. immer das erste Literal, d.h. left-to-right).
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).