如何使用谓词包含（b，l，t）正确地写出空（b，t）-action的效果公理如果桶b在时间t保持l升水，则谓词评估为True。
空（b，t）：在时间t完全清空桶b。在时间t + 1可以看到转移的影响
转移（b，b'，t）：尽可能多的水从桶b转移到桶b'，而不会在时间t溢出任何开始。在时间t + 1可以看到转移的影响。
铲斗1装满水并容纳7升。铲斗2是空的并且容纳3升。目标状态是b2含有1升水。
我会说正确的解决方案是：
to any b,t,l( empty(b,t) -> contains(b,l,t))
这是正确的还是我应该将升的数量设置为l = 5，例如？
对于此问题，不需要显式时间，因此我们将历史记录表示为操作列表。另一方面，您需要明确表示系统的状态，即三个存储桶的当前内容。原因是Prolog数据结构（即术语）一旦创建就无法更改。由于存在许多无意义的术语，因此最好先通过a来定义数据类型 is_type/1 谓词。因为你将在某些时候使用算术（当你从一个水桶倒水到另一个水桶时），我将使用算术约束而不是古代 is/2 谓词。
:- 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).
看起来我们得到了清空水桶的所有可能性（仅此而已:-)）。现在您需要添加从一个桶倒到另一个桶的规则。祝你好运！
（编辑：拼写错误，第二条规则中的错误）
我将离开旧的答案，因为它留下了一些思考的部分（问题是关于仅实现空行动）。只是提供一个完整的实现：
:- 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.
编辑：删除域约束以加速计算（我们从固定状态开始，因此约束将始终被接地并且可以在没有标记的情况下传播）。
我认为答案是：
Empty(b,t) => Contains(b,0,t+1)