Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2...

153
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

Transcript of Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2...

Page 1: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 2: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 3: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 4: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 5: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 6: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 7: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 8: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 9: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 10: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 11: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 12: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 13: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 14: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 15: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 16: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 17: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 18: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 19: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 20: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 21: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 22: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 23: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 24: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 25: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 26: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 27: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 28: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 29: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 30: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 31: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 32: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 33: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 34: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 35: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 36: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 37: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 38: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 39: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 40: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 41: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 42: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 43: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 44: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 45: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 46: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 47: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 48: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 49: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 50: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 51: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 52: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 53: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 54: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 55: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 56: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 57: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 58: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 59: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 60: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 61: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 62: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 63: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 64: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 65: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 66: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 67: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 68: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 69: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 70: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 71: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 72: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 73: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 74: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 75: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 76: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 77: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 78: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 79: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 80: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 81: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 82: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 83: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 84: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 85: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 86: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 87: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 88: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 89: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 90: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 91: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 92: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 93: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 94: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 95: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 96: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 97: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 98: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 99: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 100: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 101: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 102: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 103: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 104: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 105: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 106: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 107: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 108: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 109: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 110: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 111: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 112: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 113: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 114: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 115: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 116: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 117: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 118: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 119: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 120: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 121: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 122: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 123: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 124: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 125: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 126: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 127: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 128: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 129: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

Logik für Informatiker Wintersemester 2012/13

Prof. Dr. Dietmar Seipel 273

Page 130: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 131: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 132: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 133: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 134: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 135: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

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

Page 136: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 137: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 138: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 139: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 140: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 141: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 142: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 143: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 144: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 145: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 146: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 147: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 148: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 149: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 150: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 151: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 152: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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

Page 153: Logik für Informatiker Wintersemester 2012/13 · Logik für Informatiker Wintersemester 2012/13 2 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits

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