Formel-Effekt-Axiom

Question

So schreiben Sie das Effektaxiom für leere (b, t) -Aktion mit dem Prädikat enthält (b, l, t) Das Prädikat liefert True, wenn der Bucket b zum Zeitpunkt t 1 Liter Wasser enthält .

leer (b, t): entleert den Eimer b vollständig zur Zeit t. Die Wirkung der Übertragung ist zum Zeitpunkt t + 1 sichtbar.

Übergabe (b, b ', t): so viel Wasser wie möglich aus dem Eimer b in den Eimer b' übertragen, ohne dass ein Start zum Zeitpunkt t erfolgt. Der Effekt der Übertragung ist zum Zeitpunkt t + 1 sichtbar.

Eimer 1 ist mit Wasser gefüllt und fasst 7 Liter. Eimer 2 ist leer und fasst 3 Liter. Der Zielzustand ist, dass b2 1 Liter Wasser enthält.

Ich würde sagen, dass die richtige Lösung ist:

to any b,t,l(empty(b,t) -> contains(b,l,t)) 

dies richtig wäre, oder sollte stelle ich die Menge an Litern l = 5, zum Beispiel?

Answer 1

Ich denke, die Antwort wäre:

Empty(b,t) => Contains(b,0,t+1) 

Answer 2

Für dieses Problem eine explizite Zeit nicht erforderlich ist, so werden wir die Geschichte als eine Liste von Aktionen darstellen. Auf der anderen Seite müssen Sie den Zustand Ihres Systems, d. H. Den aktuellen Inhalt der drei Buckets, explizit darstellen. Der Grund dafür ist, dass Prolog-Datenstrukturen (d. H. Terme) nicht mehr geändert werden können, sobald sie einmal erstellt wurden. Da es viele bedeutungslose Begriffe gibt, ist es eine gute Methode, Datentypen zuerst über ein Prädikat zu definieren. Da Sie zu einem bestimmten Zeitpunkt Arithmetik verwenden (wenn Sie Wasser von einem Eimer in einen anderen gießen), verwende ich arithmetische Einschränkungen anstelle des alten Prädikats is/2.

:- use_module(library(clpfd)). 

Zuerst wir feststellen, dass es 3 Eimer, durch die Atome b1 dargestellt, b2 und b3:

is_bucket(b1). 
is_bucket(b2). 
is_bucket(b3). 

Dann müssen wir unseren Staat definieren. Wir verwenden nur einen Ausdruck buckets/3, wobei das erste Argument die Kapazität von b1 und ebenso die anderen beiden enthält.

Alle Container dürfen nicht negativ werden, daher setzen wir ihre Domäne auf einen Bereich von Null bis (positiv) unendlich.

Was ist nun eine Aktion? Bisher beschriebene Sie Entleerung und Gießen:

is_action(empty(B)) :- 
    is_bucket(B). 
is_action(pour(From, To)) :- 
    is_bucket(From), 
    is_bucket(To). 

einen Eimer leeren, wir müssen nur wissen, welche. Wenn wir Wasser von einem zum anderen gießen, müssen wir beides beschreiben. Da wir bereits ein Prädikat haben einen Eimer zu beschreiben, können wir nur eine Regel als „Zustand, wenn From und To Eimer sind, dann ist pour(From, To) eine Aktion.

Jetzt müssen wir erklären, wie eine Aktion einen Zustand verwandelt. Dies ist ein Beziehung zwischen dem alten Zustand, der neue Zustand, und weil wir wissen, gerne würden, was auch die Geschichte. geschieht

% initial state 
state_goesto_action(buckets(7,5,3), buckets(7,5,3), []). 

der Übergang für den Anfangszustand ändert nichts und hat eine leere Geschichte (die []).

% state transitions for moving 
state_goesto_action(buckets(X,Y,Z), buckets(0,Y,Z), [empty(b1) | History]) :- 
    state_goesto_action(_S0, buckets(X,Y,Z), History). 

kann diese Regel als gelesen werden: „Wenn wir eine Aktion kommt von einem Zustand _S0 führt zu dem Zustand buckets(X,Y,Z) mit einigen History hatte, dann können wir die empty(b1) Aktion als nächstes durchführen und wir werden den Zustand buckets(0,Y,Z) erreichen“ . Mit anderen Worten, der Status wird aktualisiert und die Aktion wird dem Verlauf vorangestellt. Eine symmetrische Regel funktioniert für die anderen Buckets:

state_goesto_action(buckets(X,Y,Z), buckets(X,0,Z), [empty(b2) | History]) :- 
    state_goesto_action(_S0, buckets(X,Y,Z), History). 
state_goesto_action(buckets(X,Y,Z), buckets(X,Y,0), [empty(b3) | History]) :- 
    state_goesto_action(_S0, buckets(X,Y,Z), History). 

Wie können wir überprüfen, ob dies sinnvoll ist? Lassen Sie uns an Geschichten der Länge aussehen 2:

?- state_goesto_action(_,S1,[H1,H2]). 
S1 = buckets(0, 3, 5), 
H1 = H2, H2 = empty(b1) . 

Ah schön, wenn beide Aktionen empty(b1) sind, ist der erste Eimer leer und die anderen davon unberührt. Lassen Sie uns an weiteren Lösungen suchen:

S1 = buckets(0, 0, 5), 
H1 = empty(b1), 
H2 = empty(b2) ; 

S1 = buckets(0, 3, 0), 
H1 = empty(b1), 
H2 = empty(b3) ; 

S1 = buckets(0, 0, 5), 
H1 = empty(b2), 
H2 = empty(b1) ; 

S1 = buckets(7, 0, 5), 
H1 = H2, H2 = empty(b2) ; 

S1 = buckets(7, 0, 0), 
H1 = empty(b2), 
H2 = empty(b3) ; 

S1 = buckets(0, 3, 0), 
H1 = empty(b3), 
H2 = empty(b1) ; 

S1 = buckets(7, 0, 0), 
H1 = empty(b3), 
H2 = empty(b2) ; 

S1 = buckets(7, 3, 0), 
H1 = H2, H2 = empty(b3). 

Sieht aus wie wir alle Möglichkeiten der Entleerung Eimer (und nichts mehr :-)) erhalten. Jetzt müssen Sie Regeln für das Gießen von einem Eimer zum anderen hinzufügen. Viel Glück!

