Database Reference
In-Depth Information
Definition 3.74 (allgemeinster Unifikator, mgu)
Ein Unifikator μ von s und
t heißt
allgemeinster Unifikator
(engl.
most general unifier, mgu
) wenn es zu jedem
Unifikator σ von s und t eine Substitution σ
mit σ = σ
◦
μ gibt.
Im vorangegangenen Beispiel ist μ ein allgemeinster Unifikator. Man kann zei-
gen, dass es fur unifizierbare Terme auch immer einen allgemeinsten Unifikator gibt.
Da jeder allgemeinste Unifikator bis auf Variablenumbenennung eindeutig bestimmt
ist, spricht man auch von
dem
allgemeinsten Unifikator von zwei Termen.
Bei der Unifikation zweier Literale P (t
1
,...,t
n
) und P (s
1
,...,s
n
) kann man
wie folgt vorgehen: Wir suchen die erste Stelle in beiden Literalen, an denen sich
die beiden unterscheiden. Dies seien t
k
i
und s
k
j
(Unterterme von den t
k
bzw. s
k
).
Ist keine der beiden Terme eine Variable, dann sind die Literale nicht unifizierbar.
Ist einer dieser Terme eine Variable, etwa t
k
i
= x, dann untersuchen wir, ob diese
Variable in s
k
j
vorkommt. Wenn ja, dann sind die Literale nicht unifizierbar. Wenn
nein, ersetzen wir uberall in beiden Literalen x durch s
k
j
. Mit dem Ergebnis verfah-
ren wir wie beschrieben, bis entweder beide Literale gleich sind oder sich als nicht
unifizierbar erwiesen haben.
Selbsttestaufgabe 3.75 (Unifikation)
Welche der folgenden Literalpaare sind
unifizierbar? Bestimmen Sie gegebenenfalls den allgemeinsten Unifikator! (x, y, z
sind wie ublich Variablen, a ist eine Konstante.)
1.
{
P (x, y, y),
P(y, z, a)
}
2.
{
P (x, y, y),
P(f (y),y,x)
}
3.
{P (f (x),a,x),
P(f (g(y))),z,z)}
Selbsttestaufgabe 3.76 (Unifikation)
Bestimmen Sie in jedem der folgenden
Falle, ob die Substitution σ ein Unifikator bzw. sogar ein allgemeinster Unifikator
der Terme t und t
ist:
1. t = f (a, y, g(z)), t
= f (x, f (f (a)),g(f (b)), σ =
{
x/a, y/f (f (a)),z/f(b)
}
2. t = f (y, g(z)), t
= f (x, g(f (b)), σ =
{
x/a, y/a, z/f(b)
}
3. t = f (y, y, g(z)), t
= f (x, f (f (a)),g(f (b)), σ =
}
Sind t und t
in den folgenden Fallen unifizierbar? Bestimmen Sie einen allgemein-
sten Unifikator bzw. begrunden Sie, warum es keinen solchen gibt:
1. t = g(f (x),z), t
= g(y, f(a))
2. t = g(f (x),z), t
= h(y, f(a))
3. t = h(f (a),f(z),g(a)), t
= h(y, f(g(b)),g(y))
{
x/a, y/f (f (a)),z/f(b)
3.6
Der Resolutionskalkul
Wie schon in Abschnitt 3.3.5 erwahnt, geht es im Resolutionskalkul nicht direkt um
das Ableiten einer Formel G aus einer Formel(menge) F . Vielmehr muss hier die zu
beweisende Formel G negiert zu F hinzugefugt und anschließend die Unerfullbarkeit
von F
∧¬
G gezeigt werden. Gelingt dies, so ist damit die logische Folgerung F
|
= G
bewiesen.
