Database Reference
In-Depth Information
Beispiel 9.6 (indefinite Antworten) Das “Nicht-Hornklauselprogramm”
P(a)
P(b).
und die Hornanfrage
P(x). seien gegeben. Dann ist die Formel
P(a) P(b) ⇒∃xP(x) .
allgemeingultig, aber es gibt keine Substitution σ,sodassdieFormel
P(a)
P(b)
σ(P (x)) .
allgemeingultig ist.
Fur Hornklauselprogramme gilt jedoch immer, dass eine Hornanfrage gultig ist ge-
nau dann, wenn es eine entsprechende korrekte Antwortsubstitution gibt.
Theorem 9.7 (Existenz korrekter Antwortsubstitutionen) Sei
P
ein Horn-
klauselprogramm und G die Anfrage
B 1 ,...,B n . mit den Variablen x 1 ,...,x r .
Dann ist
B n )
allgemeingultig gdw. es eine korrekte Antwortsubstitution fur
P⇒∃
x 1 ...
x r (B 1
...
P
und G gibt.
Selbsttestaufgabe 9.8 (Hornformeln und definite Antworten) Folgendes
kann man leicht zeigen:
P (a)
xP(x) ist allgemeingultig, aber:
Es existiert kein Term t,sodassP (a)
P (b)
⇒∃
P (b)
P (t) ebenfalls allge-
meingultig ist.
Theorem 9.7 sagt hingegen aus, dass bei Hornprogrammen diese Unbestimmtheit
nicht auftritt, es also immer ein entsprechendes t gibt. Zu P (a)
P (b) kann man
eine intuitiv ahnliche Formel
¬
N (a)
∨¬
N (b) angeben, wobei N als Verneinung von
P gedacht ist. Nun ist
¬
N (a)
∨¬
N (b) eine Hornformel, aber es gilt wiederum:
¬
N (x) ist allgemeingultig, aber:
Es existiert kein Term t,sodass
N (a)
∨¬
N (b)
⇒∃
x
¬
¬
N (a)
∨¬
N (b)
⇒¬
N (t) ebenfalls
allgemeingultig ist.
Ist dies ein Widerspruch zu Theorem 9.7?
Auf die Behandlung disjunktiver Information in logischen Programmen werden
wir noch in Abschnitt 9.10 eingehen.
9.3
Resolution von Hornklauseln
Im Folgenden wollen wir uns damit beschaftigen, wie man Anfragen an ein logisches
Programm mittels SLD-Ableitungen, einem zielorientierten Inferenzverfahren (vgl.
Abschnitt 4.3.3), beantworten und welche Antwortsubstitution man dabei generie-
ren kann.
Search WWH ::




Custom Search