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
Search WWH ::




Custom Search