2

这是要解决的问题：

如果吉姆不给他的孩子买玩具，那么吉姆的孩子就不会收到圣诞节的玩具。如果吉姆的孩子不写圣诞信，吉姆就不会给他们买玩具。吉姆的孩子们确实收到了圣诞节玩具。” 假设对这个故事的预期解释暗示吉姆的孩子们写了他们的圣诞信。

现在我想将上面的信息编码成规则和事实，以便 clgo 推断吉姆的孩子是否写了这些信。

我写的程序如下：

son(peter,jim).
receive_presents(peter,jim).
-buy_presents(jim,peter) :- son(peter,jim),
                            not write_letters(peter).
-receive_presents(peter,jim) :- not buy_presents(jim,peter).

为简单起见，我只是假设吉姆只有一个名叫彼得的孩子。

在我自己的想法中，答案集的推理过程是：

  1. 所有事实都在答案集中，即son(peter,jim)肯定receive_toys(peter,jim)应该在答案集中。

  2. 既然receive_toys(peter,jim)在答案集中，-receive_presents(peter,jim)就不会在。因此not buy_presents(jim,peter)应该是假的，并且buy_presents(jim,peter)在答案集中。

  3. 因为buy_presents(jim,peter)在答案集中，-buy_presents(jim,peter)所以是假的。并且由于son(peter,jim)在答案集中，not write_letters(peter)将是错误的，并且write_letters(peter)将在答案集中。

所以我认为答案应该是 { son(peter,jim), receive_toys(peter,jim), buy_presents(jim,peter), write_letters(peter)}

因此我们可以得出结论是彼得确实写了这封信。

但是在 cligo 中运行它时，我得到以下信息：

clingo version 5.3.0
Reading from jim.lp
jim.lp:4:29-49: info: atom does not occur in any rule head:
  write_letters(peter)
jim.lp:5:37-60: info: atom does not occur in any rule head:
  buy_presents(jim,peter)
Solving...
UNSATISFIABLE

Models       : 0
Calls        : 1
Time         : 0.001s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.001s

我有点认为 cligo 要求首先在规则中定义每个原子操作。但是在这里我只想推理彼得是否写了这封信，所以我不能自我定义“如果 xxx，那么彼得写这封信”，因为那只是我自己在做推理部分。

如何解决答案集编程中的此类问题？

4

1 回答 1

3

请注意，在经典逻辑p => q中等价于!q => !p. 看起来这个练习是用第二种形式表达的，所以你所要做的就是把它转回第一种形式：

If Jim does not buy toys for his children, Jim’s children will not receive toys for Christmas

变成

If Jim’s children do receive toys for Christmas, then Jim did buy toys for his children

第二条规则：

If Jim’s children do not write their Christmas letters, Jim will not buy them toys

变成

If Jim did buy toys for his children, Jim’s children did write their Christmas letters

所以程序将是：

jim_did_buy_toys :- children_do_receive_toys.
children_did_write_their_christmas_letters :- jim_did_buy_toys.
children_do_receive_toys.

显然，该练习的目标是表明，这种“反事实”推理可以通过简单地用经典逻辑法则“消除”任何否定来编码，避免了找出使用哪种否定的所有麻烦。

于 2018-11-29T03:27:55.297 回答