在答案集编程中如何表示未知知识？

Question

下面是要解决的问题：

如果吉姆不给他的孩子买玩具，吉姆的孩子们就不会在圣诞节收到玩具。如果吉姆的孩子不给他们写圣诞信，吉姆就不会给他们买玩具。吉姆的孩子们圣诞节确实会收到玩具。“假设这个故事的原意解释意味着吉姆的孩子们写了他们的圣诞信。

现在，我想把上面的信息编码成规则和事实，让克莱戈来解释吉姆的孩子们是否写了这些信。

我编写的程序如下：

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)应该是false，而buy_presents(jim,peter)在答案集中。
3. 因为buy_presents(jim,peter)在答案集中，所以-buy_presents(jim,peter)是假的。由于son(peter,jim)位于应答集中，not write_letters(peter)将为false，而write_letters(peter)将位于应答集中。

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

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

但是，当在clingo中运行这个程序时，我会得到以下信息：

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

我认为clingo要求每个原子操作首先在规则中定义。但在这里，我只想解释一下，如果彼得写了这封信，我就不能自我定义“如果某某，那么彼得写这封信”，因为那只是我自己在做推理的部分。

在答案集编程中如何解决这类问题？

Answer 1

注意，在经典逻辑中，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.

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