时间戳

首页 > 解决方案 > 在 clgo/ASP 中 1<0 和 1=-1 是什么意思？

answer-set-programming - 在 clgo/ASP 中 1<0 和 1=-1 是什么意思？

问题描述

我以前从未使用过 clgo，而且我发现在线文档不完整（我也无法在 Potassco 论坛上发帖）。我有一段带有格式规则行的 cligo 代码

foo(L1, L2, L3) :- isa(thing,object), isa(thing, object)...

这部分代码是有道理的，但在最后一条规则之前的行尾，我的条件是 1>0、1<0 或 1==-1。我不确定它们是什么意思，因为它们似乎不遵循正常的布尔规则。有谁知道这在 clgo 中具体意味着什么？

标签： answer-set-programmingclingogringo

解决方案

假设您使用的是 Clingo 5，则条件应该像正常的布尔条件一样解析。

由于您没有发布确切的行，我只能假设它是以下形式的一行：

atom :- 1 > 0, 1 < 0, 1 = -1.

这条线说

atom 为真，如果：“1 > 0” AND “1 < 0” AND “1 = -1”。

我有一种感觉，混乱的根源在于这条线的解释方式。只有第一个布尔条件为真，其他 2 个为假。但这并不意味着 atom 是错误的：它只是意味着没有证据表明 atom 是正确的。

运行这一行会给我们输出：

Answer: 1

SATISFIABLE

因为没有证据证明原子是真的。

这意味着我们可以有这样的程序：

atom :- 1 > 0, 1 < 0, 1 = -1.
atom :- 1 = 1.

它会有答案：

Answer: 1
atom
SATISFIABLE

第二行提供了 atom 为真的证据，而第一行没有提供 atom 为真的证据。因此，atom 为真，答案可满足。没有矛盾。

在这个程序中：

atom :- 1 > 0, 1 < 0, 1 = -1.
atom :- 1 = 0.

我们得到答案：

Answer: 1

SATISFIABLE

因为这两行都没有提供 atom 是真的证据。没有矛盾，所以答案是满足的，但是只有当有证据证明它是真的时，一个原子才被证明是真的。

在这个程序中：

atom :- 1 > 0, 1 < 0, 1 = -1.
:- atom.

我们得到答案：

Answer: 1

SATISFIABLE

第一行仍然没有提供 atom 为真的证据，但第二行证明它是假的。由于线条并不矛盾，我们再次得到了一个空洞但满意的答案。

最后，我们有程序：

atom :- 1 > 0, 1 < 0, 1 = -1.
atom :- 1 = 1.
:- atom.

哪个有答案：

UNSATISFIABLE

第 1 行没有证明 atom 是真的，第 2 行证明 atom 是真的，第 3 行证明 atom 是假的。第 2 行和第 3 行矛盾，所以答案不令人满意。

显然，如果没有给出实际行，我无法告诉您任何细节，但布尔值确实以与传统编程语言相同的方式解析。

我希望这有帮助！

推荐阅读