(Edit: Tippfehler, Fehler in der zweiten Regel)

Answer 3

ich die alte Antwort zu verlassen, weil es einige Teile verläßt, um darüber nachzudenken (und die Frage ist, nur die leere Aktion Umsetzung). Nur eine vollständige Umsetzung zu schaffen, zu:

:- use_module(library(clpfd)). 

bucket_capacity(b1,7). 
bucket_capacity(b2,3). 
bucket_capacity(b3,5). 

% projections to a single bucket 
state_bucket_value(buckets(X, _, _),b1,X). 
state_bucket_value(buckets(_, Y, _),b2,Y). 
state_bucket_value(buckets(_, _, Z),b3,Z). 

% state update relation by a single bucket 
state_updated_bucket_value(buckets(_, Y, Z), buckets(X0, Y, Z), b1, X0). 
state_updated_bucket_value(buckets(X, _, Z), buckets(X, Y0, Z), b2, Y0). 
state_updated_bucket_value(buckets(X, Y, _), buckets(X, Y, Z0), b3, Z0). 


% initial state 
state_goesto_action(S0, S0, []) :- 
    S0 = buckets(X,Y,Z), 
    bucket_capacity(b1,X), 
    bucket_capacity(b2,Y), 
    bucket_capacity(b3,Z). 
% state transition for emptying 
state_goesto_action(S1, S2, [empty(Bucket) | History]) :- 
    state_updated_bucket_value(S1, S2, Bucket, 0), 
    state_goesto_action(_S0, S1, History). 
% state transition for pouring 
state_goesto_action(S1, S3, [pour(From,To) | History]) :- 
    bucket_capacity(b1,Max), 
    state_bucket_value(S1,From,X), 
    state_bucket_value(S1,To,Y), 
    From0 #= min(X+Y, Max), 
    To0 #= max(X-Y, 0), 
    state_updated_bucket_value(S1, S2, From, From0), 
    state_updated_bucket_value(S2, S3, To, To0), 
    state_goesto_action(_S0, S1, History). 

Um herauszufinden, ob wir einen Eimer mit genau einem Liter finden, können wir ziemlich alle Geschichten aufzählen:

?- length(L,_), state_bucket_value(S,_,1), state_goesto_action(_, S, L). 
L = [pour(b1, b3), pour(b1, b2), empty(b1), pour(b1, b3)], 
S = buckets(5, 0, 1) ; 
L = [pour(b1, b3), pour(b1, b2), pour(b1, b1), pour(b1, b3)], 
S = buckets(5, 0, 1) ; 
L = [pour(b1, b3), pour(b1, b2), pour(b2, b1), empty(b1)], 
S = buckets(7, 0, 1) ; 
L = [pour(b1, b3), pour(b1, b2), pour(b2, b1), pour(b1, b1)], 
[...]. 

Und nur zu prüfen, ob die Prädikat ist reversibel:

?- L = [pour(b1, b3), pour(b1, b2), empty(b1), pour(b1, b3)], state_goesto_action(_, S, L). 
L = [pour(b1, b3), pour(b1, b2), empty(b1), pour(b1, b3)], 
S = buckets(5, 0, 1) ; 
false. 

Edit: Entfernte Domain Constraints die Berechnung zu beschleunigen (wir mit einem festen Zustand zu starten, so Zwänge immer geschliffen werden und kann ohne LABÉLI vermehrt werden ng).