© 2001
François Bry
Dieses Lehrmaterial wird ausschließlich zur privaten Verwendung
angeboten. Eine nichtprivate Nutzung (z.B. im Unterricht oder eine
Veröffentlichung von Kopien oder Übersetzungen) dieses Lehrmaterials
bedarf der Erlaubnis des Autors.
und liefert dabei als Begründung B einer Antwort alle Formeln aus SW, der Menge des speziellen Wissens, die zum Beweis dieser Antwort beitragen.
Wird das spezielle Wissen SW geändert, dann werden solche Begründungen an diese Änderungen angepaßt, was zu der Bezeichnung "Begründungsverwaltung" geführt hat.
[L1, ..., Ln] ---> K.
mit 1<=n, wobei jedes Li die Gestalt
+Ai oder -Ai hat und die Ai und
K Atome sind. Dabei steht +Ai für ein Atom,
-Ai für ein negiertes Atom. Diese ungewöhnliche symmetrische
Darstellung von positiven und negativen Literalen im Rumpf einer Regel
erleichtert die Implementierung der Begründungsverwaltung.
Ein Basisfaktum F wird dargestellt als:
[] ---> F.
wobei [] als andere Bezeichnung für
true angesehen werden kann. Damit haben beide
Arten von Wissen eine einheitliche syntaktische Darstellung.
F hat eine oder mehrere
"Begründungen". Eine Begründung ist eine Liste aller Fakten, die zur
Herleitung von F beigetragen haben. Ein Faktum zusammen mit
einer Begründung nennen wir ein begründetes Faktum. Die begründeten Fakten
werden in der PROLOG-Datenbank gespeichert durch PROLOG-Fakten der Form
begruendet(F,Begruendung), wobei es mehrere begründete Fakten
für dasselbe F geben kann. Jedes Basisfaktum F,
dargestellt in der Form [] ---> F, führt dabei zu einem
begründeten Faktum begruendet(F,[]).
:- op(1200, xfx, --->), dynamic(begruendet/2).
auswerten :-
(
(Rumpf ---> Kopf),
maplist(plusify, Atome, Rumpf),
beweisen(Atome, Rumpf_Begr),
einfuegen(Atome, Rumpf_Begr, Kopf_Begr),
\+ begruendet(Kopf, Kopf_Begr)
->
assert(begruendet(Kopf, Kopf_Begr)),
auswerten
;
true
).
beweisen(Atome, Begruendung) :-
maplist(begruendet, Atome, Begruendungen),
flatten(Begruendungen, Begruendung).
einfuegen(Atome, Liste, Neue_Liste) :-
append(Atome, Liste, Neue_Liste).
plusify(X, +X).
Das Prädikat maplist(+Pred, ?List1, ?List2) wendet dabei
Pred auf alle aufeinanderfolgenden Paare von Elementen aus
List1 und List2 an; es scheitert, falls
Pred für eines der Paare scheitert.
Mittels diesem Prädikat
kann auch in Prolog ein higher-order-Programmierstil verwendet werden.
Das Prädikat flatten(+List1, -List2) transformiert die Liste
List1, die auch selber wieder Listen als Argumente enthalten kann,
in eine "flache" Liste List2, indem jede Liste rekursiv durch
deren Elemente ersetzt wird.
:- op(1200, xfx, --->), dynamic(begruendet/2), dynamic(anfrage/1).
auswerten(Anfrage) :-
retractall(anfrage(_)),
assert(anfrage(Anfrage)),
hilfs_auswerten(Kopf, Kopf_Begr),
antwort_reicht(Kopf, Kopf_Begr).
hilfs_auswerten(AKopf, AKopf_Begr) :-
(
(Rumpf ---> Kopf),
maplist(plusify, Atome, Rumpf),
beweisen(Atome, Rumpf_Begr),
einfuegen(Atome, Rumpf_Begr, Kopf_Begr),
\+ begruendet(Kopf, Kopf_Begr)
->
assert(begruendet(Kopf, Kopf_Begr)),
(
anfrage(Kopf),
AKopf=Kopf,
AKopf_Begr=Kopf_Begr
;
hilfs_auswerten(AKopf, AKopf_Begr)
)
;
fail
).
beweisen(Atome, Begruendung) :-
maplist(begruendet, Atome, Begruendungen),
flatten(Begruendungen, Begruendung).
einfuegen(Atome, Liste, Neue_Liste) :-
append(Atome, Liste, Neue_Liste).
plusify(X,+X).
antwort_reicht(Atom, Begruendung) :-
anfrage(Atom),
write('Antwort: '), write(Atom), nl,
write('Begruendung: '), write(Begruendung), nl,
write('weiter? (ja./nein.) '),
read(Eingabe),
Eingabe == nein.
hilfs_auswerten/2
generiert durch Rücksetzen mehrere Antworten. Diese Antworten werden
durch das Prädikat anfrage_reicht/2 wieder verbraucht.
fail der
leeren Liste [] und die Disjunktion ';' dem
Paarbildungsoperator '.'.
:- [user].
[] ---> r(a, b).
[] ---> r(b, a).
[+t(X, Y), +t(Y, Z)] ---> t(X, Z).
[+r(X, Y)] ---> t(X, Y).
Yes
:- auswerten(t(a, a)).
Antwort: t(a, a)
Begruendung: [t(a, b), t(b, a), r(a, b), r(b, a)]
weiter? (ja./nein.) ja.
Antwort: t(a, a)
Begruendung: [t(a, b), t(b, a), r(a, b), t(b, a),
t(a, a), r(b, a), t(a, b), t(b, a), r(a, b), r(b, a)]
weiter? (ja./nein.) ja.
Antwort: t(a, a)
Begruendung: [t(a, b), t(b, a), r(a, b), t(b, a),
t(a, a), r(b, a), t(a, b), t(b, a), r(a, b), t(b, a),
t(a, a), r(b, a), t(a, b), t(b, a), r(a, b), r(b, a)]
weiter? (ja./nein.) nein.
Yes
t(a,a) auf
verschiedene Weisen hergeleitet werden kann: aus r(a,b) und
r(b,a), aus r(a,b), r(b,a) und t(a,a),
was wiederum aus r(a,b) und r(b,a) hergeleitet wurde,
usw.
% markierten Zeilen
\+ memberchk(Kopf, Kopf_Begr), %
sort(Zwischen_Liste, Neue_Liste). %
sort/2 hat zur Folge,
daß die Begründungen sortiert sowie Duplikate aus der
Begründung beseitigt werden.
:- op(1200, xfx, --->), dynamic(begruendet/2), dynamic(anfrage/1).
auswerten(Anfrage) :-
retractall(anfrage(_)),
assert(anfrage(Anfrage)),
hilfs_auswerten(Kopf, Kopf_Begr),
antwort_reicht(Kopf, Kopf_Begr).
hilfs_auswerten(AKopf, AKopf_Begr) :-
(
(Rumpf ---> Kopf),
maplist(plusify, Atome, Rumpf),
beweisen(Atome, Rumpf_Begr),
einfuegen(Atome, Rumpf_Begr, Kopf_Begr),
\+ memberchk(Kopf, Kopf_Begr), %
\+ begruendet(Kopf, Kopf_Begr)
->
assert(begruendet(Kopf, Kopf_Begr)),
(
anfrage(Kopf),
AKopf=Kopf,
AKopf_Begr=Kopf_Begr
;
hilfs_auswerten(AKopf, AKopf_Begr)
)
;
fail
).
beweisen(Atome, Begruendung) :-
maplist(begruendet, Atome ,Begruendungen),
flatten(Begruendungen, Begruendung).
einfuegen(Atome, Liste, Neue_Liste_Sortiert) :-
append(Atome, Liste, Neue_Liste),
sort(Neue_Liste, Neue_Liste_Sortiert). %
plusify(X, +X).
antwort_reicht(Atom, Begruendung) :-
write('Antwort: '), write(Atom), nl,
write('Begruendung: '), write(Begruendung), nl,
write('weiter? (ja./nein.) '),
read(Eingabe),
Eingabe == nein.
:- [user].
[] ---> r(a, b).
[] ---> r(b, a).
[+t(X, Y), +t(Y, Z)] ---> t(X, Z).
[+r(X, Y)] ---> t(X, Y).
Yes
:- auswerten(t(a, a)).
Antwort: t(a, a)
Begruendung: [r(a, b), r(b, a), t(a, b), t(b, a)]
weiter? (ja./nein.) ja.
No
:- [user].
[] ---> student(anna).
[] ---> student(berndt).
[] ---> hoert(anna, prolog).
[] ---> hoert(anna, ml).
[+student(X), +hoert(X, prolog)] ---> mag(X, logik).
[+student(X), +hoert(X, ml)] ---> mag(X, logik).
Yes
:- auswerten(mag(X, logik)).
Antwort: mag(anna, logik)
Begruendung: [hoert(anna, prolog), student(anna)]
weiter? (ja./nein.) ja.
Antwort: mag(anna, logik)
Begruendung: [hoert(anna, ml), student(anna)]
weiter? (ja./nein.) ja.
No
[]
dargestellt sind. Die Menge der hergeleiteten Fakten mit ihren
Begründungen soll dann so verändert werden, daß sie der Änderung des
speziellen Wissens entspricht. Dabei will man natürlich die
Berechnungen so weit wie möglich einschränken (sonst könnte man ja
einfach sämtliche hergeleiteten Fakten samt Begründungen ganz neu
berechnen).
In diesem Abschnitt wird angenommen, daß alle Rechtfertigungen monoton sind, d.h. ihre Rümpfe enthalten keine negativen Literale.
Wenn ein Basisfaktum F gelöscht wird, gelten
alle hergeleiteten Fakten nicht mehr, deren Herleitungen Bezug auf
F nehmen. Es müssen also genau diejenigen
begründeten Fakten entfernt werden, deren Begründung
F enthält.
Aus dieser Bemerkung ergibt sich das folgende Programm zur
Aktualisierung eines Reason-Maintenance-Systems nach dem
Löschen eines Basisfaktums F, wobei diese
Änderung -F notiert wird:
aktualisieren(-F) :- retract(([] ---> F)),
retract(begruendet(F, [])),
begruendet(Atom, Begruendung),
memberchk(F, Begruendung),
retract(begruendet(Atom, Begruendung)),
fail.
aktualisieren(_).
Wie zuvor wird das Löschen eines Basisfaktums
F mit -F notiert. Das Einfügen eines
Basisfaktums F wird +F notiert. Das
Einfügen verursacht mehr Arbeit als das Löschen.
Zunächst kann ein hinzuzufügendes Basisfaktum
F schon vorhanden sein. In diesem Fall ist es
angemessen, gar nichts weiter zu tun.
Sonst müssen die Rechtfertigung [] ---> F
sowie das begründete Faktum begruendet(F, []) in
die Prolog-Datenbank hinzugefügt und die vorhandene Menge der
begründeten Fakten aktualisiert werden. Diese Aktualisierung
leistet das Prädikat aenderungen_propagieren/3,
das wiederum als Generator implementiert ist.
aktualisieren(-F) :-
retract(([] ---> F)),
retract(begruendet(F, [])),
begruendet(Atom, Begruendung),
memberchk(F, Begruendung),
retract(begruendet(Atom, Begruendung)),
fail.
aktualisieren(-_).
aktualisieren(+F) :-
(
([] ---> F)
->
true
;
assert(([] ---> F)),
assert(begruendet(F, [])),
aenderungen_propagieren(F, Kopf, Kopf_Begr),
antwort_reicht(Kopf, Kopf_Begr)
).
aenderungen_propagieren(F, AKopf, AKopf_Begr) :-
(Rumpf ---> Kopf),
(
memberchk(+F, Rumpf),
maplist(plusify, Atome, Rumpf),
beweisen(Atome, Rumpf_Begr),
einfuegen(Atome, Rumpf_Begr, Kopf_Begr),
\+ memberchk(Kopf, Kopf_Begr),
\+ begruendet(Kopf, Kopf_Begr)
->
assert(begruendet(Kopf, Kopf_Begr)),
(
anfrage(Kopf),
AKopf=Kopf,
AKopf_Begr=Kopf_Begr
;
aenderungen_propagieren(Kopf, AKopf, AKopf_Begr)
)
;
fail
).
beweisen und einfuegen, negative
Literale -A zu berücksichtigen.
p(a) bei den folgenden
Rechtfertigungen zeigt:
[+p(X), -q(X)] ---> r(X).
[+p(X)] ---> q(X).
p(a) als Basisfaktum hinzugefügt wurde, kann wegen der
ersten Rechtfertigung r(a) hergeleitet werden mit der
Begründung, daß p(a) gilt und q(a) nicht
gilt. Außerdem kann wegen der zweiten Rechtfertigung
q(a) hergeleitet werden, wodurch aber die Begründung für
r(a) ungültig wird.
[] ---> p(a).
[+p(X), -q(X)] ---> r(X).
q(a) zum Löschen
des vorher herleitbaren r(a) führen. Deswegen spricht man
von nichtmonotonen Rechtfertigungen.
[-p] ---> p.
[-p] ---> q.
[-q] ---> p.
p noch q mittels einer
weiteren Rechtfertigung begründet werden, hat diese Regelmenge
zwei stabile Zustände: Entweder p wird als wahr
betrachtet (und damit q als falsch) oder
q wird als wahr betrachtet (und damit p
als falsch).
Letzte Änderung: 18. August 1998
Dabei wird üblicherweise angenommen, daß die Regeln bereichsbeschränkt und die Fakten variablenfrei sind.
Das Beweisverfahren steht im Grunde genommen nicht fest. Oft wird das Vorwärtsschließen angewendet.
In diesem Kapitel behandeln wir Reason-Maintenance-Systeme, die als allgemeines Wissen bereichsbeschränkte Regeln und als spezielles Wissen variablenfreie Fakten voraussetzen. Als Beweisverfahren wird das Vorwärtsschließen angewendet.