Database Reference
In-Depth Information
P|
=
∃
x
1
...
∃
x
r
(B
1
∧
...
∧
B
n
)
(9.2)
gilt, wobei x
1
,...,x
r
die in B
1
,...,B
n
auftretenden Variablen sind. Mit dem De-
duktionstheorem gilt die Beziehung (9.2) genau dann, wenn
P⇒∃
x
1
...
∃
x
r
(B
1
∧
...
∧
B
n
)
allgemeingultig ist. Diese Implikation wird im logischen Programmieren
konstruktiv
in dem Sinne bewiesen, dass dabei Terme t
1
,...,t
r
konstruiert werden, die als Be-
legungen oder
Zeugen
(
witness
)fur die existenzquantifizierten Variablen x
1
,...,x
r
diese Formel allgemeingultig machen.
Definition 9.2 (Antwortsubstitution, korrekte Antwortsubstitution)
Sei
P
ein logisches Programm und G die Anfrage
←
B
1
,...,B
n
. mit den Variablen
x
1
,...,x
r
.Eine
Antwortsubstitution
fur
P
und G ist eine Substitution σ mit
Definitionsbereich dom(σ)
⊆{
x
1
,...,x
r
}
. σ ist eine
korrekte Antwortsubstitution
genau dann, wenn die Formel
P⇒∀
y
1
...
∀
y
r
σ(B
1
∧
...
∧
B
n
)
allgemeingultig ist, wobei y
1
,...,y
r
die in σ(B
1
∧
...
∧
B
n
) auftretenden Variablen
sind.
Im Bildbereich einer korrekten Antwortsubstitution konnen also durchaus noch
Variable auftreten. Aus der Definition folgt unmittelbar, dass
jede
Instanz einer
korrekten Antwortsubstitution wieder eine korrekte Antwortsubstitution ist.
Definition 9.3 (korrekte Antwort)
Fur ein logisches Programm
und eine An-
frage G ist eine
korrekte Antwort
entweder eine korrekte Antwortsubstitution σ -
Sprechweise: Die Anfrage G
gelingt
(mit σ)-oderdieAntwort“
no
”, falls
P
P |
=
∃
x
1
...
∃
x
r
(B
1
∧
...
∧
B
n
)
gilt - Sprechweise: Die Anfrage G
scheitert
.
Beispiel 9.4 (Antwortsubstitution)
In Abbildung 9.1 sind fur verschiedene
Programme und Anfragen die korrekten Antworten angegeben. Fur das Programm
P
4
gibt es auf die Anfrage
←
Weg(a,c).
genau eine korrekte Antwortsubstitution,
namlich die identische Substitution
id
=
←
Weg(c,a).
gibt
es dagegen
keine
korrekte Antwortsubstitution, die einzige korrekte Anwort ist also
“
no
”.
{}
. Auf die Anfrage
P
4
markiert
Kante(x,y)
eine (gerichtete) Kante von
x
nach
y
und
Weg(x,y)
entsprechend einen Pfad von
x
nach
y
.In
Im Beispielprogramm
P
4
gibt es offen-
sichtlichkeinenWegvon
c
nach
a
,daherist
no
die einzig korrekte Antwort auf die
Frage nach einem Weg von
c
nach
a
. Gelingt es einem logischen Programmiersystem
(wie Prolog) nicht, einen Beweis fur ein Atom
A
zu finden, so konnte man dies daher
