Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2...
Transcript of Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2...
Logik für Informatiker Wintersemester 2012/13
2 Prädikatenlogik
In der Prädikatenlogik kann man die in der Aussagenlogik bereits
betrachteten atomaren Aussagen eleganter formulieren:
A = „Borussia Dortmund ist deutscher Fußballmeister“:
deutscher_fussballmeister(’Borussia Dortmund ’ , 2012 ).
B = „eine Stadt mit mindestens 100000 Einwohnern ist groß“:
grosse_stadt(Stadt)← einwohner(Stadt ,X ) ∧X ≥ 100000 .
C = „Würzburg hat über 300.000 Einwohner“:
einwohner(’Wuerzburg ’ , 300000 ).
Dann kann man generische Aussagen machen. Z.B. ist die Formel zu B auf
alle Städte mit mindestens 100000 Einwohnern anwendbar.
Prof. Dr. Dietmar Seipel 145
Logik für Informatiker Wintersemester 2012/13
2.1 Grundbegriffe der Prädikatenlogik
Erweiterung der Aussagenlogik um
Variablen– }
Symbole
U, V,W,X, Y, Z
Funktions– f, g, h a, b, c
Prädikaten– p, q, r
und Quantoren:
• Existenzquantor:∃,
• Allquantor:∀.
Die bekannten Junktoren∧, ∨, ¬ und→ sind weiterhin erlaubt.
Prof. Dr. Dietmar Seipel 146
Logik für Informatiker Wintersemester 2012/13
Beispiel (Prädikatenlogiche Formeln)
1. Konvergenz, Grenzwert:
limn→∞ f(n) = a ist in der Analysis definiert als
∀ ǫ > 0 ∃n0 ∀n ≥ n0 |f(n)− a| < ǫ.
Hier sindǫ, n0 undn Variablensymbole (nur über diese kann man
quantifizieren),0, a, f ,− und | . . . | sind Funktionssymbole, und>,≥
und< sind Prädikatensymbole.
Funktionssymbole ohne Argumente – wie0 unda – nennt man auch
Konstantensymbole; ihre Stelligkeit ist0. f und | . . . | sind1–stellig,
− ist 2–stellig. Hier sind auch alle Prädikatensymbole2–stellig.
Fürf(n) = 1/n gilt z.B. limn→∞ f(n) = limn→∞ 1/n = 0 = a.
Für jede vorgegebene reelle Zahlǫ > 0 existiert einn0 ∈ IN , etwa
n0 = ⌈1/ǫ⌉+ 1, so daß für allen ≥ n0 gilt |1/n− 0| < ǫ.
Prof. Dr. Dietmar Seipel 147
Logik für Informatiker Wintersemester 2012/13
2. Konjunktion:
(∃ Jahr weltmeister(brasilien, Jahr)) ∧
(∀ Jahr ¬weltmeister(nigeria, Jahr))
• Brasilien war bereits Fußballweltmeister, d.h.:
es gibt ein Jahr, in dem Brasilien Fußballweltmeister war;
• Nigeria aber noch nicht.
3. Implikation:
∀ Stadt ∀X ( grosse_stadt(Stadt)←
einwohner(Stadt ,X ) ∧X ≥ 100000 )
ist äquivalent zu
∀ Stadt ( grosse_stadt(Stadt)←
∃X ( einwohner(Stadt ,X ) ∧X ≥ 100000 ) )
Prof. Dr. Dietmar Seipel 148
Logik für Informatiker Wintersemester 2012/13
Syntax
Wir setzen folgende abzählbaren Mengen voraus:
• Variablensymbole: V = {X1, X2, . . . },
• Funktionssymbole:F = { f1, f2, . . . },
• Prädikatensymbole:P = { p1, p2, . . . }.
Jedes Funktions– bzw. Prädikatensymbol hat eineStelligkeitk ∈ IN0.Schöningh schreibtfk
i , pki , wir schreibenfi/k, pi/k.
Allerdings kann dasselbe Funktions– bzw. Prädikatensymbol in einerFormel mit unterschiedlichen Stelligkeiten auftreten. In
f(f(a), f(a, a, a))
ist das erste Auftreten vonf zweistellig, das zweite einstellig, und das drittedreistellig. Eigentlich handelt es sich dabei um unterschiedicheFunktionssymbolef/2, f/1 undf/3 mit demselben Namenf .
Prof. Dr. Dietmar Seipel 149
Logik für Informatiker Wintersemester 2012/13
Induktive Definitionen
Terme
1. Jedes VariablensymbolX ∈ V ist ein Term.
2. Istf ein Funktionssymbol der Stelligkeitk, und sindt1, . . . , tk(ebenso viele) Terme, so ist auchf(t1, . . . , tk) ein Term.
3. Istk = 0, so schreibt man kurzf ausstelle vonf(), und man nenntfdann eineKonstante.
Beispiel (Terme)
• f1(X2),
• f3(f2, f1(X3)).
Stelligkeiten:f1 f2 f3
1 0 2
Prof. Dr. Dietmar Seipel 150
Logik für Informatiker Wintersemester 2012/13
Formeln
1. Für eink–stelliges Prädikatensymbolp und Termet1, . . . tk istp(t1, . . . , tk) eineatomare Formel.Fallsk = 0 ist, so schreiben wir kurzp anstelle vonp().
2. Für jede FormelF ist auch¬F eine Formel.
3. SindF1 undF2 Formeln, so auch(F1 ∧ F2) und(F1 ∨ F2).
4. FallsX ein Variablensymbol ist undF eine Formel, so sind auch∃X F und∀X F Formeln.
Man kann wieder redundante Klammerpaare weglassen, und Teilformelnwerden analog zur Aussagenlogik definiert.
Man könnte weitere Formeln mittels anderer Junktoren bilden, z.B. dieImplikationF1 → F2. Andererseits könnte man diese Formel auch wie
¬F1 ∨ F2 auffassen.
Prof. Dr. Dietmar Seipel 151
Logik für Informatiker Wintersemester 2012/13
Beispiel (Formeln)
1. In der Formel
F = (∃X1 p1(X1, f1(X2))) ∨ (∀X2 p2(X2, f3(f2, f1(X3))))
haben die Prädikatensymbole die folgenden Stelligkeiten:
p1 p2
2 2
2. Man kann auch über Variablensymbole quantifizieren, die nicht in derbetroffenen Formel vorkommen:F = ∀X p(Y ).
3. In der folgenden Implikation bezeichnen die beiden Vorkommen vonXdasselbe:F = ∀X ( student(X)→ person(X) ).
4. In F = ∀X ( p(X )→ ∃X q(X) ) bezieht sich die Allquantifizierung∀X aufp(X), die Existenzquantifizierung∃X auf q(X). Es gibtkeinen Zusammenhang zwischen den beiden Vorkommen vonX .
Prof. Dr. Dietmar Seipel 152
Logik für Informatiker Wintersemester 2012/13
Klammerungsregeln
1. Wir nehmen an, daß die Quantoren am stärksten binden. D.h.
QX F ⊗G bedeutet(QX F )⊗G,
für einen QuantorQ ∈ {∀, ∃ } und einen Junktor⊗ ∈ {∧,∨,→}.
Z.B. bedeutet
∀X ∀Y ( ∃Z (p(X,Z) ∧ p(Z, Y ))→ p(X, Y ) )
dasselbe wie
∀X ∀Y ( (∃Z (p(X,Z) ∧ p(Z, Y )))→ p(X, Y ) )
2. Wir nehmen an, daß die Negation stärker bindet als die Konjunktion,
die Disjunktion und die Implikation, und wir nehmen an, daß die
Konjunktion stärker bindet als die Disjunktion (Punkt vor Strich) und
die Implikation, und die Disjunktion stärker als die Implikation. D.h.
F ∨ ¬G ∧G′ → H bedeutet(F ∨ ((¬G) ∧G′))→ H.
Prof. Dr. Dietmar Seipel 153
Logik für Informatiker Wintersemester 2012/13
Schreibweisen
Die Formel
∀ ǫ > 0 ∃n0 ∀n ≥ n0 |f(n)− a| < ǫ
müßte man eigentlich ausführlich wie folgt schreiben:
∀ǫ ( ǫ ∈ IR ∧ ǫ > 0 →
∃n0 (n0 ∈ IN ∧
∀n (n ∈ IN ∧ n ≥ n0 → |f(n)− a| < ǫ ) ) ).
In der Kurzschreibweise wurde implizit angenommen, daßǫ eine reelle
Zahl ist, und daßn undn0 natürliche Zahlen sind.
Daneben wurde die vereinfachende Infix– bzw. Zirkumfix–Notation für
Funktions– und Prädikatensymbole verwendet.
Manchmal schreibt man anstelle von∀X F auch∀X : F ; analog für∃.
Prof. Dr. Dietmar Seipel 154
Logik für Informatiker Wintersemester 2012/13
Infix– und Zirkumfix–Notation
Zur leichteren Lesbarkeit kann man gewisse binäre Funktions– und
Prädikatensymbole in Infix–Notation schreiben.
Anstelle der Präfix–Notation⊙(t1, t2) schreiben wir dann die
Infix–Notationt1 ⊙ t2.
Die atomare Formel
|f(n)− a| < ǫ
mit dem binären Prädikatensymbol< und dem binären Funktionssymbol−
würde in Präfix–Notation wie folgt aussehen:
< ( || (−(f(n), a)), ǫ )
Einen Term||(t) mit dem unären Funktionssymbol|| (Betrag) können wir in
Zirkumfix–Notation|t| schreiben.
Prof. Dr. Dietmar Seipel 155
Logik für Informatiker Wintersemester 2012/13
Freie und gebundene Variablen
1. Ein Vorkommen einer VariableX in einer FormelF heißtgebunden,
falls X quantifiziert in einer Teilformel vonF der Form∃X G oder
∀X G vorkommt (d.h. im Geltungsbereich eines Quantors überX).
2. Andernfalls heißt das Vorkommen vonX frei.
3. Eine FormelF ohne Vorkommen von freien Variablen heißt
geschlossen, oder eine Aussage. Andernfalls heißtF offen.
Beispiel: Die folgende FormelF ist offen:
F = (∃X1 p1(X1, f1(X2))) ∨ (∀X2 p2(X2, f3(f2, f1(X3)))).
• Die beiden unterstrichenen Vorkommen der VariablenX1 undX2 sind
gebunden. Alle anderen Vorkommen sind frei.
• Das (einzige) Vorkommen vonX3 ist frei.
Prof. Dr. Dietmar Seipel 156
Logik für Informatiker Wintersemester 2012/13
Definition (Semantik der Prädikantenlogik)
EineStrukturist ein PaarA = (UA, IA) mit
1. UA ist eine beliebige, nicht–leere Menge, genannt GrundmengevonA,
Grundbereich, Individuenbereich, Universum.
2. IA ist eine partielle Abbildung aufV ∪ F ∪ P mit
• jedemk–stelligen Prädikantensymbolp ∈ P ∩ def (IA) ist ein
k–stelliges PrädikatIA(p) überUA zugeordnet, d.h. eine Relation
IA(p) ⊆ UkA.
• jedemk–stelligen Funktionssymbolf ∈ F ∩ def (IA) ist eine
k–stellige FunktionIA(f) : UkA → UA zugeordnet.
• jedem VariablensymbolX ∈ V ∩ def (IA) ist ein Individuum
IA(X) ∈ UA zugeordnet.
Dabei istUkA die Menge allerk–Tupel mit Komponenten ausUA.
Prof. Dr. Dietmar Seipel 157
Logik für Informatiker Wintersemester 2012/13
Der Definitionsbereichdef (IA) der partiellen AbbildungIA ist meist eine
echte Teilmenge vonV ∪ F ∪ P:
def (IA) ⊆ V ∪ F ∪ P .
Die StrukturA paßtzu einer FormelF , falls IA für alle inF
vorkommenden Prädikaten–, Funktions– und Variablensymbole für freie
Variablen definiert ist.
Abkürzung:
IA(α) = αA, für alleα ∈ V ∪ F ∪ P .
Fallsα außerhalb des Definitionsbereichsdef (IA) liegt, so istαA
undefiniert.
Prof. Dr. Dietmar Seipel 158
Logik für Informatiker Wintersemester 2012/13
Beispiel (Struktur)
Die folgende StrukturA paßt zur Formel
F = ∀X p(X, f(X)) ∧ q(g(a, Z)).
Die Grundmenge vonA und die Interpretation der Prädikaten– und
Funktionssymbole seien wie folgt:
UA = IN0 = { 0, 1, 2, . . . },
pA = { (m,n) ∈ IN20 |m < n },
qA = { (n) ∈ IN10 | n ist eine Primzahl},
fA(n) = n+ 1, d.h.fA ist die Nachfolgerfunktion aufIN0,
gA(n,m) = n+m, d.h.gA ist die Additionsfunktion aufIN0.
Das0–stellige Funktionssymbola werde alsaA = 2 interpretiert, und die
Variablensymbole alsXA = 23, ZA = 3.
Prof. Dr. Dietmar Seipel 159
Logik für Informatiker Wintersemester 2012/13
In dieser StrukturA gilt F offensichtlich (die entsprechenden Definitionen
der Semantik folgen noch), denn
• die NachfolgerfunktionfA paßt zur Kleiner–RelationpA:
p(X, f(X)) entspricht inA dem VergleichX < X + 1; und
• gA(aA, ZA) = 2 + 3 = 5 ist in der Primzahl–RelationqA.
Ändert man dagegenqA zu
qA′
= { (n) ∈ IN10 | n ist eine gerade Zahl},
und läßt den Rest unverändert, so giltF in der veränderten StrukturA′
nicht, da5 keine gerade Zahl ist.
Wenn man eine fest vorgegebene Interpretation eines Funktions– oder
Prädikatensymbols betrachten will, dann muß man diese durch Hinzunahme
geeigneter Axiome zuF erzwingen.
Prof. Dr. Dietmar Seipel 160
Logik für Informatiker Wintersemester 2012/13
Definition (Semantik der Prädikatenlogik)
Wir betrachten im folgenden FormelnF und zuF passende StrukturenA.
Der WertA(t) eines Termst wird induktiv definiert als:
1. A(t) = tA, falls t ∈ V eine Variable ist.
2. A(t) = fA(A(t1), . . . ,A(tk)), falls t = f(t1, . . . , tk) ein komplexer
Term ist.
Eine Herbrand–Struktur bildet alle Terme auf sich selbst ab.
FürX ∈ V undu ∈ UA seiA[X|u] diejenige StrukturB, welche man ausA
erhält, indem manXA aufXB = u ändert undA ansonsten unverändert läßt:
• für alleα ∈ P ∪ F ∪ V \ {X} gilt αB = αA,
• XB = u (unabhängig vonXA).
Prof. Dr. Dietmar Seipel 161
Logik für Informatiker Wintersemester 2012/13
Der WahrheitswertA(F ) wird dann ebenfalls induktiv definiert:
A(p(t1, . . . , tk)) =
1, falls (A(t1), . . . ,A(tk)) ∈ pA
0, sonst
A(¬G) = ¬A(G),
A(F1 ∧ F2) = A(F1) ∧ A(F2),
A(F1 ∨ F2) = A(F1) ∨ A(F2),
A(∀XG) =
1, falls für alleu ∈ UA gilt A[X|u](G) = 1
0, sonst
A(∃XG) =
1, falls es einu ∈ UA gibt mitA[X|u](G) = 1,
0, sonst
Damit gilt offensichtlich auchA(F → G) = A(F )→ A(G).
Prof. Dr. Dietmar Seipel 162
Logik für Informatiker Wintersemester 2012/13
Die Definitionen für die booleschen Junktoren sind exakt analog zur
Aussagenlogik. Die Fallunterscheidungen könnte man wie folgt abkürzen:
A(p(t1, . . . , tk)) = (A(t1), . . . ,A(tk)) ∈ pA,
A(∀XG) = ∧u∈UA A[X|u](G),
A(∃XG) = ∨u∈UAA[X|u](G).
1. Ersteres gilt, da der Teste ∈M auf Elementschaft in einer Menge
einen der Wahrheitswerte1 oder0 als Resultat hat.
2. Die – potentiell unendliche – Konjunktion im zweiten Teilist genau
dann1, wenn für alleu ∈ UA gilt A[X|u](G) = 1.
3. Die – potentiell unendliche – Disjunktion im dritten Teilist genau
dann1, wenn es (mindestens) einu ∈ UA gibt mitA[X|u](G) = 1.
Prof. Dr. Dietmar Seipel 163
Logik für Informatiker Wintersemester 2012/13
Die Prädikatenlogik verallgemeinert die Aussagenlogik.
Die atomaren Formelnp der Aussagenlogik entsprechen0–stelligen
Prädikatensymbolen.
Es gibt es nur zwei mögliche RelationenpA ⊆ U 0A = {( )} :
• FallspA = {( )} nur das0–stellige Tupel( ) enthält, so istA(p) = 1.
• FallspA = {} leer ist, so istA(p) = 0.
In der Aussagenlogik gibt es keine höherstelligen Prädikatensymbole, und
deswegen braucht man auch keine Variablen– bzw. Funktionssymbole um
Terme zu bilden.
Auch die Quantifizierung ist in der Aussagenlogik sinnlos, da es dort keine
Variablensymbole gibt.
Prof. Dr. Dietmar Seipel 164
Logik für Informatiker Wintersemester 2012/13
Definition (Modelle)
1. Eine StrukturA erfüllt eine FormelF , fallsA zuF paßt und
A(F ) = 1 ist.
2. Dann sagen wir auch, daß die FormelF in A gilt.
3. Dann istA ein Modell vonF , und wir schreiben auchA |= F .
Herbrand–Strukturen
In der Praxis arbeitet man meist mit geschlossenen FormelnF und
Herbrand–StrukturenA = (UA, IA) :
1. Ihre GrundmengeUA besteht aus den Termen über den
Funktionssymbolen vonF . Terme werden nicht interpretiert.
2. Herbrand–Strukturen können also alleine durch die Interpretation der
Prädikatensymbole charakterisiert werden.
Prof. Dr. Dietmar Seipel 165
Logik für Informatiker Wintersemester 2012/13
Variablenbelegungen
• Für geschlossene FormelnF ist die Belegung der VariablenX ∈ V mit
WertenXA ∈ UA irrelevant.
• Für eine quantifizierte VariableX werden sowieso alle Strukturen
A[X|u] für u ∈ UA untersucht – ohne den WertXA zu beachten.
• Der WertXA einer VariableX ist nur relevant, fallsX mindestens
einmal frei inF vorkommt.
Für die FormelF = ( ∀X p(X) ) ∧ q(X) mit je einem gebundenen
und einem freien Vorkommen des VariablensymbolsX , istXA nur für
das zweite Vorkommen vonX relevant. Es giltpA[X|u] = pA und
A(F ) = ∧u∈UAA[X|u](p(X)) ∧ A(q(X))
= ∧u∈UA(u) ∈ pA ∧ (XA) ∈ qA.
Prof. Dr. Dietmar Seipel 166
Logik für Informatiker Wintersemester 2012/13
Beispiel (Herbrand–Struktur, Modell)
Wir betrachten die folgende geschlossene FormelF :
F = f ∧ ∀X r,
f = married(a, b),
r = student(X )→ person(X ).
a undb sind verheiratet, und jeder Studierende ist eine Person.
Wir betrachten eine Herbrand–StrukturA. Diese bildet alle
Funktionssymbole auf sich selbst ab. Hier gibt es nur Konstanten, d.h.
0–stellige Funktionssymbole; diese bilden die GrundmengeUA.
UA = { a, b },
αA = α, für alle Konstantenα ∈ UA.
Prof. Dr. Dietmar Seipel 167
Logik für Informatiker Wintersemester 2012/13
Wir werden später sehen, daß man das gebundene Variablensymbol X in∀X r umbenennen könnte, z.B. inY . Dann würde man die Teilformel
∀ Y ( student(Y )→ person(Y ) )
erhalten, die – entsprechend unserer Anschauung – zu∀X r äquivalent ist,da man fürX undY sowieso alle Werteu ∈ UA einsetzen kann.
Wir interpretieren die Prädikatensymbole wie folgt:
marriedA = { (a, b) },
studentA = { (a), (b) },
personA = { (a) }.
Diese Interpretationen könnte man durch eine einzige Mengevon Atomenrepräsentieren:
I = {married(a, b), student(a), student(b), person(a) }.
Prof. Dr. Dietmar Seipel 168
Logik für Informatiker Wintersemester 2012/13
Dann gilt
A(f) = (a, b) ∈ marriedA = 1,
A(∀X r) = ∧u∈UA ( (u) ∈ studentA → (u) ∈ personA )
= ( (a) ∈ studentA → (a) ∈ personA ) ∧
( (b) ∈ studentA → (b) ∈ personA )
= 0,
da(b) 6∈ personA. Dastudent undperson 1–stellige Prädikatensymbole
sind, werden Tupel(u) ∈ U1A mit nur einer Komponente untersucht.
Also ist die untersuchte StrukturA zwar ein Modell vonf , aber kein
Modell von∀X r, und somit auch kein Modell vonF .
Die StrukturA paßt zuF auch ohne eine InterpretationXA des
VariablensymbolsX anzugeben, da überX quantifiziert wird.
Prof. Dr. Dietmar Seipel 169
Logik für Informatiker Wintersemester 2012/13
Beispiel (Herbrand–Struktur, Modell)
Wir betrachten die folgende geschlossene FormelF :
F = f1 ∧ f2 ∧ f3 ∧ ∀X ∀Y ∀Z r,
f1 = father(a, b),
f2 = brother(b, c),
f2 = brother(b, d),
r = father(X ,Y ) ∧ brother(Y ,Z )→ uncle(X ,Z ).
Ein OnkelZ vonX ist ein Bruder des VatersY . Man könntefather undbrother auch mittels zweier Prädikateparent undmale definieren.
Wir betrachten wieder eine Herbrand–StrukturA, die die Konstanten (hierdie einzigen Funktionssymbole) inF auf sich selbst abbildet:
UA = { a, b, c, d },
αA = α, für alle Konstantenα ∈ UA.
Prof. Dr. Dietmar Seipel 170
Logik für Informatiker Wintersemester 2012/13
Wir interpretieren die Prädikatensymbole wie folgt:
fatherA = { (a, b) },
brotherA = { (b, c), (b, d) },
uncleA = { (a, c) }.
Für die Variablenbelegung
XA = a, Y A = b, ZA = c,
istA ein Modell für die Faktenf1, f2, f3, und die Regelr:
A(r) = A(father(X ,Y )) ∧ A(brother(Y ,Z ))→ A(uncle(X ,Z ))
= (a, b) ∈ fatherA ∧ (b, c) ∈ brotherA → (a, c) ∈ uncleA
= 1 ∧ 1→ 1 = 1.
Der Wahrheitswert vone ∈M ist 1, falls e ∈M gilt, sonst0.
Prof. Dr. Dietmar Seipel 171
Logik für Informatiker Wintersemester 2012/13
Die StrukturA[Z|d] interpretiert die Prädikatensymbole wieA.
A[Z|d] ist ebenfalls ein Modell für die Faktenf1, f2, f3.
Da (a, d) 6∈ uncleA, istA[Z|d] aber kein Modell für die Regelr:
A[Z|d](r) = A[Z |d](father(X ,Y )) ∧ A[Z |d](brother(Y ,Z ))
→ A[Z |d](uncle(X ,Z ))
= (a, b) ∈ fatherA ∧ (b, d) ∈ brotherA → (a, d) ∈ uncleA
= 1 ∧ 1→ 0 = 0.
Also istA auch kein Modell für die quantifizierte Regel∀X ∀Y ∀Z r, undsomit auch kein Modell für die komplette FormelF .
Wenn wir die Interpretation vonuncle erweitern zu
uncleA′
= { (a, c), (a, d) }
und sonst alles wie inA belassen, dann erhalten wir ein ModellA′ vonF .
Prof. Dr. Dietmar Seipel 172
Logik für Informatiker Wintersemester 2012/13
Logische Folgerung, Erfüllbarkeit, Gültigkeit
SeienF undG prädikatenlogische Formeln.
1. G folgt logischausF , falls jedes ModellA vonF auch ein Modell vonG ist. Dann schreiben wirF |= G.
2. F ist erfüllbar, falls es ein Modell vonF gibt.
3. F ist gültig, falls jede zuF passende Struktur ein Modell vonF ist.
Man kann die logische Folgerung auf die Erfüllbarkeit bzw. die Gültigkeitzurückführen:
F |= G ⇐⇒
F ∧ ¬G ist unerfüllbar ⇐⇒ ¬ (F ∧ ¬G) ist gültig.
Man kann die bekannten Begriffe auf FormelmengenF ausdehnen.Eine endliche FormelmengeF = { f1, . . . , fn } ist dabei äquivalent zueiner Konjunktionf1 ∧ . . . ∧ fn.
Prof. Dr. Dietmar Seipel 173
Logik für Informatiker Wintersemester 2012/13
2.2 Normalformen
Wir werden im folgenden sehen, daß man eine prädikatenlogische Formel
äquivalent umformen kann, so daß alle Quantoren am Anfang der Formel
stehen (Pränexform).
Man kann sogar noch – mittels Skolemfunktionen – alle Existenzquantoren
entfernen (Skolemform). Die Skolemform ist genau dann erfüllbar, wenn
die Ausgangsformel erfüllbar ist.
Die Skolemform kann man dann – wie in der Aussagenlogik – auf
Klauselform bringen (KNF). Darauf können wir dann eine verallgemeinerte
Resolutionsmethode anwenden.
Prof. Dr. Dietmar Seipel 174
Logik für Informatiker Wintersemester 2012/13
Definition (Äquivalenz)
Zwei prädikatenlogische FormelnF undG heißenäquivalent,
falls für alle sowohl zuF als auch zuG passenden StrukturenA gilt:
A(F ) = A(G).
Dann schreiben wirF ≡ G.
Satz (Äquivalenz)
1. Negation vertauscht die Quantoren∀ und∃:
¬∀X F ≡ ∃X ¬F,
¬∃X F ≡ ∀X ¬F.
Nicht alle Strukturen passen zuF ist z.B. äquivalent zu
es gibt Strukturen, die nicht zuF passen.
Prof. Dr. Dietmar Seipel 175
Logik für Informatiker Wintersemester 2012/13
2. FallsX in G nicht frei vorkommt:
(QX F ⊗G) ≡ QX (F ⊗G),
für einen QuantorQ ∈ {∀, ∃ } und einen Junktor⊗ ∈ {∧,∨}.
3. Ausklammern von Quantoren:
(∀X F ∧ ∀XG) ≡ ∀X (F ∧G),
(∃X F ∨ ∃XG) ≡ ∃X (F ∨G).
4. Vertauschen gleichartiger Quantoren:
∀X ∀Y F ≡ ∀Y ∀X F,
∃X ∃Y F ≡ ∃Y ∃X F.
Dagegen sind die folgenden Formeln im allgemeinen nicht äquivalent:
(∀XF ∨ ∀XG) 6≡ ∀X (F ∨G),
(∃XF ∧ ∃XG) 6≡ ∃X (F ∧G).
Prof. Dr. Dietmar Seipel 176
Logik für Informatiker Wintersemester 2012/13
Beispiel (Äquivalenz)
1. Nach 1. gilt
¬∀X r(X, Y ) ≡ ∃X ¬ r(X, Y ).
2. DaX undY nicht frei in¬ q(Z) vorkommen, kann man nach 2. die
Quantoren∀X und∃Y sich auf beide Formeln erstrecken lassen:
∀X ∃Y p(X, g(Y, f(X))) ∨ ¬ q(Z)
≡ ∀X ∃Y (p(X, g(Y, f(X))) ∨ ¬ q(Z)).
DaX frei in q(X) vorkommt, kann man den Quantor∀X nicht sich auf
beide Formeln erstrecken lassen:
∀X p(X) ∧ q(X) 6≡ ∀X ( p(X) ∧ q(X) ).
3. Für Konjunktionen kann man nach 3. universelle Quantorenausklammern:
∀X p(X) ∧ ∀X q(X) ≡ ∀X ( p(X) ∧ q(X) ).
Prof. Dr. Dietmar Seipel 177
Logik für Informatiker Wintersemester 2012/13
4. Dagegen kann man unterschiedliche Quantoren im Allgemeinen nicht
vertauschen:
∀X ∃Y F 6≡ ∃Y ∀X F.
FürF = Y > X (Infix–Notation) gilt: wenn man> als die
Größer–Relation auf den natürlichen Zahlen interpretiert, d.h.
UA = IN0 = { 0, 1, 2, . . . },
>A = { (m,n) ∈ IN20 |m > n },
dann erfülltA die Formel∀X ∃Y F , da es für alleX ∈ IN0 eine
größere ZahlY ∈ IN0 gibt, während∃Y ∀X F nicht erfüllt ist,
da es keinY ∈ IN0 gibt, das größer ist als alle ZahlenX ∈ IN0:
A(∀X ∃Y F ) = 1 6= 0 = A(∃Y ∀X F ).
Prof. Dr. Dietmar Seipel 178
Logik für Informatiker Wintersemester 2012/13
Äquivalenz vs. Implikation
1. F ≡ G gilt genau dann,
wennF → G undG→ F gültig (Tautologien) sind.
2. AusF ≡ G folgt, daßF → G undG→ F gültig sind.
Für die nicht geltenden Äquivalenzen
(∀XF ∨ ∀XG) 6≡ ∀X (F ∨G),
(∃XF ∧ ∃XG) 6≡ ∃X (F ∧G).
sind zumindest die folgenden Implikationen gültig:
(∀XF ∨ ∀XG) → ∀X (F ∨G),
(∃XF ∧ ∃XG) ← ∃X (F ∧G).
Prof. Dr. Dietmar Seipel 179
Logik für Informatiker Wintersemester 2012/13
Definition (Ersetzung von Variablen)
1. SeiF eine Formel,X eine Variable undt ein Term. Dann bezeichnet
F [X |t] diejenige Formel, die man ausF erhält, indem man jedes freie
Vorkommen vonX durcht ersetzt.
2. [X |t] wird alsSubstitutionbezeichnet.
3. Eine Folge
θ = [X1|t1] . . . [Xn|tn]
von Substitutionen wird auch als Substitution bezeichnet.
4. Für eine FormelF bezeichnetFθ die Formel
(((F [X1|t1])[X2|t2]) . . . )[Xn|tn],
die man durch sukzessive Anwendung der Substitutionen[Xi|ti] erhält.
Prof. Dr. Dietmar Seipel 180
Logik für Informatiker Wintersemester 2012/13
Beispiel (Substitution)
Seiθ = [X |h(Z)] [Y |U ]. In der folgenden Formel sind die ersten beidenVorkommen vonX gebunden und werden nicht durchh(Z) ersetzt:
(∀X p(X, f(X), g(Y )) ∨ q(X)) θ =
(∀Xp(X, f(X), g(U))∨ q(h(Z))).
Gebundene Umbenennung
Ist F = QX G eine Formel mit einem QuantorQ ∈ {∃, ∀ } undX ′ eineVariable, die inG nicht vorkommt, dann gilt
F = QX G ≡ QX ′ G [X |X ′].
Beispiel (Gebundene Umbenennung)
FürG = p(X, g(Y, f(X))) gilt
∃Y G ≡ ∃Y ′ G [Y |Y ′] = ∃Y ′ p(X, g(Y ′, f(X))).
Prof. Dr. Dietmar Seipel 181
Logik für Informatiker Wintersemester 2012/13
Beispiel (Gebundene Umbenennung)
1. Die folgenden offenen Formeln sind nicht äquivalent:
F = p(X),
G = p(Y ).
Für die StrukturAmit der GrundmengeUA = { 1, 2 } und
pA = { (1) } und der VariablenbelegungXA = 1, Y A = 2 gilt
A(F ) = (1) ∈ pA = 1 6= 0 = (2) ∈ pA = A(G).
2. Die folgenden quantifizierten Formeln sind dagegen äquivalent:
F = ∀X p(X),
G = ∀Y p(Y ).
Es giltG = ∀Y p(X) [X |Y ].
Für gebundene Vorkommen kann man das Variablensymbol umbenennen.
Prof. Dr. Dietmar Seipel 182
Logik für Informatiker Wintersemester 2012/13
Beispiel (Ausklammern nach gebundener Umbenennung)
1. Die folgenden Formeln sind bekanntermaßen im allgemeinen nicht
äquivalent:
(∀XF ∨ ∀XG) 6≡ ∀X (F ∨G),
(∃XF ∧ ∃XG) 6≡ ∃X (F ∧G).
2. SeiF = rot(X) undG = blau(X).
• Dann besagt(∀XF ∨ ∀XG) : entweder alle Kugeln sind rot, oder
alle Kugeln sind blau.
• Dagegen besagt∀X (F ∨G), daß jede Kugel entweder rot oder
blau ist. Aber es kann sowohl rote als auch blaue Kugeln geben.
In den folgenden Strukturen mit einfarbigen Kugeln unterscheiden sich
auch die Formeln mit der existentiellen Quantifizierung.
Prof. Dr. Dietmar Seipel 183
Logik für Informatiker Wintersemester 2012/13
F1 = (∀Xrot(X) ∨ ∀Xblau(X)) 6≡ F2 = ∀X (rot(X) ∨ blau(X)),
G1 = (∃Xrot(X) ∧ ∃Xblau(X)) 6≡ G2 = ∃X (rot(X) ∧ blau(X)).
Die folgenden StrukturenAi mit einfarbigen Kugeln erfüllenG2 nicht,
da es keine Kugeln gibt, die gleichzeitig rot und blau sind.
A1 A2 A3
A1 erfüllt F2 undG1, aber nichtF1 undG2, denn jede Kugel ist
entweder rot oder blau (mit Punkt in der Mitte), und es gibt rote und
blaue Kugeln.
A2 undA3 erfüllenF1 undF2, aber nichtG1 undG2, denn in beiden
Strukturen haben alle Kugeln dieselbe Farbe, rot bzw. blau.
Prof. Dr. Dietmar Seipel 184
Logik für Informatiker Wintersemester 2012/13
3. Für ein frisches VariablensymbolX ′, das nicht in(∀XF ∨ ∀XG)
vorkommt, gilt:
(∀XF ∨ ∀XG) ≡ (∀X ′F [X |X ′] ∨ ∀XG)
≡ ∀X ′ (F [X |X ′] ∨ ∀XG) ≡ ∀X ′ ∀X (F [X |X ′] ∨ G).
Also gilt z.B.
(∀X rot(X) ∨ ∀X blau(X)) ≡ ∀X ′ ∀X (rot(X ′) ∨ blau(X)).
Prinzipiell können Kugeln mehrfarbig sein. Wenn es aber eine rote
Kugel r gäbe, die nicht auch blau ist, und eine blaue Kugelb, die nicht
auch rot ist, dann wäreA[X′|b][X|r](rot(X′) ∨ blau(X)) = 0.
4. Für ein frisches VariablensymbolX ′, das nicht in(∃XF ∧ ∃XG)
vorkommt, gilt analog auch:
(∃XF ∧ ∃XG) ≡ ∃X ′ ∃X (F [X |X ′] ∧ G).
Prof. Dr. Dietmar Seipel 185
Logik für Informatiker Wintersemester 2012/13
5. Auch aus einer Implikation kann man nach gebundener Umbenennung
ausklammern:
F = ∀X ( p(X )→ ∃X q(X) )
≡ ∀X ( p(X )→ ∃X ′ q(X ′) )
≡ ∀X ∃X ′ ( p(X )→ q(X ′) ).
Hier mußteX gebunden inX ′ umbenannt werden, da das Vorkommen
vonX in p(X) durch∀X und das Vorkommen vonX in q(X) durch
∃X gebunden waren.
Nach dem Vorziehen des Quantors∃X ′ erstrecken sich nun beide
Quantoren aufp(X )→ q(X ′), also auf beide Teilformeln.
Prof. Dr. Dietmar Seipel 186
Logik für Informatiker Wintersemester 2012/13
Definition (BPF, bereinigte Pränexform)
1. Eine FormelF heißtbereinigt,
• wenn es keine VariableX gibt, die inF sowohl gebunden als auch
frei vorkommt, und
• wenn hinter allen vorkommenden Quantoren verschiedene
Variablen stehen.
2. Eine FormelF heißt Pränex oder in Pränexform, falls sie von der Form
Q1X1 Q2X2 . . . QnXn G
ist, mit QuantorenQi ∈ {∃, ∀ } und VariablenXi, und falls fernerG
quantorenfrei ist.
Satz (BPF)
Für jede FormelF gibt es eine äquivalente FormelG in BPF.
Prof. Dr. Dietmar Seipel 187
Logik für Informatiker Wintersemester 2012/13
∀X ∃Y p(X, g(Y, f(X))) ¬q(Z)
∨ ¬∀X r(X,Y )
∨
Beispiel (BPF)
Aus
¬∀X r(X, Y )
≡ ∃X ′ ¬ r(X ′, Y ),
∀X ∃Y p(X, g(Y, f(X))) ∨ ¬ q(Z)
≡ ∀X ∃Y ′ (p(X, g(Y ′, f(X))) ∨ ¬ q(Z)),
folgt:
F = (∀X ∃Y p(X, g(Y, f(X))) ∨ ¬ q(Z)) ∨ ¬∀X r(X, Y )
≡ ∀X ∃Y ′ ∃X ′ ( p(X, g(Y ′, f(X))) ∨ ¬ q(Z) ∨ ¬ r(X ′, Y ) ).
Die Quantoren∀X und∃Y beziehen sich nicht auf¬∀X r(X, Y ).
Deswegen benennen wirY vorne inY ′ gebunden um undX hinten inX ′.
Danach können alle Quantoren ganz nach vorne gezogen werden.
Prof. Dr. Dietmar Seipel 188
Logik für Informatiker Wintersemester 2012/13
Die enstandene Formel in BPF hat immer noch 2 freie VorkommenvonVariablensymbolen, nämlichY undZ.
p(X, g(Y ′, f(X))) ¬q(Z)
∨ ¬ r(X ′, Y )
∨
∀X ∃Y ′ ∃X ′
Die gebundenen Umbenennungen waren erforderlich,
• daX einmal universell und einmal existentiell quantifiziert ist, und
• da sich der Quantor∃Y ′ nicht auf¬ r(X ′, Y ) beziehen soll.
Prof. Dr. Dietmar Seipel 189
Logik für Informatiker Wintersemester 2012/13
Beispiel (BPF)
In der folgenden BPF–FormelF kommt das universell quantifizierte
VariablensymbolY nur im Regelrumpf vonr vor:
F = ∀X ∀Y ∀Z r,
r = father(X ,Y ) ∧ brother(Y ,Z )→ uncle(X ,Z ).
Dann könnte man den vorr stehenden Allquantor∀Y auch als
Existenzquantor∃Y in den Regelrumpf vonr ziehen:
∀Y r ≡ ∀Y (¬ (father(X ,Y ) ∧ brother(Y ,Z )) ∨ uncle(X ,Z ))
≡ ∀Y ¬ (father(X ,Y ) ∧ brother(Y ,Z )) ∨ uncle(X ,Z )
≡ ¬ ∃Y (father(X ,Y ) ∧ brother(Y ,Z )) ∨ uncle(X ,Z )
≡ ∃Y (father(X ,Y ) ∧ brother(Y ,Z ))→ uncle(X ,Z ).
Prof. Dr. Dietmar Seipel 190
Logik für Informatiker Wintersemester 2012/13
Exkurs: Existenzquantor im Regelkopf
Ein Existenzquantor∃Y im Kopf einer BPF–Regel,
F = ∀X ( kugel(X )→ ∃Y farbe(X ,Y ) ),
entspricht dagegen einem vor der Regel stehenden Existenzquantor∃Y :
F ≡ ∀X ∃Y ( kugel(X )→ farbe(X ,Y ) ).
Für eine vorgegebene StrukturA ergibt er eine Disjunktion im Regelkopf:
A(F ) = ∧u∈UA( (u) ∈ kugelA → ∨v∈UA
(u, v) ∈ farbeA ).
Da die GrundmengeU = UA für Herbrand–Strukturen unabhängig vonA
ist, könnte manF praktisch wie eine Regel mit einem disjunktiven Kopf
auffassen:
F = ∀X ( kugel(X )→ ∨v∈U farbe(X , v) ).
Prof. Dr. Dietmar Seipel 191
Logik für Informatiker Wintersemester 2012/13
In der Praxis möchte man allerdings fürv ∈ U nur Farben zulassen, etwa
rot , grun, blau. Dann meint man eigentlich die folgende Formel:
F = ∀X
( kugel(X ) →
farbe(X , rot) ∨ farbe(X , grun) ∨ farbe(X , blau) ).
Diese könnte man wieder mit einem Existenzquantor∃Y im Regelkopf
ausdrücken,
G = ∀X ( kugel(X )→ ∃Y (farbe(Y ) ∧ farbe(X ,Y )) ).
Man könnte dazu ein1–stelliges Prädikatfarbe, das die zugelassenen
Farben angibt, mit Hilfe geeigneter Formeln definieren.
Prof. Dr. Dietmar Seipel 192
Logik für Informatiker Wintersemester 2012/13
Definition (Skolemform)
Zu einer FormelF in BPF erhält man die Skolemform durch Eliminationder Existenzquantoren nach folgendem Schema:
1. Wir betrachten den ersten Existenzquantor inF :
F = ∀X1 ∀X2 . . .∀Xn ∃X G.
2. Seif ein neues bisher inF nicht vorkommendesn–stelligesFunktionssymbol. Dann setzen wir
F ′ = ∀X1 ∀X2 . . .∀Xn G [X |f(X1, . . . , Xn)].
Nun eliminieren wir nach demselben Schema alle weiterenExistenzquantoren inF ′.
3. Sobald die so erhaltene FormelF ′′ keine Existenzquantoren mehrenthält, ist sie inSkolemform:
F ′′ = ∀X1∀X2 . . .∀Xk F∗
mit quantorenfreier FormelF ∗, die wir Matrix nennen.
Prof. Dr. Dietmar Seipel 193
Logik für Informatiker Wintersemester 2012/13
Beispiel (Skolemform)
Wir betrachten die folgende FormelF in BPF:
F = ∃X ∀Y ∃Z ∀V ∃W ¬p(X, Y, Z, V,W )
F ′ = ∀Y ∃Z ∀V ∃W ¬p(a, Y, Z, V,W )
F ′′ = ∀Y ∀V ∃W ¬p(a, Y, f(Y ), V,W )
F ′′′ = ∀Y ∀V ¬p(a, Y, f(Y ), V, g(Y, V )).
Wir ersetzen die existentiell quantifizierten Variablen durch Terme:
• Zuerst ersetzen wirX durch eine frische Konstantea.
• Dann ersetzen wirZ im Scope vonY durch einen Termf(Y ).
• Schließlich ersetzen wirW im Scope vonY undV durch einen Term
g(Y, V ).
Prof. Dr. Dietmar Seipel 194
Logik für Informatiker Wintersemester 2012/13
Beispiel (Skolemform)
Das3–stellige Prädikatensymbolp steht für eine Gruppenoperation;
wir schreibenp(X, Y, Z) anstelle vonX ◦ Y = Z (Produkt).
Die folgende Formel beschreibt die Gruppenaxiome zur Existenz eines
links–neutralen Elements (X) und zur Existenz von Links–Inversen (Z):
F = ∃X ( ∀Y p(X, Y, Y ) ∧ ∀Y ∃Z p(Z, Y,X) ).
Wir bringenF zuerst in BPF, und dann mittels zweier Skolemfunktionene
(0–stellig) undi (1–stellig) in SkolemformF ′:
F ≡ ∃X ∀Y ∃Z ( p(X, Y, Y ) ∧ p(Z, Y,X) ),
F ′ = ∀Y ( p(e, Y, Y ) ∧ p(i(Y ), Y, e) ).
Bei der Erzeugung der BPF wurde der bekannte Satz zur Verschiebung der
Quantoren∀Y und∃Z angewendet.
Prof. Dr. Dietmar Seipel 195
Logik für Informatiker Wintersemester 2012/13
Definition (Erfüllbarkeitsäquivalenz)
Zwei prädikatenlogische FormelnF undG heißenerfüllbarkeitsäquivalent,
wenn gilt:F ist genau dann erfüllbar, wennG erfüllbar ist.
F undG müssen nicht dieselben Modelle haben.
Die Erfüllbarkeitsäquivalenz bedeutet aber, daßF undG entweder beide
ein Modell besitzen, oder daß keine der beiden Formeln ein Modell besitzt.
Beispiel (Erfüllbarkeitsäquivalenz)
Indem man die freie VariableX in
G = ∀Y p(X, Y, Y ) ∧ ∀Y ∃Z p(Z, Y,X)
existentiell quantifiziert, erhält man eine erfüllbarkeitsäquivalente Formel
F = ∃X ( ∀Y p(X, Y, Y ) ∧ ∀Y ∃Z p(Z, Y,X) ).
Prof. Dr. Dietmar Seipel 196
Logik für Informatiker Wintersemester 2012/13
Satz (Skolemform)
Eine FormelF in BPF ist genau dann erfüllbar, wenn ihre Skolemform
erfüllbar ist.
Beweis:
Wir betrachten den EliminationsschrittF 7→ F ′ für den ersten
Existenzquantor:
F = ∀X1 ∀X2 . . .∀Xn ∃X G.
1. Annahme:F ′ ist erfüllbar mit einer passenden StrukturA′, d.h.
A′(F ′) = 1. Dann paßtA′ auch zuF und es gilt
∀u1, . . . , un ∈ UA′ :
A′[X1|u1]...[Xn|un]
(G[X |f(X1, . . . , Xn)]) = 1.
Prof. Dr. Dietmar Seipel 197
Logik für Informatiker Wintersemester 2012/13
Daraus folgt
∀u1, . . . , un ∈ UA′ :
A′[X1|u1]...[Xn|un][X|fA′(u1,... ,un)]
(G) = 1.
Daraus folgt
∀u1, . . . , un ∈ UA′ : ∃u = fA′
(u1, . . . , un) ∈ UA′ :
A′[X1|u1]...[Xn|un][X|u](G) = 1.
Daraus folgt
A′(∀X1 . . . ∀Xn ∃X G) = 1.
Also istA′ auch ein Modell fürF .
Prof. Dr. Dietmar Seipel 198
Logik für Informatiker Wintersemester 2012/13
2. Annahme:F ist erfüllbar mit einer passenden StrukturA,
d.h.A(F ) = 1.
Wir können annehmen, daßIA auf keinen anderen als den inF
vorkommenden Funktionssymbolen, Prädikatensymbolen undfreien
Variablen definiert ist.
Dann gilt:
∀u1, . . . , un ∈ UA : ∃u ∈ UA :
A[X1|u1]...[Xn|un][X|u](G) = 1.
Wir erweitern nun die StrukturA zu einer neuen StrukturA′ durch
Definition einer FunktionfA′
mit
fA′
(u1, . . . , un) = u
durch Verwendung desAuswahlaxioms. Es gilt UA′ = UA.
Prof. Dr. Dietmar Seipel 199
Logik für Informatiker Wintersemester 2012/13
Daraus folgt
∀u1, . . . , un ∈ UA′ :
A′[X1|u1]...[Xn|un][X|fA′(u1,... ,un)]
(G) = 1.
Daraus folgt
∀u1, . . . , un ∈ UA′ :
A′[X1|u1]...[Xn|un]
(G[X |f(X1, . . . , Xn)]) = 1.
Daraus folgt
A′(∀X1 . . . ∀Xn G[X |f(X1, . . . , Xn)]) = 1.
Also istA’ ein Modell fürF .
Prof. Dr. Dietmar Seipel 200
Logik für Informatiker Wintersemester 2012/13
Zusammenfassung (BPF, Skolemform)
1. Für jede FormelF gibt es eine äquivalente FormelG in BPF.
2. F undG haben genau dieselben Modelle.
3. Für jede FormelF gibt es eine FormelH in Skolemform.
• F undH müssen nicht dieselben Modelle haben.
• Insbesondere unterscheiden sich die Modelle in der Regel aufgrund
der Skolemfunktionen inH.
• Die SkolemformH wird durch Elimination der Existenzquantoren
aus der BPFG konstruiert.
4. Eine FormelF ist genau dann erfüllbar, wenn ihre SkolemformH
erfüllbar ist.
Prof. Dr. Dietmar Seipel 201
Logik für Informatiker Wintersemester 2012/13
Klauselform
Aus einer FormelF kann man über die Skolemform eine KlauselmengeM
gewinnen. Eine Klausel ist eine Disjunktion prädikatenlogischer Literale.
1. Durch systematisches Umbenennen der gebundenen Variablen inF
bilden wir eine neue, bereinigte FormelF1, die zuF äquivalent ist.
2. SeienY1, . . . , Yn die inF1 vorkommenden freien Variablen.
Dann enthältF2 = ∃Y1 . . .∃Yn F1 keine ungebundenen Variablen
mehr, undF2 ist erfüllbarkeitsäquivalent zuF1.
3. SeiF3 = ∀X1 . . .∀XmG3 eine Skolemform zuF2 mit der
(quantorenfreien) MatrixG3. Dann sind alle Variablen inF3 universell
quantifiziert, undF3 ist erfüllbarkeitsäquivalent zuF2.
4. Man kann die MatrixG3 in eine KNFG4 = ∧ki=1 βi mit Klauselnβi
umformen. Dann istF4 = ∀X1 . . .∀Xm G4 zuF3 äquivalent.
Prof. Dr. Dietmar Seipel 202
Logik für Informatiker Wintersemester 2012/13
Insgesamt gilt:
• F4 ist erfüllbarkeitsäquivalent zuF , und
• alle Variablen inF4 sind universell quantifiziert.
Die KlauselmengeM = {β1, . . . , βk } spielt später bei Inferenzmethoden
eine entscheidente Rolle. Man kann mittels der Resolutionsmethode genau
dann die leere Klausel ausM ableiten, wennF unerfüllbar ist.
Beispiel (Klauselmenge)
Die Formel
G = ∀Y p(X, Y, Y ) ∧ ∀Y ∃Z p(Z, Y,X)
wird zur Klauselmenge
M = { p(e, Y, Y ), p(i(Y ), Y, e) }.
Prof. Dr. Dietmar Seipel 203
Logik für Informatiker Wintersemester 2012/13
2.3 Unentscheidbarkeit
Es gibt prädikatenlogische FormelnF , die zwar erfüllbar sind, jedoch nurunendliche ModelleA = (UA, IA) besitzen, also solche mit unendlicherGrundmengeUA:
F = ∀X p(X, f(X)) ∧
∀Y ¬p(Y, Y ) ∧
∀U ∀V ∀W ( (p(U, V ) ∧ p(V,W ))→ p(U,W ) )
Dann gibt es das folgende unendliche ModellA = (UA, IA) :
UA = IN0 = { 0, 1, 2, . . . },
pA = { (m,n) ∈ IN20 |m < n },
fA(n) = n+ 1.
Die FormelF besitzt jedoch kein endliches Modell.
Prof. Dr. Dietmar Seipel 204
Logik für Informatiker Wintersemester 2012/13
AngenommenB = (UB, IB) ist ein Modell mit endlicher GrundmengeUB.
Für ein beliebiges Elementm0 ∈ UB betrachten wir die Folge
m0,m1,m2, . . . ∈ UB, mit mi+1 = fB(mi).
Wegen des ersten Konjunktionsgliedes vonF gilt
(m0,m1), (m1,m2), . . . , (mi,mi+1) ∈ pB, für alle i ∈ IN0.
Wegen des dritten Konjunktionsgliedes vonF ist pB transitiv, d.h.
(mi,mj) ∈ pB, für alle i, j ∈ IN0 mit i < j.
DaUB endlich ist, muß es zwei Indizesi undj mit i < j geben, mit
mi = mj = m.
Also gibt es(m,m) ∈ pB, im Widerspruch zum zweiten Konjunktionsglied
vonF (Irreflexivität).
Prof. Dr. Dietmar Seipel 205
Logik für Informatiker Wintersemester 2012/13
Obiges Beispiel zeigt, daß sich die Wahrheitstafelmethodenicht in die
Prädikatenlogik übertragen läßt.
Entscheidbarkeit
Ein (ja/nein–) Problem heißtentscheidbaroderrekursiv, falls es ein
Rechenverfahren gibt (z.B. formuliert als Programm in C++), das für alle
Eingaben immer nach endlicher Zeit stoppt, und dann korrekt“ja” oder
“nein” ausgibt.
Anderenfalls heißt ein Problemunentscheidbar.
Gültigkeitsproblemder Prädikatenlogik:
Gegeben eine prädikatenlogische FormelF .
Frage: IstF eine gültige Formel ?
Prof. Dr. Dietmar Seipel 206
Logik für Informatiker Wintersemester 2012/13
Satz (Church)
Das Gültigkeitsproblem der Prädikatenlogik ist unentscheidbar.
Beweis durch Zurückführung auf das unentscheidbarePostsche
Korrespondenzproblem:
• Gegeben eine endliche Folge(x1, y1), . . . , (xn, yn) von Paaren
xi, yi ∈ {0, 1}+ von nicht–leeren Strings über{0, 1}.
• Frage: Gibt es eine Folge von Indizesi1, . . . , im ∈ { 1, . . . , n }, mit
m ≥ 1, so daß die Konkatenationen der entsprechenden Strings
übereinstimmen ?
xi1xi2 . . . xim = yi1yi2 . . . yim .
Prof. Dr. Dietmar Seipel 207
Logik für Informatiker Wintersemester 2012/13
Beispiel (Postsches Korrespondenzproblem)
SeiK = ((x1, y1), (x2, y2), (x3, y3)) mit
x1 = 1 und y1 = 101,x2 = 10 und y2 = 00,x3 = 011 und y3 = 11.
Lösung:i1 = 1, i2 = 3, i3 = 2, i4 = 3
x1 x3 x2 x3 =
x1︷︸︸︷
1
x3︷ ︸︸ ︷
0 1 1
x2︷︸︸︷
1 0
x3︷ ︸︸ ︷
0 1 1 = y1 y3 y2 y3.︸ ︷︷ ︸
y1
︸︷︷︸
y3
︸︷︷︸
y2
︸︷︷︸
y3
Folgerung (Erfüllbarkeitsproblem)
DasErfüllbarkeitsproblemder Prädikatenlogik
Ist eine gegebene prädikatenlogische FormelF erfüllbar ?
ist ebenfalls unentscheidbar.
Prof. Dr. Dietmar Seipel 208
Logik für Informatiker Wintersemester 2012/13
2.4 Herbrand–Theorie
Jacques Herbrand, Kurt Gödel, Thoralf Skolem
Definition (Herbrand–Universum)
Das Herbrand–UniversumHUF einer FormelF ist die Menge aller
variablenfreien Terme, die aus Bestandteilen vonF gebildet werden
können.
FallsF keine Konstante (d.h., kein0–stelliges Funktionssymbol) enthält,
so nehmen wir eine beliebige Konstantea und zur Konstruktion vonHUF
hinzu.
Das Herbrand–UniversumHUF ist meist unendlich groß, aber man kann es
systematisch konstruieren.
Prof. Dr. Dietmar Seipel 209
Logik für Informatiker Wintersemester 2012/13
Induktive Konstruktion:
1. Alle in F vorkommenden Konstanten sind inHUF .
2. FallsF keine Konstanten enthält, so nimmt man eine beliebige
Konstantea zuHUF hinzu.
3. Für jedes inF vorkommende
• n–stellige Funktionssymbolf und
• Termet1, . . . , tn ∈ HUF
ist auch der Termf(t1, . . . , tn) in HUF .
Für ein1–stelliges Funktionssymbolf und eine Konstantea setzen wir
• f0(a) = a und
• fk+1(a) = f(fk(a)), für allek ∈ IN0.
Z.B. entstehtf2(a) = f(f(a)) durch2–malige Anwendung vonf aufa.
Prof. Dr. Dietmar Seipel 210
Logik für Informatiker Wintersemester 2012/13
Beispiel (Herbrand–Universum)
Die FormelF = p(f(a), g(b)) enthält zwei Konstanten (0–stellige
Funktionssymbole)a undb und zwei einstellige Funktionssymbolef undg.
Daraus setzen sich die Terme des Herbrand–Universums zusammen.
1. a undb sind inHUF . DaF bereits Konstanten enthält, ist keine
zusätzliche Konstante erforderlich.
2. Mit den Funktionssymbolenf undg kann man weitere Terme bilden.
Die Tatsache, daßa in F nur als Argument vonf vorkommt undb nur
als Argument vong ist dabei unerheblich. Auch die “gekreuzten”
Termef(b) undg(a) sind inHUF .
3. Fallsh1, . . . , hn eine beliebige Folge von Funktionssymbolen ist, mit
hi ∈ {f, g}, so sind auchh1(. . . (hn(a))) undh1(. . . (hn(b))) in HUF .
4. HUF = { a, b, f(a), f(b), g(a), g(b), f(f(a)), f(g(a)), . . . }.
Prof. Dr. Dietmar Seipel 211
Logik für Informatiker Wintersemester 2012/13
HUF ist genau dann unendlich groß, wennF einn–stelliges
Funktionssymbol mitn ≥ 1 enthält.
Für ein1–stelliges Funktionssymbolf in F und eine Konstantea ∈ HUF
sind z.B. auch alle Termefk(a) in HUF .
Beispiel (Herbrand–Universum)
Die FormelF in BPF enthält ein einstelliges Funktionssymbolf :
F = ∃X p(f(X)),
HUF = { a, f(a), f(f(a)), . . . } = { fk(a) | k ∈ IN0 }.
DaF keine Konstanten enthält, nehmen wir die Konstantea zuHUF hinzu.
Dasselbe Herbrand–Universum würden wir auch für die variablenfreie
Formel F ′ = p(f(a)) erhalten.
Prof. Dr. Dietmar Seipel 212
Logik für Informatiker Wintersemester 2012/13
Man kann das Herbrand–UniversumHUF wie folgt systematisch als
unendliche Vereinigung endlicher Mengen konstruieren:
1. HU1 sei die Menge aller inF vorkommenden Konstanten,
bzw.HU1 = { a }, fallsF keine Konstanten enthält.
2. HU ′k+1 sei die Menge aller Termef(t1, . . . , tn) aus einem inF
vorkommendenn–stelligen Funktionssymbolf und Termen
t1, . . . , tn ∈ HUk, undHUk+1 = HUk ∪HU ′k+1.
3. Dann sind alle MengenHUk endlich, die Folge(HUk)k∈IN+ ist
aufsteigend, undHUF = ∪∞k=1 HUk.
Also ist das Herbrand–UniversumHUF abzählbar. Man erhält per
Induktion eine injektive AbbildungHUF → IN, indem man sukzessive die
endlichen MengenHUk+1 \ HUk fortlaufend durchnummeriert.
Prof. Dr. Dietmar Seipel 213
Logik für Informatiker Wintersemester 2012/13
Beispiel (Herbrand–Universum)
Die folgende FormelF enthält vier Funktionssymbole:
F = ∀X ∀Y p(a, f(X), g(Y, b)).
a undb sind0–stellig, und somit Konstanten.f ist 1–stellig,g ist 2–stellig.
HU1 = { a, b },
HU2 = HU1 ∪ { f(a), f(b), g(a, a), g(a, b), g(b, a), g(b, b) },
HUk+1 = HUk ∪ { f(t) | t ∈ HUk } ∪ { g(t1, t2) | t1, t2 ∈ HUk }.
Sobald eine FormelF mindestens einn–stelliges Funktionssymbolf ,
mit n ≥ 1, enthält, ist das Herbrand–UniversumHUF unendlich groß:
HUF enthält immer eine Konstante, und man kann aus jedem Term
t ∈ HUk+1 \HUk einen neuen Termf(t, . . . , t) ∈ HUk+2 \HUk+1 bilden.
Prof. Dr. Dietmar Seipel 214
Logik für Informatiker Wintersemester 2012/13
Definition (Herbrand–Strukturen)
SeiF eine Formel undA = (UA, IA) eine zuF passende Struktur.
Dann heißtA eine Herbrand–Struktur fürF , falls gilt:
1. Die Grundmenge vonA ist UA = HUF .
2. Für alle Termef(t1, . . . , tn) ∈ HUF :
A(f(t1, . . . , tn)) = fA(A(t1), . . . ,A(tn)) = f(t1, . . . , tn).
Terme werden also von Herbrand–Strukturen durch sich selbst interpretiert.
Herbrand–Strukturen für geschlossene Formeln sind vollständig durch dieInterpretationpA der Prädikatensymbole charakterisiert.Man nennt die entsprechende MengeI eine Herbrand–Interpretation:
I = { p(t1, . . . , tn) | t1, . . . , tn ∈ HUF ∧ (t1, . . . , tn) ∈ pA }
Eine Herbrand–Struktur, welche ein Modell für eine FormelF ist, heißtHerbrand–Modellfür F .
Prof. Dr. Dietmar Seipel 215
Logik für Informatiker Wintersemester 2012/13
Beispiel (3–Färbbarkeit)
Gesucht ist eine Färbung der Knoten eines GraphenG = 〈V,E 〉 mit drei
Farben (rot, grün, blau), so daß adjazente Knoten unterschiedliche Farben
haben:
a
b
c
d e
Wir repräsentieren die Knoten und Kanten des Graphen als Fakten:
f1 = node(a), f2 = node(b), . . . , f5 = node(e),
e1 = edge(a, b), e2 = edge(a, c), . . . , e6 = edge(d , e).
Prof. Dr. Dietmar Seipel 216
Logik für Informatiker Wintersemester 2012/13
g = color(X , red) ∨ color(X , green) ∨ color(X , blue)← node(X ),
c0 = ← edge(X ,Y ) ∧ color(X ,C ) ∧ color(Y ,C ),
c1 = ← color(X , red) ∧ color(X , green),
c2 = ← color(X , red) ∧ color(X , blue),
c3 = ← color(X , green) ∧ color(X , blue).
Die disjunktive Regelg wählt für jeden Knoten eine Farbe aus.
Die Integritätsbedingungc0 verhindert, daß adjazente Knoten die gleiche
Farbe bekommen. Die Integritätsbedingungenc1, c2, c3 verhindern, daß ein
Knoten zwei Farben bekommt.
Nebenbemerkung: Jeder planare Graph ist 4–färbbar.
Für allgemeine Graphen ist der Test auf 3–FärbbarkeitNP–vollständig.
Prof. Dr. Dietmar Seipel 217
Logik für Informatiker Wintersemester 2012/13
Wir betrachten dann die Formel
F = f1 ∧ . . . ∧ f5 ∧ e1 ∧ . . . ∧ e6 ∧
∀Xg ∧
∀X∀Y ∀C c0 ∧
∀Xc1 ∧ . . . ∧ ∀Xc3.
F ist äquivalent zur folgenden FormelF ′ in Skolemform:
F ′ = ∀X ∀Y ∀C
(f1 ∧ . . . ∧ f5 ∧ e1 ∧ . . . ∧ e6 ∧ g ∧ c0 ∧ . . . ∧ c3).
Das Herbrand–Universum ist
HUF = { a, b, c, d, e, red , green, blue }.
Prof. Dr. Dietmar Seipel 218
Logik für Informatiker Wintersemester 2012/13
a
b
c
d e
Die folgende Herbrand–InterpretationI repräsentiert ein Herbrand–Modell
für die FormelF :
I = { node(a), . . . , node(e), edge(a, b), . . . , edge(d , e),
color(a, red), color(b, green), color(c, blue),
color(d , red), color(e, green) }.
Prof. Dr. Dietmar Seipel 219
Logik für Informatiker Wintersemester 2012/13
Die zugehörigen InterpretationenpA der Prädikatensymbole sind folgende:
nodeA = { (a), . . . , (e) },
edgeA = { (a, b), . . . , (d, e) },
colorA = { (a, red), (b, green), (c, blue),
(d, red), (e, green) }.
Die Herbrand–InterpretationI faßt diese MengenpA zu einer einzigenMenge zusammen.
Damit man die Tupel(t1, . . . , tn) ∈ pA korrekt zuordnen kann, werden sie
in I als Atomep(t1, . . . , tn) mit Prädikatensymbol notiert:
I = { p(t1, . . . , tn) | t1, . . . , tn ∈ HUF ∧ (t1, . . . , tn) ∈ pA }.
Würde man einfach die Vereinigung der MengenpA benutzen, so könnteman z.B. nicht wissen, ob ein Paar(t1, t2) zu edgeA oder zucolorA gehört.
Prof. Dr. Dietmar Seipel 220
Logik für Informatiker Wintersemester 2012/13
Satz (Herbrand–Modell)
Eine AussageF in Skolemformist genau dann erfüllbar,
wennF ein Herbrand–Modell besitzt.
Beweis:
1. ⇐: Klar.
2. ⇒: SeiA = (UA, IA) ein beliebiges Modell fürF .
FallsF keine Konstanten enthält unda als zusätzliche Konstante
gewählt wurde, so setzen wiraA = a′, für ein beliebiges Element
a′ ∈ UA.A ist danach immer noch ein Modell fürF .
Wir konstruieren nun ausA eine Herbrand–StrukturB = (UB, IB)
für F , d.h. mit der GrundmengeUB = HUF .
Dazu müssen wir die Prädikatensymbolep ausF interpretieren.
Prof. Dr. Dietmar Seipel 221
Logik für Informatiker Wintersemester 2012/13
Seip einn–stelliges Prädikatensymbol, und seient1, . . . , tn ∈ HUF :
(t1, . . . , tn) ∈ pB g.d.w.(A(t1), . . . ,A(tn)) ∈ pA
Wir zeigen nun, daßB ein Modell fürF ist. Mehr noch:
Für jede AussageG in Skolemform, die aus den Bestandteilen vonF
aufgebaut ist, gilt:
A |= G ⇒ B |= G.
Wir führen eine Induktion über die Anzahln der Allquantoren vonG.
n = 0: G enthält keine Quantoren.
Dann haben alle Atome vonG unterA undB denselben Wahrheitswert,
und deshalb giltA(G) = B(G).
n→ n+ 1: SeiG eine Formel mitn+ 1 Allquantoren, und zwar von der
FormG = ∀X H, wobeiH nurn Allquantoren enthält.
Prof. Dr. Dietmar Seipel 222
Logik für Informatiker Wintersemester 2012/13
WegenA |= G gilt:
∀u ∈ UA : A[X|u](H) = 1.
Insbesondere gilt für alleu = A(t) ∈ UA mit t ∈ HUG:
A[X|A(t)](H) = 1.
Deshalb gilt:
∀ t ∈ HUG : A(H[X |t]) = A[X|A(t)](H) = 1.
Nach Induktionsvoraussetzung gilt nun:
∀ t ∈ HUG : B(H[X |t]) = 1.
Deshalb gilt:
∀ t ∈ HUG : B[X|B(t)](H) = B(H[X |t]) = 1.
Also gilt B(G) = B(∀XH) = 1.
Prof. Dr. Dietmar Seipel 223
Logik für Informatiker Wintersemester 2012/13
Der obige Satz über Herbrand–Modelle wäre falsch, wenn wir nicht eine
frische Konstantea zuHUF hinzunehmen würden, fallsF keine
Konstanten enthält – denn dann wäre die GrundmengeHUF = ∅.
Beispiel (Herbrand–Modell)
Für die Formel
F = ∃X p(X)
ist das Herbrand–UniversumHUF = { a }, und das einzige
Herbrand–ModellA ist gegeben durch
pA = { (a) }.
Ohne die frische Konstantea könnte man kein Herbrand–Modell bilden, da
F fordert, daßpA mindestens ein Tupel(t), mit t ∈ HUF , enthalten muß.
Prof. Dr. Dietmar Seipel 224
Logik für Informatiker Wintersemester 2012/13
Satz (Löwenheim und Skolem)
Jede erfüllbare FormelF der Prädikatenlogik besitzt ein abzählbares
ModellB = (UB, IB), d.h. mit einer abzählbaren GrundmengeUB.
Man kann fürB ein Herbrand–Modellder Skolemform vonF wählen.
Definition (Herbrand–Expansion)
Sei
F = ∀X1∀X2 . . .∀Xn G
eine Formel in Skolemform mit der (quantorenfreien) MatrixG.
Dann ist die Herbrand–Expansion vonF definiert als
E(F ) = {G[X1|t1] . . . [Xn|tn] | t1, . . . , tn ∈ HUF }.
Prof. Dr. Dietmar Seipel 225
Logik für Informatiker Wintersemester 2012/13
Beispiel (Herbrand–Expansion)
Für die folgende FormelF in Skolemform
F = ∀X (f ∧ r),
f = married(a, b),
r = student(X )→ person(X ),
ist HUF = { a, b }, und die Herbrand–Expansion
E(F ) = {married(a, b) ∧ (student(a)→ person(a)),
married(a, b) ∧ (student(b)→ person(b)) }
hat2 Elemente, da man das VariablensymbolX mit den zwei Konstanten
ausHUF belegen kann.
Prof. Dr. Dietmar Seipel 226
Logik für Informatiker Wintersemester 2012/13
Beispiel (Herbrand–Expansion)
Für die FormelF = ∀X1∀X2∀X3G, mit G = F1∧F2∧F3∧F4 ∧F5 und
F1 = ancestor(X1, X2)← parent(X1, X2),
F1 = ancestor(X1, X2)← parent(X1, X3) ∧ ancestor(X3, X2),
F3 = parent(a, b),
F4 = parent(b, c),
F5 = parent(c, d),
git HUF = { a, b, c, d }, undE(F ) hat43 = 64 Elemente. Eines davon ist
z.B.Gθ = F1θ ∧ F2θ ∧ F3 ∧ F4 ∧ F5, für θ = [X1|a] [X2|c] [X3|b]:
F1θ = ancestor(a, c)← parent(a, c),
F2θ = ancestor(a, c)← parent(a, b) ∧ ancestor(b, c).
Prof. Dr. Dietmar Seipel 227
Logik für Informatiker Wintersemester 2012/13
FallsF Variablensymbole und Funktionssymbole der Stelligkeitn ≥ 1
enthält, so sindHUF undE(F ) unendlich groß.
Beispiel (Herbrand–Expansion)
Für die Formel
F = ∀X1∀X2 p(X1, f(X2), g(X1, X2))
in Skolemform erhalten wir die folgende Herbrand–Expansion:
HUF = { a, f(a), g(a, a), f(f(a)), f(g(a, a)),
g(a, f(a)), g(a, g(a, a)),
g(f(a), a), g(f(a), f(a)), g(f(a), g(a, a)),
g(g(a, a), a), g(g(a, a), f(a)), g(g(a, a), g(a, a)), . . . },
E(F ) = { p(t1, f(t2), g(t1, t2)) | t1, t2 ∈ HUF }.
DaF keine Konstante enthält, wurdea zuHUF hinzugenommen.
Prof. Dr. Dietmar Seipel 228
Logik für Informatiker Wintersemester 2012/13
Im Grunde genommen kannE(F ) als eine – meist unendliche –
aussagenlogische Formelmenge angesehen werden, wenn man die in E(F )
vorkommenden Grundatome als atomare Formeln der Aussagenlogik
auffaßt.
Satz (Gödel, Herbrand und Skolem)
Eine AussageF in Skolemform ist genau dannunerfüllbar,
wenn es eine endliche Teilmenge vonE(F ) gibt,
die (im aussagenlogischen Sinne) unerfüllbar ist.
Beweis:
Mittels des Satzes von Gödel, Herbrand und Skolem und des
Endlichkeitssatzes der Aussagenlogik.
Prof. Dr. Dietmar Seipel 229
Logik für Informatiker Wintersemester 2012/13
Semi–Entscheidungsverfahren für die Prädikatenlogik
Gilmore:
Für jede prädikatenlogische FormelF ist die Herbrand–Expansion
E(G) = {G1, G2, . . . }
der SkolemformG vonF abzählbar, da auch das Herbrand–Universum
HUF abzählbar ist.
F ist genau dannerfüllbar, wenn alle Konjunktionen
G1 ∧G2 ∧ . . . ∧Gn,
mit n ∈ IN+ = { 1, 2, . . . }, erfüllbar sind. Durch sukzessives Testen dieser
Konjunktionen auf Unerfüllbarkeit erhält man also ein Verfahren, welches
für unerfüllbare FormelnF nach endlicher Zeit stoppt.
Prof. Dr. Dietmar Seipel 230
Logik für Informatiker Wintersemester 2012/13
Für erfüllbare FormelnF terminiert das Verfahren offensichtlich nicht.
→ Semi–EntscheidbarkeitdesUnerfüllbarkeitsproblems.
Durch Anwendung des Testverfahrens auf¬F kann man auf Gültigkeit
testen.
→ Semi–EntscheidbarkeitdesGültigkeitsproblems.
Prof. Dr. Dietmar Seipel 231
Logik für Informatiker Wintersemester 2012/13
2.5 Resolution
Wir betrachten eine prädikatenlogische Formel
F = ∀X1∀X2 . . .∀Xm G
in Skolemform ohne freie Variablen und mit der MatrixG in KNF.
• Die Matrix G ist quantorenfrei und von der FormG = ∧ki=1 βi.
• Wir untersuchen nun die zugehörige Klauselmenge
M = {β1, . . . , βk }.
Eine StrukturA heißt Modell fürM , fallsA ein Modell fürF ist.
Wir betrachten eine KlauselmengeM also wie eine KNF zusammen mitAllquantoren für alle vorkommenden Variablen.
Eine Klauselβ = L1 ∨ . . . ∨ Ln wird auch oft als Menge{L1, . . . , Ln }
von Literalen repräsentiert.
Prof. Dr. Dietmar Seipel 232
Logik für Informatiker Wintersemester 2012/13
Definition (Resolutionsableitung)
SeiM eine Klauselmenge.
Eine FolgeK1, K2, . . . , Kn von Klauseln nennt manResolutionsableitung,
falls für alle1 ≤ i ≤ n gilt:
1. Ki ist eine Grundinstanz einer KlauselK ∈M ,
d.h.Ki = K[X1|t1] . . . [Xk|tk], mit t1, . . . , tk ∈ HUF , oder
2. Ki ist eine (aussagenlogische) Resolvente
zweier KlauselnKa undKb mit 1 ≤ a, b ≤ i− 1.
M ist genau dannunerfüllbar, wenn es eine Resolutionsableitung der leeren
KlauselKn = 2 gibt.
Dasselbe gilt für die entsprechende prädikatenlogische FormelF .
Prof. Dr. Dietmar Seipel 233
Logik für Informatiker Wintersemester 2012/13
Beispiel (Resolution)
Wir betrachten die KlauselmengeM = {F1, F2, F3 } mit
F1 = ¬p(X) ∨ ¬p(f(a)) ∨ q(Y ),
F2 = p(Y ),
F3 = ¬p(g(b,X)) ∨ ¬q(b).
Dann kann man
• F1[X |f(a)] [Y |b] undF2[Y |f(a)] zuK = { q(b) } resolvieren, und
• F2[Y |g(b, a)] undF3[X |a] zuK′ = {¬q(b) }.
AusK undK′ erhält man schließlich die leere Klausel2.
Also sind die KlauselmengeM und die zugehörige FormelF unerfüllbar:
F = ∀X ∀Y (F1 ∧ F2 ∧ F3).
Prof. Dr. Dietmar Seipel 234
Logik für Informatiker Wintersemester 2012/13
Baumdarstellung:
{¬p(X),¬p(f(a)), q(Y ) } { p(Y ) } {¬p(g(b,X)),¬q(b) }
{ p(f(a)) } { p(g(b, a)) }{¬p(f(a)), q(b) } {¬p(g(b, a)),¬q(b) }
{ q(b) } {¬q(b) }
2
[X|f(a)] [Y |b] [Y |f(a)] [Y |g(b, a)] [X|a]
? ? R
U � U �
s +
Die Klausel{ p(Y ) } wurde in der Resolutionsableitung zweimal benutzt.
Prof. Dr. Dietmar Seipel 235
Logik für Informatiker Wintersemester 2012/13
{¬p(X),¬p(f(a)), q(Y ) } { p(Y ) } {¬p(g(b,X)),¬q(b) }
K2 = {A } K3 = {C }K1 = {¬A,B } K4 = {¬C,¬B }
K5 = {B } K6 = {¬B }
K7 = 2
[X|f(a)] [Y |b] [Y |f(a)] [Y |g(b, a)] [X|a]
? ? R
U � U �
s +
Durch die vollständige Grundinstanziierung auf
A = p(f(a)), B = q(b), C = p(g(b, a)),
wird das Problem auf die Aussagenlogik reduziert.
Prof. Dr. Dietmar Seipel 236
Logik für Informatiker Wintersemester 2012/13
AusEffizienzgründenversucht man Substitutionen aber nur auszuführen,wenn es für den direkt nachfolgenden Resolutionsschritt erforderlich ist.
{¬p(X),¬p(f(a)), q(Y ) } { p(Y ) } {¬p(g(b,X)),¬q(b) }
{ p(f(a)) } { p(g(b,X)) }{¬p(f(a)), q(Y ) } {¬p(g(b,X)),¬q(b) }
{ q(Y ) }
{ q(b) }
{¬q(b) }
{¬q(b) }
2
[X|f(a)] [Y |f(a)] [Y |g(b,X)]
[Y |b]
? ? R
U � U �
? ?
s +
Prof. Dr. Dietmar Seipel 237
Logik für Informatiker Wintersemester 2012/13
Definition (Unifikator, allgemeinster Unifikator)
Seiθ = [X1|t1] . . . [Xn|tn] eine Substitution.
1. Für eine endliche Literalmenge
L = {L1, . . . , Lk }
setzen wirLθ = {L1θ, . . . , Lkθ }.
2. θ ist einUnifikator vonL, falls
L1θ = L2θ = . . . = Lkθ.
3. Ein Unifikatorθ vonL heißtallgemeinster UnifikatorvonL,
falls für jeden Unifikatorθ′ vonL eine Substitutionγ existiert mit
θ′ = θγ,
d.h.Fθ′ = (Fθ)γ für alle FormelnF .
θ′
θ
γ?
R
Prof. Dr. Dietmar Seipel 238
Logik für Informatiker Wintersemester 2012/13
Beispiel (Allgemeinster Unifikator)
1. θ ist ein allgemeinster Unifikator für die Literalmenge
L = { p(X), p(f(a)) }.
θ′ ist ein weiterer Unifikator, und es giltθ′ = θγ.
θ′ = [X |f(a)] [Y |b]
θ = [X |f(a)]
γ = [Y |b]
?
R
Prof. Dr. Dietmar Seipel 239
Logik für Informatiker Wintersemester 2012/13
2. θ ist ein allgemeinster Unifikator für die Literalmenge
L = { p(Y ), p(g(b,X)) }.
θ′ ist ein weiterer Unifikator, und es giltθ′ = θγ.
θ′ = [X |a] [Y |g(b, a)]
θ = [Y |g(b,X)]
γ = [X |a]
?
R
Prof. Dr. Dietmar Seipel 240
Logik für Informatiker Wintersemester 2012/13
Allgemeinste Unifikatoren sind i.a. nicht eindeutig:
L = { p(X), p(Y ) }
hat z.B. die beiden folgenden allgemeinsten Unifikatoren:
θ1 = [X |Y ],
θ2 = [Y |X ].
Es gilt θ1θ2 = θ2 und θ2θ1 = θ1.
Der folgende weitere Unifikator
θ3 = [X |Z][Y |Z]
ist allerdings kein allgemeinster Unifikator.
Es gilt θ1[Y |Z] = θ3 und θ2[X |Z] = θ3.
Prof. Dr. Dietmar Seipel 241
Logik für Informatiker Wintersemester 2012/13
Die Substitutionen bilden keine Gruppe. Es gibt ein neutrales Element[ ].Aber für
θ3 = [X |Z][Y |Z]
gibt es z.B. kein Rechts–Inversesγ3 mit
θ3γ3 = [ ].
Man kann die Anwendung vonθ3 nicht rückgängig machen, da man für einZ nicht weiß, ob es von einemX oder einemY herrührt. Ebenso gibt es für
θ4 = [X |a]
kein Rechts–Inverses, da man die Konstantea nicht auf eine VariableXabbilden kann. Auch fürθ1 undθ2 gibt es keine Rechts–Inverse.
Deswegen sindθ1θ2 = θ2 undθ2θ1 = θ1 möglich. Interessanterweise giltaußerdemθ1θ1 = θ1 undθ2θ2 = θ2 (Idempotenz).
Prof. Dr. Dietmar Seipel 242
Logik für Informatiker Wintersemester 2012/13
Unifikationssatz (J.A. Robinson)
Jede unifizierbare Menge von Literalen besitzt auch einenallgemeinsten
Unifikator.
Wir interessieren uns hauptsächlich für denjenigen allgemeinsten
Unifikator, der durch den folgenden Algorithmus bestimmt wird.
Unifikationsalgorithmus
Eingabe: eine endliche, nicht–leere Literalmenge (Literalfolge)L
θ = [ ]; ([ ] ist die leere Substitution, d.h. die identische Abbildung)
while |Lθ| > 1 do begin
durchsuche die Literale inLθ von links nach rechts, bis die erste
Position gefunden ist, wo sich mindestens zwei LiteraleL1 undL2
unterscheiden (Prädikaten– oder Argument–Position);
Prof. Dr. Dietmar Seipel 243
Logik für Informatiker Wintersemester 2012/13
if keines der beiden Zeichen an den gefundenen Positionen
ist eine Variable
thenstoppe mit der Ausgabe “nicht unifizierbar”
else begin
seiX die an der einen Position gefundene Variable
undt der Term an der anderen Position;
if X kommt in t vor (“Occurs Check”)
thenstoppe mit der Ausgabe “nicht unifizierbar”
elseθ = θ [X |t];
end;
end;
Ausgabe: θ ist einallgemeinster UnifikatorvonL
Prof. Dr. Dietmar Seipel 244
Logik für Informatiker Wintersemester 2012/13
Beispiel (Unifikationsalgorithmus)
1. Für die LiteralmengeL = { p(X), p(f(a)), p(Y ) } sind die
Prädikatenpositionen alle gleichp.
L = { p( X︸︷︷︸
), p(f(a)︸︷︷︸
), p( Y︸︷︷︸
) }? ? ?
6 6 6
Die ersten Unterschiede liegen in den Argumenten. Also setzen wir
θ1 = [X |f(a)] und erhaltenLθ1 = { p(f(a)), p(Y ) }, da die ersten
beiden Atome zusammenfallen.
Mittels θ2 = [Y |f(a)] erhalten wirθ = θ1θ2 = [X |f(a)][Y |f(a)] und
Lθ = { p(f(a)) }. Wegen|Lθ| = 1 ist θ ein allgemeinster Unifikator.
Prof. Dr. Dietmar Seipel 245
Logik für Informatiker Wintersemester 2012/13
2. Für die LiteralmengeL = {L1, L2 }, mit
L1 = p(f(Z, g(a, Y )), h(Z)),
L2 = p(f(f(U, V ),W ), h(f(a, b))),
sind die ersten unterschiedlichen PositionenX = Z undt = f(U, V ).
Somit erhalten wirθ1 = [Z|f(U, V )].
FürLθ1 = {L1θ1, L2θ1 }, mit
L1θ1 = p(f(f(U, V ), g(a, Y )), h(f(U, V ))),
L2θ1 = L2,
sind die ersten unterschiedlichen PositionenX = W undt = g(a, Y ).
Somit erhalten wirθ2 = [W |g(a, Y )].
Prof. Dr. Dietmar Seipel 246
Logik für Informatiker Wintersemester 2012/13
FürLθ1θ2 = {L1θ1θ2, L2θ1θ2 }, mit
L1θ1θ2 = p(f(f(U, V ), g(a, Y )), h(f(U, V ))) und
L2θ1θ2 = p(f(f(U, V ), g(a, Y )), h(f(a, b)))
sind die ersten unterschiedlichen PositionenX = U undt = a. Somit
erhalten wirθ3 = [U |a]. Abschließend erhalten wir nochθ4 = [V |b].
Insgesamt erhalten wir die Substitution
θ = θ1θ2θ3θ4
= [Z|f(U, V )][W |g(a, Y )][U |a][V |b]
= [Z|f(a, b)][W |g(a, Y )][U |a][V |b],
und
L1θ = p(f(f(a, b), g(a, Y )), h(f(a, b))) = L2θ.
Prof. Dr. Dietmar Seipel 247
Logik für Informatiker Wintersemester 2012/13
3. Die LiteralmengeL = { p, q } ist nicht unifizierbar,
da die Prädikatensymbole nicht übereinstimmen.
4. Die LiteralmengeL = { p(a), p(b) } ist nicht unifizierbar,
da die Argumente unterschiedliche Konstanten sind.
5. Die LiteralmengeL = { p(f(X)), p(g(X)) } ist nicht unifizierbar,
da die Funktionssymbolef undg nicht übereinstimmen.
6. Die LiteralmengeL = { p(X), p(f(X)) } ist ebenfalls nicht
unifizierbar, denn der Occurs Check stellt fest,
daß der Termt = f(X) die VariableX enthält.
Wenn manX mittelsθ = [X |t′] durch einen Termt′ ersetzt, etwa
durcht′ = t = f(X), dann enthältp(X)θ = p(t′) immer ein Auftreten
des Funktionssymbolsf weniger alsp(f(X))θ = p(f(t′)).
Prof. Dr. Dietmar Seipel 248
Logik für Informatiker Wintersemester 2012/13
Occurs Check
In PROLOG wird der Occurs Check aus Effizienzgründen meistweggelassen, da der aufX zu testende Termt sehr groß sein kann.
?- X = f(X).
X = f(**).
• Das Ergebnis der Unifikation vonX undf(X) ist in SWI–PROLOG dieSubstitution[X |f(**)] – aber ohne die sonst übliche Ausgabetrue.
• Wie bei Dauerschleifen in herkömmlichen Programmiersprachen wieJAVA , geht man aber davon aus, daß ein Programmierer in der Praxisdiese fehlerhaften Unifikationen vermeidet.
• Aus rein theoretischer Sicht könnte man über unendlichenTermstrukturen als Ergebnis die Substitution[X |f(f(f(...)))] angeben,dieX durch einen unendlich tief verschachtelten Term ersetzt.
Prof. Dr. Dietmar Seipel 249
Logik für Informatiker Wintersemester 2012/13
Definition (Prädikatenlogische Resolution)
SeienK1 undK2 prädikatenlogische Klauseln.
1. Seienθ1 undθ2 Substitutionen, welche die Variablen vonK1 undK2
so umbenennen, daßK1θ1 undK2θ2 keine gemeinsamen Variablenmehr enthalten – wir nennen sie dannvariablendisjunkt.
2. Für ein AtomA setzen wirA = ¬A und¬A = A.
3. Es gebe nun LiteraleL1, . . . , Lm ∈ K1θ1 undL′1, . . . , L
′n ∈ K2θ2,
mit m ≥ 1 undn ≥ 1, so daß
L = {L1, . . . , Lm, L′1, . . . , L
′n }
unifizierbar ist mit einem allgemeinsten Unifikatorθ.
4. Dann ist die folgende prädikatenlogische KlauselK eineprädikatenlogischeResolventevonK1 undK2:
K = ((K1θ1\{L1, . . . , Lm }) ∪ (K2θ2\{L′1, . . . , L
′m }))θ.
K1 K2
KU �
Prof. Dr. Dietmar Seipel 250
Logik für Informatiker Wintersemester 2012/13
Alternative, abstraktere Formulierung
• 1. und 2. wie oben.
• Für eine LiteralmengeL setzen wirdL = {L |L ∈ L}.
• Es gebe nun nicht–leere Literalmengen
L1 ⊆ K1θ1, L2 ⊆ K2θ2,
so daßL1 ∪ L2 unifizierbar ist mit einem allgemeinsten Unifikatorθ.
• Dann ist die prädikatenlogische Klausel
K = ((K1θ1 \ L1) ∪ (K2θ2 \ L2))θ
eine prädikatenlogischeResolventevonK1 undK2.
K1 K2
KU �
Prof. Dr. Dietmar Seipel 251
Logik für Informatiker Wintersemester 2012/13
Beispiel (Prädikatenlogische Resolution)
Da die Klauselmenge{K1, K2 } für die Formel
∀X (p(X) ∧ ¬p(f(X))) ≡ (∀X p(X)) ∧ (∀X ¬p(f(X)))
steht, können wirK1 undK2 variablendisjunkt machen.
K1 = { p(X) } K2 = {¬p(f(X)) }
K′1 = { p(X) } K′
2 = {¬p(f(U)) }
K = 2
? ?
j �
Wir setzenK′1 = K1, d.h.θ1 = [ ], undK′
2 = K2θ2, mit θ2 = [X |U ].
Dann istθ = [X |f(U)] ein allgemeinster Unifikator für
L = { p(X), p(f(U)) }, und wir erhalten die ResolventeK = 2 = ∅.
Prof. Dr. Dietmar Seipel 252
Logik für Informatiker Wintersemester 2012/13
Beispiel (Prädikatenlogische Resolution)
K1 = { p(f(X)),¬q(Z), p(Z) } K2 = {¬p(X), r(g(X), a) }
K = {¬q(f(X)), r(g(f(X)), a) }^ �
Wir setzen
θ1 = [ ],
θ2 = [X |U ],
θ = [U |f(X)] [Z|f(X)].
θ ist ein allgemeinster Unifikator fürL = { p(f(X)), p(Z), p(U) }.
Prof. Dr. Dietmar Seipel 253
Logik für Informatiker Wintersemester 2012/13
Die Resolutionsmengenwerden analog zur Aussagenlogik definiert.
Definition (Resolutionsmengen)
SeiM eine prädikatenlogische Klauselmenge.
Res(M) = M ∪ {K |K ist eine prädikatenlogische Resolvente
zweier KlauselnK1, K2 ∈M }.
Ferner definieren wir:
Res0(M) = M,
Resn+1(M) = Res(Resn(M)), für n ≥ 0,
Res∗(M) =⋃
n≥0Resn(M).
Es gibt meist sehr viele Resolventen, die wir nicht alle aufzählen können.
Außerdem ist das Variablendisjunkt–Machen nicht eindeutig.
Prof. Dr. Dietmar Seipel 254
Logik für Informatiker Wintersemester 2012/13
Beispiel (Resolutionsmengen)
Für die KlauselmengeM = {F1, F2, F3 } mit
F1 = ¬p(X) ∨ ¬p(f(a)) ∨ q(Y ),
F2 = p(Y ),
F3 = ¬p(g(b,X)) ∨ ¬q(b),
zur FormelF = ∀X ∀Y (F1 ∧ F2 ∧ F3) erhalten wir folgendes:
• Je nachdem ob wir bei der Resolution vonF1 undF2 beidep–Literale
ausF1 gegenF2 = p(Y ) resolvieren oder jeweils nur eines, erhalten
wir drei unterschiedliche Resolventen:
q(Y ), ¬p(f(a)) ∨ q(Y ), ¬p(X) ∨ q(Y ).
• Die Resolution vonF2 undF3 über diep–Literale ergibt
¬q(b).
Prof. Dr. Dietmar Seipel 255
Logik für Informatiker Wintersemester 2012/13
• Die Resolution vonF1 undF3 über dieq–Literale ergibt
¬p(X) ∨ ¬p(f(a)) ∨ ¬p(g(b,X ′)).
Um die Klauseln variablendisjunkt zu machen, habenX in F3 durch
X ′ ersetzt. Diese Substitution ist natürlich nicht eindeutig.
Wir erhalten also die folgenden Resolutionsmengen:
Res0(M) = M,
Res1(M) = M ∪ {¬p(f(a)) ∨ q(Y ), ¬p(X) ∨ q(Y ), q(Y ), ¬q(b),
¬p(X) ∨ ¬p(f(a)) ∨ ¬p(g(b,X ′)) },
Res2(M) = Res1(M) ∪ {2, . . . }.
Res2(M) enthält hier – neben der leeren Klausel2 – weitere Resolventen,
die wir nicht alle aufzählen wollen.
Prof. Dr. Dietmar Seipel 256
Logik für Informatiker Wintersemester 2012/13
Resolutionssatz der Prädikatenlogik
SeiF eine prädikatenlogische Formel in Skolemform ohne freie Variablen
und mit (quantorenfreier) Matrix in KNF, und seiM die zugehörige
Klauselmenge.
F ist genau dannunerfüllbar, wenn2 ∈ Res∗(M).
Eine Resolutionsableitung verwendet immer nur endlich viele Klauseln.
Deswegen ist der Kompaktheitssatz entscheident, der besagt, daß eine
unerfüllbare Formelmenge bereits eine endliche unerfüllbare Teilmenge
haben muß.
Der Beweis des Resolutionssatzes erfolgt durch Lifting des
aussagenlogischen Satzes.
Prof. Dr. Dietmar Seipel 257
Logik für Informatiker Wintersemester 2012/13
Lifting–Lemma
SeienK1 undK2 zwei prädikatenlogische Klauseln, und seienK′1 undK′
2
beliebigeGrundinstanzenvonK1 bzw.K2.
• SeiK′ eine Resolvente vonK′1 undK′
2 im aussagenlogischen Sinn.
• Dann gibt es eineprädikatenlogische ResolventeK vonK1 undK2,so daßK′ eine Grundinstanz vonK ist.
K1 K2
K
K′1 K′
2
K′
j �
j �
? ?
?
Prof. Dr. Dietmar Seipel 258
Logik für Informatiker Wintersemester 2012/13
Beispiel (Lifting–Lemma)
{ p(f(X)),¬q(Z), p(Z) } {¬p(X), r(g(X), a) }
{¬q(f(X)), r(g(f(X)), a)
{ p(f(b)),¬q(f(b)), p(f(b)) } {¬p(f(b)), r(g(f(b)), a) }
{¬q(f(b)), r(g(f(b)), a)
θ1 = [X|b] [Z|f(b)] θ2 = [X|f(b)]j �
j �
? ?
?
Prof. Dr. Dietmar Seipel 259
Logik für Informatiker Wintersemester 2012/13
Beispiel (Resolution mit Gruppenaxiomen)
Wir schreibenp(X, Y, Z) anstelle vonX ◦ Y = Z (Produkt).
(1) Abgeschlossenheit:
∀X∀Y ∃Z p(X, Y, Z).
(2) Assoziativität:
∀U∀V ∀W ∀X∀Y ∀Z
( p(X, Y, U) ∧ p(Y, Z, V )→ (p(X,V,W )↔ p(U,Z,W ) ).
äquivalent:∀ . . . ( X ◦ (Y ◦ Z) = W ↔ (X ◦ Y ) ◦ Z = W ).
(3) Existenz eines links–neutralen Elements (X) und Existenz von
Links–Inversen (Z):
∃X ∀Y (p(X, Y, Y ) ∧ ∃Z p(Z, Y,X)).
äquivalent:∃X ∀Y ((X ◦ Y = Y ) ∧ ∃Z (Z ◦ Y = X)).
Prof. Dr. Dietmar Seipel 260
Logik für Informatiker Wintersemester 2012/13
(4) Existenz von Rechts–Inversen:
∃X ∀Y (p(X, Y, Y ) ∧ ∃Z p(Y, Z,X)).
äquivalent:∃X ∀Y ((X ◦ Y = Y ) ∧ ∃Z (Y ◦ Z = X)).
Es stellt sich heraus, daß man die Existenz von Rechts–Inversen nicht
separat in einem Axiom fordern muß, da sie bereits aus den anderen
Gruppenaxiomen (1), (2) und (3) folgt.
Um dies zu zeigen, betrachten wir die Negation von (4).
Diese ist äquivalent zur BPF
∀X ∃Y ∀Z (¬p(X, Y, Y ) ∨ ¬p(Y, Z,X)).
• DaZ nicht in der Teilformelp(X, Y, Y ) vorkommt, kann man in (4)den Existenzquantor∃Z nach vorne ziehen.
• Die Negation vertauscht All– und Existenzquantoren, und sie
verwandelt nach De Morgan eine Konjunktion in eine Disjunktion.
Prof. Dr. Dietmar Seipel 261
Logik für Informatiker Wintersemester 2012/13
Die Formel zur Assoziativität wird z.B. schematisch wie folgt umgeformt:
∀ . . . ( α→ (A↔ B) ) ≡
∀ . . . ( α→ ((A ∧B) ∨ (¬A ∧ ¬B)) ) ≡
∀ . . . ( α→ ((A ∨ ¬B) ∧ (¬A ∨B)) ) ≡
∀ . . . ( (α ∧B → A) ∧ (α ∧A→ B) ).
Es wurde zweimal verwendet, daß ein negiertes Literal¬B im Kopf einer
Regel alsB in den Rumpf verschoben werden kann:
∀ . . . ( A1 ∧A2 → (A ∨ ¬B) ) ≡
∀ . . . ( ¬A1 ∨ ¬A2 ∨A ∨ ¬B ) ≡
∀ . . . ( A1 ∧A2 ∧B → A ).
Wir erhalten also aus(2) zwei Implikationen.
Die Folgerung{ (1), (2), (3) } |= (4) gilt genau dann, wenn
{ (1), (2), (3),¬(4) } unerfüllbar ist.
Prof. Dr. Dietmar Seipel 262
Logik für Informatiker Wintersemester 2012/13
Klauselformvon (1) ∧ (2) ∧ (3) ∧ ¬(4) mit Skolemfunktionenm, e, i, j:
(1) Abgeschlossenheit:
(a) { p(X, Y,m(X, Y )) }.
(2) Assoziativität:
(b) {¬p(X, Y, U),¬p(Y, Z, V ),¬p(X,V,W ), p(U,Z,W ) },
(c) {¬p(X, Y, U),¬p(Y, Z, V ),¬p(U,Z,W ), p(X,V,W ) }.
(3) Existenz eines links–neutralen Elementse und Existenz von
Links–Inverseni(Y ) für GruppenelementeY :
(d) { p(e, Y, Y ) },
(e) { p(i(Y ), Y, e) }.
(4) Negation der Existenz von Rechts–Inversen:
(f) {¬p(X, j(X), j(X)),¬p(j(X), Z,X) }.
Prof. Dr. Dietmar Seipel 263
Logik für Informatiker Wintersemester 2012/13
Resolutionsherleitungder leeren Klausel
(f) {¬p(X, j(X), j(X)),¬p(j(X), Z,X) }
| (d) { p(e, Y, Y ) }↓ ւ
{¬p(j(e), Z, e) }
| (b) {¬p(X, Y, U),¬p(Y, Z, V ),¬p(X,V,W ), p(U,Z,W )}↓ ւ
{¬p(X, Y, j(e)),¬p(Y, Z, V ),¬p(X,V, e) }
| (e) { p(i(Y ), Y, e) }↓ ւ
{¬p(i(V ),W, j(e)),¬p(W,Z, V ) }
| (d) { p(e, Y, Y ) }↓ ւ
{¬p(i(V ), e, j(e)) }
Prof. Dr. Dietmar Seipel 264
Logik für Informatiker Wintersemester 2012/13
| (c) {¬p(X, Y, U),¬p(Y, Z, V ),¬p(U,Z,W ), p(X,V,W )}↓ ւ
{¬p(i(V ), Y, U),¬p(Y, Z, e),¬p(U,Z, j(e))}
| (d) { p(e, Y, Y ) }↓ ւ
{¬p(i(V ), Y, e),¬p(Y, j(e), e)}
| (e) { p(i(Y ), Y, e) }↓ ւ
{¬p(i(V ), i(j(e)), e) }
| (e) { p(i(Y ), Y, e) }↓ ւ
2
Also folgt das vierte Gruppenaxiom aus den ersten dreien:
(1) ∧ (2) ∧ (3) |= (4).
Prof. Dr. Dietmar Seipel 265
Logik für Informatiker Wintersemester 2012/13
Da wir in diesem Beispiel ausschließlich Horn–Klauseln vorliegen haben,
können wir dieResolutionsherleitungauch in Implikationsnotation schreiben:
(f) ← p(X, j(X), j(X)) ∧ p(j(X), Z,X)
| (d) p(e, Y, Y )↓ ւ
← p(j(e), Z, e)
| (b) p(U,Z,W )← p(X, Y, U) ∧ p(Y, Z, V ) ∧ p(X,V,W )↓ ւ
← p(X, Y, j(e)) ∧ p(Y, Z, V ) ∧ p(X,V, e)
| (e) p(i(Y ), Y, e)↓ ւ
← p(i(V ),W, j(e)) ∧ p(W,Z, V )
| (d) p(e, Y, Y )↓ ւ
← p(i(V ), e, j(e))
Prof. Dr. Dietmar Seipel 266
Logik für Informatiker Wintersemester 2012/13
| (c) p(X,V,W )← p(X, Y, U) ∧ p(Y, Z, V ) ∧ p(U,Z,W )↓ ւ
← p(i(V ), Y, U) ∧ p(Y, Z, e) ∧ p(U,Z, j(e))
| (d) p(e, Y, Y )↓ ւ
← p(i(V ), Y, e) ∧ p(Y, j(e), e)
| (e) p(i(Y ), Y, e)↓ ւ
← p(i(V ), i(j(e)), e)
| (e) p(i(Y ), Y, e)↓ ւ
2
Es handelt sich um einelineare Herleitungvon Goals. Bis auf den ersten
Schritt wird immer zuerst das rechteste Atom des Goal–Rumpfes resolviert.
Wenn man zuerst mit (b) und dann mit (d) resolvieren würde, dann wäre
dies – wie bei der SLD–Resolution in Kapitel 3 – immer der Fall.
Prof. Dr. Dietmar Seipel 267
Logik für Informatiker Wintersemester 2012/13
Prädikatenlogik der zweiten Stufe (PL2)
Die Prädikatenlogik ist zwar ausdrucksstärker als die Aussagenlogik.
Aber trotzdem kann auch im Rahmen der Prädikatenlogik nichtjede
mathematische Aussage formuliert werden.
Wir erhalten eine noch größere Ausdrucksstärke, wenn wir zusätzlich
Quantifizierungenüber
• Prädikaten–und
• Funktionssymbolen
erlauben.
Beispiel (PL2)
F = ∀p ∃f ∀X p(f(X)).
Prof. Dr. Dietmar Seipel 268
Logik für Informatiker Wintersemester 2012/13
Exkurs: Induktionsaxiom der natürlichen Zahlen in PL2
DasInduktionsaxiomwurde ursprünglich in der PL2 formuliert:
∀p ( p(0) ∧ ∀N (N ∈ IN0 ∧ p(N)→ p(s(N))) →
∀N (N ∈ IN0 → p(N)) ).
Es verwendet ein1–stelliges Funktionssymbols zur Bezeichnung desNachfolgers einer natürlichen Zahl, und es quantifiziert über ein1–stelligesPrädikatensymbolp.
Das Axiom besagt, daß jede induktive Teilmenge vonIN0 – beschriebendurch das Prädikatp – gleichIN0 sein muß:
• Fallsp für die Zahl0 gilt, und
• falls für alleN ∈ IN0 ausp(N) auchp(s(N)) folgt,d.h., wennp für N gilt, dann giltp auch fürN + 1,
• dann giltp für alleN ∈ IN0.
Prof. Dr. Dietmar Seipel 269
Logik für Informatiker Wintersemester 2012/13
Peano–Axiome der natürlichen Zahlen
(P1) ∀N ¬ (s(N) ≡ 0),
(P2) ∀N ∀M (s(N) ≡ s(M) → N ≡M),
(P3) ∀p ( p(0) ∧ ∀N (p(N)→ p(s(N))) → ∀N p(N) ).
(P3) ist eine verkürzte Version des Induktionsaxioms in derPL2.
Zusätzlich muß das Gleichheitsprädikat≡ geeignet axiomatisiert werden.
Dann sind alle ModelleA der GesamtformelmengeF isomorph.
Z.B. gibt es das (eindeutige)Herbrand–Modellmit der Grundmenge
HUF = { 0, s(0), s(s(0)), . . . } = { sn(0) | n ∈ IN0 }.
Das Herbrand–Modell repräsentiert eine natürliche Zahln ∈ IN als einen
Termsn(0) mit n Auftreten des Funktionssymbolss.
Wir setzen dazus0(0) = 0 undsn+1(0) = s(sn(0)), für n ∈ IN0.
Prof. Dr. Dietmar Seipel 270
Logik für Informatiker Wintersemester 2012/13
Ein anderes ModellA, das vonJohn von Neumannvorgeschlagen wurde,repräsentiert eine natürliche Zahln ∈ IN als eine Menge.
Dazu werden die Termesn(0) ausHUF folgendermaßen interpretiert:
0A = ∅,
s(t)A = tA ∪ {tA}.
Wenn wir(sn(0))A = sn schreiben, dann erhalten wir:
s0 = ∅,
s1 = s0 ∪ { s0 } = ∅ ∪ { ∅ } = { ∅ } = { s0 },
s2 = s1 ∪ { s1 } = { ∅, { ∅ } } = { s0, s1 },
sn+1 = sn ∪ { sn } = { s0, s1, . . . , sn }.
Man kann dagegen zeigen, daß jede Axiomatisierung der natürlichenZahlen als Peano–Struktur im Rahmen der PL1Nicht–Standardmodelle
aller unendlichen Kardinalitäten zuläßt.
Prof. Dr. Dietmar Seipel 271
Logik für Informatiker Wintersemester 2012/13
Mathematische Theorien
EineTheorieist eine MengeT von Formeln (möglicherweise beschränkt
auf solche Formeln, die nur aus bestimmten vorgegebenen Bestandteilen –
z.B. bestimmten Prädikaten– und Funktionssymbolen – aufgebaut ist), die
gegenüber Folgerbarkeit abgeschlossen ist. D.h., falls
{F1, . . . , Fn } ⊆ T
gilt und
F eine Folgerung aus{F1, . . . , Fn } ist,
dann gilt auch
F ∈ T
Die FormelnF ∈ T heißen auchSätzeder Theorie.
Prof. Dr. Dietmar Seipel 272
Logik für Informatiker Wintersemester 2012/13
Prof. Dr. Dietmar Seipel 273
Logik für Informatiker Wintersemester 2012/13
2.6 Hyperresolution für Hornformeln
Eine prädikatenlogische KlauselK = L1 ∨ . . . ∨ Ln ist eineHornklausel,
falls maximal ein LiteralLi positiv ist – wie in der Aussagenlogik.
Es gibt auch wieder drei interessante Spezialfälle;
im folgenden seienA undB1, . . . , Bm prädikatenlogische Atome:
• Eine(definite) Regelist ein HornklauselK = A ∨ ¬B1 ∨ . . . ∨ ¬Bm
mit genau einem positiven Literal.
• Ein (definites) Faktist einen RegelK = A ohne negative Literale (m = 0).
• EineGoal (Ziel, Anfrage)ist eine HornklauselK = ¬B1 ∨ . . . ∨ ¬Bm
ohne positives Literal.
Prof. Dr. Dietmar Seipel 274
Logik für Informatiker Wintersemester 2012/13
In der Logikprogrammierung verwendet man – aufgrund der Regeln von De
Morgan – für Hornklauseln folgende Implikations–Notation:
Fakt: A,
Regel: A← B1 ∧ . . . ∧Bm, m ≥ 0,
Goal: ← B1 ∧ . . . ∧Bm, m ≥ 0.
Regeln und Fakten:
• Das AtomA heißtKopf einer Regelr = A← β.
• Die Konjunktionβ = B1 ∧ . . . ∧Bm ist derRumpfder Regelr.
Die AtomeBi, mit 1 ≤ i ≤ m, heißen Rumpfatome.
• Fallsm = 0 ist, so wird die Regel mit dem FaktA gleichgesetzt.
Goals werden bei der SLD–Resolution (Kapitel 3) für Anfragen benutzt; in
diesem Abschnitt zur Hyperresolution verwenden wir keine Goals.
Prof. Dr. Dietmar Seipel 275
Logik für Informatiker Wintersemester 2012/13
DATALOG –Programme: verwendet in Deduktiven Datenbanken
In der Aussagenlogik enthalten Hornformeln keine Variablensymbole.
Als Erweiterung betrachten wir nun in der Prädikatenlogik Hornformeln,
bei denen alle Variablensymbole in mindestens einem Rumpfatom
vorkommen. Solche Hornformeln nennen wirbereichsbeschränkt.
Eine Menge von bereichsbeschränkten Hornformeln in
Implikationsnotation nennen wir DATALOG–Programm.
• Im strengen Sinne können DATALOG–ProgrammeP auch keine
Funktionssymbole enthalten. Dann ist das Herbrand–UniversumHUP
endlich, und es können nur endlich viele Atome abgeleitet werden.
• In praktischen Anwendungen verwendet man aber oft die Erweiterung
um Funktionssymbole namens DATALOGfun . Dann liegt es am
Programmierer, Dauerschleifen bei der Ableitung zu vermeiden.
Prof. Dr. Dietmar Seipel 276
Logik für Informatiker Wintersemester 2012/13
Beispiel (DATALOG–Programm)
Die folgenden Regeln bilden ein DATALOG–ProgrammP zur Berechnung
der Vorfahren (ancestor ) aufgrund der Eltern–Relation (parent):
ancestor(X, Y )← parent(X, Y ),
ancestor(X, Y )← parent(X,Z) ∧ ancestor(Z, Y ).
Zugehörige Eltern–Fakten:
parent(a, b), parent(b, c), parent(c, d).
Jeder Elternteil ist ein Vorfahre (Regel 1), und jeder Vorfahre der Eltern ist
ebenfalls ein Vorfahre (Regel 2).
In PROLOG sind auch Regeln sinnvoll, bei denen Variablensymbole nur im
Kopf vorkommen – wie z.B. das Fakt zuhres_iteration/3 am Ende
dieses Abschnittes.
Prof. Dr. Dietmar Seipel 277
Logik für Informatiker Wintersemester 2012/13
Hyperresolution
Die sukzessive,n–fache Anwendung der binären Resolution auf eine RegelA← B1 ∧ . . . ∧Bn und geeignete FaktenAi nennt man Hyperresolution.Die RumpfatomeBi werden sukzessive mit den FaktenAi resolviert.
A ∨ ¬B1 ∨ ¬B2 ∨ . . . ∨ ¬Bn
(A ∨ ¬B2 ∨ . . . ∨ ¬Bn) θ1
...
(A ∨ ¬Bn) θ1 . . . θn−1
Aθ1 . . . θn
θ1
θ2
θn
A1
A2
...
An
?
?
?
?
9
9
9
9
Wir nennen das berechnete FaktAθ1 . . . θn eine Hyperresolvente.
Prof. Dr. Dietmar Seipel 278
Logik für Informatiker Wintersemester 2012/13
DATALOG–Fakten enthalten keine Variablensymbole.
Deswegen muß man die FaktenAi und die zwischendurch erhaltenen
Regeln nicht variablendisjunkt machen.
Es genügt Substitutionenθi zu finden, so daß
(Bi θ1 . . . θi−1) θi = Ai.
Wir bezeichen
θ = θ1 . . . θn
als die berechnete Substitution. Die berechnete Hyperresolvente
Aθ
ist dann automatisch auch ein Fakt ohne Variablensymbole,
da ja alle Variablensymbole aus dem RegelkopfA in den RumpfatomenBi
enthalten sind und somit vonθ grundinstanziiert werden.
Prof. Dr. Dietmar Seipel 279
Logik für Informatiker Wintersemester 2012/13
Beispiel (Hyperresolution)
Für das DATALOG–ProgrammP mit den Regeln
anc(X, Y )← par(X, Y ),
anc(X, Y )← par(X,Z) ∧ anc(Z, Y ),
und den Eltern–Fakten
par(a, b),
par(b, c),
par(c, d),
erhalten wir folgendes:
1. Die Fakten ausP werden mittels einer Hyperresolution durchn = 0
Anwendungen der binären Resolution abgeleitet.
Prof. Dr. Dietmar Seipel 280
Logik für Informatiker Wintersemester 2012/13
2. Dann kann aus dem Faktpar(b, c) und der ersten Regel ein Fakt
anc(b, c) abgeleitet werden:
anc(X,Y )← par(X,Y )
anc(b, c)
θ1 = [X|b] [Y |c]
par(b, c)
?)
Die berechnete Substitution ist
θ = θ1 = [X |b] [Y |c],
und es wirdanc(X, Y )θ = anc(b, c) abgeleitet.
Ebenso werden die Faktenanc(a, b) undanc(c, d) abgeleitet.
Prof. Dr. Dietmar Seipel 281
Logik für Informatiker Wintersemester 2012/13
3. Danach kann aus den Faktenpar(a, b) undanc(b, c) und der zweiten
Regel das Faktanc(a, c) abgeleitet werden:
anc(X,Y )← par(X,Z) ∧ anc(Z, Y )
anc(a, Y )← anc(b, Y )
anc(a, c)
θ1 = [X|a] [Z|b]
θ1 = [Y |c]
par(a, b)
anc(b, c)
?
?
9
9
Die berechnete Substitution ist
θ = θ1θ2 = [X |a] [Z|b] [Y |c],
und es wirdanc(X, Y )θ = anc(a, c) abgeleitet.
Prof. Dr. Dietmar Seipel 282
Logik für Informatiker Wintersemester 2012/13
Ebenso kann das Faktanc(b, d) abgeleitet werden.
4. Zuletzt kann aus dem Faktanc(b, d) das Faktanc(a, d) abgeleitet
werden:
anc(X,Y )← par(X,Z) ∧ anc(Z, Y )
anc(a, Y )← anc(b, Y )
anc(a, d)
θ1 = [X|a] [Z|b]
θ1 = [Y |d]
par(a, b)
anc(b, d)
?
?
9
9
Insgesamt haben wir also die folgendenanc–Fakten abgeleitet:
anc(a, b), anc(b, c), anc(c, d), anc(a, c), anc(b, d), anc(a, d).
Prof. Dr. Dietmar Seipel 283
Logik für Informatiker Wintersemester 2012/13
In Iterationn ≥ 2 werden also dieanc–Fakten zu den Pfaden der Länge
n− 1 in der Vorfahrenhierarchie abgeleitet:
a
b
c
d
6
6
6
I
� Y
Die durchgezogenen Linien zeigen diepar–Fakten und die entsprechenden
anc–Fakten zu den Pfaden der Länge1.
Die gestrichelten Linien zeigen dieanc–Fakten zu den Pfaden der Länge2
und3. Das Faktanc(a, d) zur Länge3 wird in Iteration4 auspar(a, b) und
anc(b, d) abgeleitet.
Prof. Dr. Dietmar Seipel 284
Logik für Informatiker Wintersemester 2012/13
Hyperresolutionsmengen
SeiP ein DATALOG–Programm undI eine Herbrand–Interpretation.
1. Hres(P, I) ist die Menge aller Hyperresolventen, die man aus einer
Regel ausP und geeigneten Fakten ausI herleiten kann:
2. Also bestehtHres(P, I) aus allen GrundatomenAθ, so daß es eine
RegelA← B1 ∧ . . . ∧Bn ∈ P gibt, mitBiθ ∈ I , für alle1 ≤ i ≤ n.
3. Man könnte auch sagen:Hres(P, I) besteht aus allen GrundatomenA,
so daß es eine GrundinstanzA← B1 ∧ . . . ∧Bn einer Regel ausP
gibt, mitBi ∈ I , für alle1 ≤ i ≤ n.
4. Wenngnd (P ) die Menge dieser Grundinstanzen ist, dann gilt:
Hres(P, I) = {A |A← β ∈ gnd (P ) ∧ I |= β }.
Für ein festesP , schreibt man anstelle vonHres(P, I) oft auchHresP (I).
Prof. Dr. Dietmar Seipel 285
Logik für Informatiker Wintersemester 2012/13
Man kann auch wieder PotenzenHresn(P ) bilden:
Hres0(P ) = ∅,
Hresn+1(P ) = Hres(P,Hresn(P )),
Hres∗(P ) =⋃
n∈IN+Hresn(P ).
Offensichtlich gilt auch hier die Monotonie–Eigenschaft:
P ⊆ P ′ ∧ I ⊆ I ′ ⇒ Hres(P, I) ⊆ Hres(P ′, I ′).
Also kann man wieder durch vollständige Induktion folgendes zeigen:
Hresn(P ) ⊆ Hresn+1(P ).
Wir schreiben Fakten in den Hyperresolutionsmengen als Atome.
Prof. Dr. Dietmar Seipel 286
Logik für Informatiker Wintersemester 2012/13
Beispiel (Hyperresolutionsmengen)
Für das DATALOG–ProgrammP mit den Regeln
anc(X, Y )← par(X, Y ),
anc(X, Y )← par(X,Z) ∧ anc(Z, Y ),
und den Eltern–Fakten
par(a, b), par(b, c), par(c, d),
erhalten wir folgendes:
Hres0(P ) = ∅,
Hres1(P ) = { par(a, b), par(b, c), par(c, d) },
Hres2(P ) = Hres1(P ) ∪ { anc(a, b), anc(b, c), anc(c, d) },
Hres3(P ) = Hres2(P ) ∪ { anc(a, c), anc(b, d) },
Hres4(P ) = Hres3(P ) ∪ { anc(a, d) }.
Prof. Dr. Dietmar Seipel 287
Logik für Informatiker Wintersemester 2012/13
Exkurs: Hyperresolution in PROLOG
Wir kodieren eine DATALOG–RegelA← B1 ∧ . . . ∧Bn als einePaar–Struktur
[A]-[B1,...,Bn].
Die Liste[A] enthält das Kopfatom, die Liste[B1,...,Bn] die
Rumpfatome. Ein Fakt, d.h., eine Regel ohne Rumpfatome (n = 0), kannauch kurz als[A] kodiert werden.
parse_rule(Head-Body, Head-Body) :-
!.
parse_rule(Head, Head-[]).
parse_rule/2 zerlegt eine DATALOG–Regel in Kopf und Rumpf.
Dann wird aus einem Fakt[A] eine Paar–Struktur[A]-[] mit einemleeren Rumpf.
Prof. Dr. Dietmar Seipel 288
Logik für Informatiker Wintersemester 2012/13
Das Prädikathres/3 generiert zu einem DATALOG–ProgrammProgram
und einer Herbrand–InterpretationInt_1 eine neue
Herbrand–InterpretationInt_2 bestehend aus den Hyperresolventen.
% hres(+Program, +Int_1, -Int_2) <-
hres(Program, Int_1, Int_2) :-
findall( A,
( member(Rule, Program),
parse_rule(Rule, [A]-Body),
members(Body, Int_1) ),
Int_2 ).
Der Aufruf findall(A,Goal,Int_2) sammelt über Backtracking alle
HyperresolventenA in einer ListeInt_2. Das DDK erlaubt sogar folgende
Mengenschreibweise:Int_2 <= {A|Goal}.
Prof. Dr. Dietmar Seipel 289
Logik für Informatiker Wintersemester 2012/13
Der Aufruf member(B, Int_1) für ein AtomB und eine
Herbrand–InterpretationInt_1 findet geeignete Grundinstanzen
vonB, die inInt_1 liegen.
?- Int_1 = [ par(a, b), par(b, c), par(c, d),
anc(b, c), anc(b, d), anc(c, d) ],
B = par(X, Z),
member(B, Int_1).
B = par(a, b), X = a, Z = b ;
B = par(b, c), X = b, Z = c ;
B = par(c, d), X = c, Z = d ;
No
?-
Prof. Dr. Dietmar Seipel 290
Logik für Informatiker Wintersemester 2012/13
Der Aufruf members(Body, Int_1) in hres/3 kann wie folgt
implementiert werden:
Variante 1 (foreach–do–Schleife):
members(Xs, Ys) :-
foreach(X, Xs) do
member(X, Ys).
Variante 2 (Listen–Rekursion):
members([X|Xs], Ys) :-
member(X, Ys),
members(Xs, Ys).
members([], _).
Prof. Dr. Dietmar Seipel 291
Logik für Informatiker Wintersemester 2012/13
Wenn man in der rekursiven ImplementierungX=B1 undXs=[B2,...,Bn]setzt, so ergibt sich wegen[B1,B2,...,Bn]=[B1|[B2,...,Bn]]folgendes: aus dem Aufruf
members([B1,B2,...,Bn],Ys)
wird ein Aufruf member(B1,Ys) und ein rekursiver Unteraufruf
members([B2,...,Bn],Ys)
erzeugt. Per Induktion kann man zeigen, daß daraus wiederumdie Aufrufemember(B2,Ys), . . . , member(Bn,Ys) erzeugt werden.
Für feste Listenlängen könnte manmembers/2 also wie folgtimplementieren:
members([B1,...,Bn], Ys) :-
member(B1, Ys), ..., member(Bn, Ys).
Die foreach–do–Schleife hat denselben Effekt.
Prof. Dr. Dietmar Seipel 292
Logik für Informatiker Wintersemester 2012/13
Innerhalb desfindall/3 wird jede RegelRule ausProgram zunächst
mittelsparse_rule/2 in Kopf und Rumpf zerlegt, und dann wirdBody
so instanziiert, daß alle instanziierten Rumpfatome inInt_1 liegen.
?- Rule = [anc(X,Y)]-[par(X,Z),anc(Z,Y)],
parse_rule(Rule, [A]-Body),
Int_1 = [ par(a,b), par(b,c), par(c,d),
anc(b,c), anc(b,d), anc(c,d) ],
members(Body, Int_1).
X=a, Y=c, Z=b, A=anc(a,c), Body=[par(a,b),anc(b,c)] ;
X=a, Y=d, Z=b, A=anc(a,d), Body=[par(a,b),anc(b,d)] ;
X=b, Y=d, Z=c, A=anc(b,d), Body=[par(b,c),anc(c,d)]
Nach dem Aufruf vonparse_rule/2 ist Body=[par(X,Z),anc(Z,Y)].
Erst durch den Aufruf vonmembers/2 wird Body weiter gebunden.
Prof. Dr. Dietmar Seipel 293
Logik für Informatiker Wintersemester 2012/13
Dies instanziiert auch den KopfA der Regel zu einer Hyperresolvente.
Über Backtracking werden für alle Regeln alle Hyperresolventen gefunden.
hres/3 berechnet durch Kombination derpar–Fakten und der
anc–Fakten aus der InterpretationInt_1 eine neue InterpretationInt_2:
?- Program = [
[anc(X, Y)]-[par(X, Z), anc(Z, Y)] ],
Int_1 = [
par(a, b), par(b, c), par(c, d),
anc(b, c), anc(b, d), anc(c, d) ],
hres(Program, Int_1, Int_2).
Int_2 = [ anc(a, c), anc(a, d), anc(b, d) ]
Prof. Dr. Dietmar Seipel 294
Logik für Informatiker Wintersemester 2012/13
Theorem 2.1 (Charakterisierung von Herbrand–Modellen)
SeiP ein DATALOG–Programm undI eine Herbrand–Interpretation vonP .
I ist ein Herbrand–Modell vonP , g.d.w. giltHres(P, I) ⊆ I.
Beweis:
“⇐” SeiI eine Herbrand–Interpretation vonP mit Hres(P, I) ⊆ I.
SeiA← β eine Grundinstanz einer Regel ausP mit I |= β.
Dann giltA ∈ Hres(P, I), und wegenHres(P, I) ⊆ I folgt A ∈ I .
Also ist I ein Herbrand–Modell vonP .
“⇒” SeiI ein Herbrand–Modell vonP .
Für jedesA ∈ Hres(P, I) gibt es eine Grundinstanz einer Regel
A← β ausP mit I |= β. DaI ein Herbrand–Modell vonP ist, folgt
sofortA ∈ I . Also gilt Hres(P, I) ⊆ I .
Prof. Dr. Dietmar Seipel 295
Logik für Informatiker Wintersemester 2012/13
Minimales Herbrand–Modell
Für ein DATALOG–ProgrammP kann man folgendes zeigen:
1. Jedes Herbrand–Modell mußHres∗(P ) enthalten.
2. Hres∗(P ) ist ein Herbrand–Modell:
Hres(P,Hres∗(P )) ⊆ Hres∗(P ).
Also istHres∗(P ) das eindeutige minimale Herbrand–Modell vonP .
Wir bezeichnen es mitMP .
EinedefiniteRegelA← B1 ∧ . . . ∧Bm besteht aus AtomenA und
B1, . . . , Bm, mit m ∈ IN0. Im Vergleich zu DATALOG gibt es keine
Bedingung für die Vorkommen der Variablensymbole.
Auch beliebige definite LogikprogrammeP (Mengen definiter Regeln)
haben ein eindeutiges minimales Herbrand–ModellMP .
Prof. Dr. Dietmar Seipel 296
Logik für Informatiker Wintersemester 2012/13
Exkurs
Für DATALOG kann das minimale Herbrand–ModellMP = Hres∗(P )
durch Iteration vonhres/3 berechnet werden:
% hres_iteration(+Program, -Interpretation) <-
hres_iteration(Program, Interpretation) :-
hres_iteration(Program, [], Interpretation).
hres_iteration(Program, Int_1, Int_2) :-
writeln(Int_1),
hres(Program, Int_1, Int_3),
sort(Int_3, Int_4),
Int_4 \= Int_1,
!,
hres_iteration(Program, Int_4, Int_2).
hres_iteration(Program, Int, Int).
Prof. Dr. Dietmar Seipel 297