我想知道我是否可以使用 Prolog 进行解析推理

Question

我对数理逻辑非常陌生，最近正在尝试学习 Prolog，不知道是否可以使用 Prolog 进行解析推理，例如，进行以下推理：

1. 知道∀x.(sheep(x)→eatgrass(x))
2. 知道 ∀x.(deadsheep(x)→¬eatgrass(x))
3. 证明∀x.(deadsheep(x)→¬sheep(x))

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

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 子句，即在正文中没有否定，也不是一般子句，即带有'否定作为失败'）。

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

完整性约束可以在 Answer Set Programming 系统中找到，它以与 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 所建议的，完整性约束可以在答案集编程系统中找到，我发现potassco's clingo 是解决我的问题的好工具，所以我将示例代码放在这里以防有人可能需要类似的代码：

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

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