Database Reference
In-Depth Information
3.5.7
Unifikation
Neben der Klauseldarstellung ist das Gleichmachen von Termen durch Instantiie-
rung von Variablen eine weitere essentielle Grundlage fur die Resolution.
Definition 3.72 (Substitution) Eine Substitution σ ist eine (totale) Funktion
σ : Term Σ (V)
Term Σ (V)
die Terme auf Terme abbildet, so dass die Homomorphiebedingung
σ(f (t 1 ,...,t n )) = f (σ(t 1 ),...,σ(t n ))
fur jeden Term f (t 1 ,...,t n ), n
0, gilt und so dass σ eingeschrankt auf V fast
uberall 9 die Identitat ist. Die Menge dom(σ)=
{
x
V
|
σ(x)
= x
}
ist der Definiti-
onsbereich (engl. domain )vonσ.
Jede Substitution σ kann eindeutig durch eine endliche Menge von (Variable, Term)-
Paaren
{
x 1 /t 1 ,...,x n /t n }
reprasentiert werden, wobei dom(σ)=
{
x 1 ,...,x n }
und
σ(x i )=t i gilt.
Die Anwendung einer Substitution σ auf einen Term t ist nun einfach die nor-
male Funktionsanwendung σ(t), da wir hier Substitutionen direkt als Abbildung von
Termen auf Terme eingefuhrt haben. σ(t)heißt Instanz des Terms t; falls σ(t)keine
Variablen enthalt, so heißt σ(t) Grundinstanz von t.Fur σ = {x 1 /t 1 ,...,x n /t n }
erhalt man σ(t), indem man alle Auftreten der Variablen x i in t (fur i =1,...,n)
simultan durch t i ersetzt. Fur die Substitution σ = {x/g(v),y/b} gilt zum Beispiel
σ(f (x, y, z)) = f (g(v),b,z) und σ(h(x, x)) = h(g(v),g(v)).
Fur die Komposition ρ
σ von zwei Substitutionen σ und ρ gilt ρ
σ(t)=ρ(σ(t));
id =
ist die identische oder leere Substitution, fur die id(t)=t fur jeden Term t
gilt. Eine Variablenumbenennung ist eine Substitution, die alle Variablen in ihrem
Definitionsbereich injektiv auf Variablen abbildet. Beispielsweise ist ρ =
{}
{
x/v, y/w
}
eine Variablenumbenennung.
Bei der Unifikation werden Terme durch Variableneinsetzungen gleich gemacht.
Definition 3.73 (Unifikator) Eine Substitution σ heißt Unifikator der Terme s
und t,wennσ(s)=σ(t) gilt; in diesem Fall sind s und t unifizierbar .
Die Begriffe der Substitution und Unifikation konnen von Termen direkt auf Formeln
und Formelmengen ubertragen werden. Insbesondere bei der Resolution werden wir
von der Unifikation von Literalen mit demselben Pradikatensymbol sprechen.
Die Terme f (x, b) und f (a, c) sind nicht unifizierbar, ebensowenig f (x) und
f (g(x)).
Die Substitutionen σ =
sind zwei
Unifikatoren von t 1 = f (x, g(a, y)) und t 2 = f (b, z). Allerdings ist μ allgemeiner als
σ insofern, als dass in σ die Variable y unnotigerweise instantiiert wird und σ(z)
spezifischer ist als μ(z) (d.h. σ(z)entstehtausμ(z) durch Instanzenbildung). Es
gilt offensichtlich σ = σ
{
x/b, y/a, z/g(a, a)
}
und μ =
{
x/b, z/g(a, y)
}
μ mit σ =
{
y/a
}
.
9 Zur Erinnerung: “fast uberall” bedeutet “alle bis auf endlich viele”.
Search WWH ::




Custom Search