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

Posted 2023-05-08

【中文标题】我想知道我是不是可以使用 Prolog 进行解析推理

【英文标题】：I wonder if I can use Prolog to do resolution reasoning我想知道我是否可以使用 Prolog 进行解析推理

【发布时间】：2021-07-03 00:19:12

【问题描述】：

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

知道∀x.(sheep(x)→eatgrass(x)) 知道 ∀x.(deadsheep(x)→¬eatgrass(x)) 证明∀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 中提到的推理，谢谢！

【参考方案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)).

在这种情况下，没有。

【讨论】：

@LiDanyuan 为什么没有完整性约束？因为它们不符合 Prolog 的处理原则，它非常“目标导向”，并且强烈偏向于“编程”而不是“定理证明”。您将需要某种通用主管，只要在证明搜索期间将新事实标记为真而不能同时为真，就会触发该主管。这相当昂贵，并且使“编程”部分的吸引力大大降低。

感谢您的回答！如果我可以问，为什么'假：- deadsheep（X），eatgrass（X）。不是 Horn 子句，正如我可以在 Wiki en.wikipedia.ahau.cf/wiki/Horn_clause 上找到的那样，在我看来，这是一个没有正面文字的 Horn 子句，有时被称为目标子句。

@LiDanyuan 我看到***将FALSE <- BODY 子句也归类为Horn。我宁愿不那样做。 FALSE <- BODY 是表达您的查询（或目标）是 BODY 的一种令人困惑的方式，或者换句话说，在经典逻辑的高度理想主义设置中，如果您将 FALSE <- BODY 添加到您的程序中，您可以推导出逻辑矛盾（通过决议驳斥），因此 BODY 必须为真。但是没有人会这样想……

但是是的，显然这属于“喇叭条款”：The Semantics of Predicate Logic as a Programming Language

缺少括号，我认为应该是sheep(X),\+( (deadsheep(X),eatgrass(X)) ).

【参考方案2】：

正如@David Tonhofer 所建议的，完整性约束可以在答案集编程系统中找到，我发现potassco's clingo 是解决我的问题的好工具，所以我将示例代码放在这里以防有人可能需要类似的代码：

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

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