如何使用谓词包含（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的量，例如？
对于这个问题，一个明确的时间是没有必要的，所以我们将代表历史的操作列表。另一方面，您需要明确表示系统的状态，即三个桶的当前内容。原因是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).
看起来我们得到排空水桶（仅此而已:-)）的所有可能性。现在您需要添加从一个桶到另一个桶的规则。祝你好运！
（编辑：错别字，错误在第二个规则）
我离开旧的答案，因为它留下一些地方考虑（和问题是关于执行的只是空的动作）。只需提供一个全面实施过：
:- 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）。
至少对于Prolog来说，你的问题没有意义。尝试用编程语言来形式化，以获得线索。 – CapelliC
也许你应该先解释一下，b，t和l代表什么，规则应该做什么。假设t是一个时间点，b代表一个桶，l代表一个水量（单位为升），你声明：“如果在某点t，任何桶都是空的，那么任何桶都有任意数量的水”。但是你的公理的一个例子是“在时间t，如果桶b是空的，那么桶b包含100升水。”这是一个矛盾。既然矛盾的公理证明了什么，你就不应该使用它们。 –
@ CapelliC @ lambda.xy.x更新了问题以便更好地理解。 – Mensch