Database Reference
In-Depth Information
9.4
Fixpunktsemantik logischer Programme
Wahrend wir in Abschnitt 9.1 die Semantik logischer Programme modelltheore-
tisch uber den Begriff der korrekten Antwortsubstitutionen definiert haben, liefert
die SLD-Resolution in Abschnitt 9.3.1 eine operationale Semantik. Aus der Korrekt-
heit und Vollstandigkeit der SLD-Resolution folgt die Aquivalenz beider Semanti-
ken. In diesem Abschnitt wollen wir noch kurz die Fixpunktsemantik fur logische
Programme vorstellen, die ebenfalls aquivalent zur modelltheoretischen und zur
operationalen Semantik ist.
Zu einem logischen Programm
auftretenden Funk-
tions- und Pradikatensymbole. Die Menge der Grundterme uber Σ wird auch als
das
Herbranduniversum
bezeichnet. Die
Herbrandbasis
P
sei Σ die Menge der in
P
H
(
P
)von
P
ist die Menge
aller Grundatome uber Σ. Jede Teilmenge M
⊆H
(
P
)isteine
Herbrandinterpreta-
tion
von
P
; M ist ein
Herbrandmodell
, falls M
|
=
Σ
P
gilt.
M
(
P
) bezeichnet die
Menge aller Herbrandmodelle von
.Fur Herbrandmodelle gilt die
Schnitteigen-
schaft
: Der Durchschnitt zweier Herbrandmodelle ist wieder ein Herbrandmodell,
P
und
M
(
P
)
∈M
(
P
)istdas
kleinste
Herbrandmodell von
P
.
Der Operator T
P
ist auf
H
(
P
) definiert durch
A
∈
T
P
(M )
gdw.
es gibt eine Klausel H
←
B
1
,...,B
n
. in
P
und eine Substitution σ,sodass
A = σ(H) und
{
σ(B
1
),...,σ(B
n
)
}⊆
M
Man kann leicht zeigen, dass T
P
ein monotoner Operator ist. Fur alle mono-
tonen Operatoren F auf Mengen definieren wir die wiederholte Anwendung von F
wie folgt:
F
↑
0:=
∅
F
↑
(k +1) := F (F
↑
k)
(k
∈ N
)
:=
k∈
N
F
↑∞
F
↑
k
Der kleinste Fixpunkt von F ist
lfp
(F ):=F
↑∞
.Fur ein logisches Programm
P
gilt
lfp
(T
P
)=
M
(
P
)
Der kleinste Fixpunkt von T
P
ist also das kleinste Herbrandmodell von
P
.
Ein Beweis fur das folgende Theorem ist z.B. in [6] zu finden.
Theorem 9.14 (Fixpunktsemantik vs. SLD-Resolution)
Fur jedes logische
Programm
P
und jedes Atom
A
(uber der Signatur von
P
)gilt:
1. Wenn es eine mittels SLD-Resolution berechnete Anwortsubstitution
σ
zu
P
und
←
A.
gibt, dann ist jede Grundinstanz von
σ(A)
in lfp
(T
P
)
enthalten.
2. Wenn
A
∈
lfp
(T
P
)
gilt, dann gibt es eine SLD-Ableitung fur
P
und
←
A
.
Damit ist die Semantik eines logischen Programms
, die durch den kleinsten
Fixpunkt von T
P
definiert wird, aquivalent zur operationalen Semantik der SLD-
Resolution und damit auch zur modelltheoretischen Semantik.
P