我想知道我是否可以使用 Prolog 进行归结推理

Question

我对数理逻辑很陌生，最近想学习Prolog，不知道能不能用Prolog做归结推理，比如做如下推理：

我想要实现的是编写如下代码：

eatgrass(X) :- sheep(X).
false       :- deadsheep(X), eatgrass(X).
sheep(X).
deadsheep(X).

并在查询

时得到查询答案'false'

?- sheep(a),deadsheep(a).

似乎在 Prolog 中我无法实现类似第 2 行的内容：

false :- deadsheep(X), eatgrass(X).

所以我想知道是否有办法在 Prolog 中进行上述推理，谢谢！

Answer 1

false :- deadsheep(X), eatgrass(X).

是完整性约束。

虽然可以在更基于分辨率的定理证明器中利用，但不能在 Prolog 中使用它，因为它不是子句（既不是定子句，又名 Horn 子句，即正文中没有否定，也不是一般子句，即正文中有 'negation as failure'）。

（例如，1981 年的 Markgraf Karl Resolution Theorem Prover 确实可以处理完整性约束）

完整性约束可以在答案集编程系统中找到，它以与 Prolog 完全不同的方式找到逻辑程序的解决方案：不是通过 SLDNF 证明搜索，而是通过寻找集合作为程序模型的基本事实（即使程序的每个语句为真）。

你用

编程

sheep(X), deadsheep(X). 没有意义（因为它说“一切都是绵羊”和“一切都是死羊”），但如果您将其更改为：

eatgrass(X) :- sheep(X).
false       :- deadsheep(X), eatgrass(X).
sheep(flopsy).
deadsheep(flopsy).

那么这个程序就是一种问法：是否有一组基于eatgrass/1、sheep/1、deadsheep/1的基原子（逻辑意义上的）是一个模型对于程序，即程序的每个语句都为真？

嗯，没有，因为我们需要

sheep(flopsy).
deadsheep(flopsy).

为真，显然 eatgrass(flopsy) 也需要为真，这违反了完整性约束。

您可以将完整性约束作为查询的一部分进行测试：

程序：

eatgrass(X) :- sheep(X).
sheep(flopsy).
deadsheep(flopsy).

查询：是否有一只羊X使得X既不吃草又不死？

?- sheep(X),\+ (deadsheep(X),eatgrass(X)).

在这种情况下，没有。

Answer 2

正如@David Tonhofer 所建议的，完整性约束可以在 Answer Set Programming systems 中找到，我发现 potassco's clingo 是解决我的问题的好工具，所以我把示例代码放在这里以备不时之需类似的：

eatgrass(X) :- sheep(X).
            :- deadsheep(X), eatgrass(X).
sheep(shawn).
deadsheep(shawn).

第二行是clingo支持的完整性约束，如果你运行这个程序使用clingo online，clingo会告诉你这是不可满足的，这表明推理是正确的.

I wonder if I can use Prolog to do resolution reasoning