我以前从未使用过 clgo，而且我发现在线文档不完整（我也无法在 Potassco 论坛上发帖）。我有一段带有格式规则行的 cligo 代码
foo(L1, L2, L3) :- isa(thing,object), isa(thing, object)...
这部分代码是有道理的，但在最后一条规则之前的行尾，我的条件是 1>0、1<0 或 1==-1。我不确定它们是什么意思，因为它们似乎不遵循正常的布尔规则。有谁知道这在 clgo 中具体意味着什么？
问问题
300 次
1 回答
1
假设您使用的是 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 行矛盾，所以答案不令人满意。
显然，如果没有给出实际行，我无法告诉您任何细节，但布尔值确实以与传统编程语言相同的方式解析。
我希望这有帮助！
于 2019-04-10T12:29:02.300 回答