公式化效應公理

Question

如何使用謂詞包含（b，l，t）正確地寫入空（b，t） - 動作的效應公理包含（b，l，t）謂詞評估爲真，如果桶b在時間t持有l升水。 （b，t）：在時間t完全清空桶b。 （b，b'，t）：儘可能多地從桶b向桶b'輸送水，而不會在時間t開始溢出任何開始。在時間t + 1處可見轉移的影響。轉移的影響在時間t + 1可見。

桶1裝滿水並容納7升。桶2是空的並且容納3升。目標狀態是b2包含1升水。

我要說的是正確的解決方案是：

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

將這個是正確或我應該設置升爲L = 5的量，例如？

Answer 1

我想答案應該是：

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

Answer 2

對於這個問題，一個明確的時間是沒有必要的，所以我們將代表歷史的操作列表。另一方面，您需要明確表示系統的狀態，即三個桶的當前內容。原因是Prolog數據結構（即術語）一旦創建就無法更改。由於存在許多無意義的術語，因此首先通過is_type/1謂詞定義數據類型是一種好的做法。因爲你會在某個時候使用算術（當你從一個桶倒水到另一個桶時），我將使用算術約束而不是古代的謂詞。

:- use_module(library(clpfd)). 

首先我們規定有3個桶，由原子B1，B2和B3表示：

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

然後，我們需要定義我們的狀態。我們只用一個術語buckets/3，其中第一個參數擁有b1的容量，其他兩個同樣適用。

is_state(buckets(X,Y,Z)) :- 
    % each bucket contains at least 0 liters 
    [X,Y,Z] ins 0 .. sup. 

所有的容器可能不會變爲負值，所以我們將它們的域設置爲從零到（正）無窮大的範圍。

現在有什麼行動？到目前爲止，您所描述的排空和澆注：

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

清空一個桶，我們只需要知道是哪一個。如果我們把水倒入另一個，我們需要描述兩者。既然我們已經有一個謂語描述一個桶，我們可以只陳述一個規則是「如果From和To是水桶，然後pour(From, To)是一個動作。

現在我們需要解釋一個動作是如何轉變的狀態。這是一箇舊的國家之間的關係，新的狀態，因爲我們想知道發生了什麼，還歷史。

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

初始狀態不會改變任何東西的過渡，並有一個空的歷史（在[] ）。

% 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). 

這個規則可以被解讀爲「如果我們有一個動作，從某些狀態_S0導致狀態buckets(X,Y,Z)一些History來了，那麼我們可以下一個執行empty(b1)行動，我們將達到國家buckets(0,Y,Z)」 。換句話說，狀態被更新並且動作被預先記錄到歷史中。對稱規則適用於其他存儲桶：

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). 

我們如何檢查這是否有意義？讓我們來看看長度爲2的歷史：

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

該多好啊，如果這兩個動作是empty(b1)，第一桶是空的，其他不變。讓我們來看看進一步的解決辦法：

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). 

看起來我們得到排空水桶（僅此而已:-)）的所有可能性。現在您需要添加從一個桶到另一個桶的規則。祝你好運！

（編輯：錯別字，錯誤在第二個規則）

Answer 3

我離開舊的答案，因爲它留下一些地方考慮（和問題是關於執行的只是空的動作）。只需提供一個全面實施過：

:- 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). 

爲了找到答案，如果我們能找到恰好與一個升斗，我們可以公平地枚舉所有的歷史：

?- 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)], 
[...]. 

而只是爲了檢查謂語是可逆的：

?- 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. 

編輯：刪除域名的限制，加快計算（我們先從一個固定的狀態，這樣的限制將永遠是地面，可以在不labeli傳播NG）。