math - 不知道能不能用Prolog做解析推理

Question

我对数理逻辑很陌生，最近正在尝试学习 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).

并在查询时获得查询答案“假”

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

似乎在 Prolog 中我无法意识到类似第 2 行的内容:

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

所以我想知道是否有办法像 Prolog 中提到的那样进行推理，谢谢!

Answer 1

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

是完整性约束。
虽然在更基于解析的定理证明器中可利用，但您不能在 Prolog 中使用它，因为它不是一个子句(既不是一个确定的子句，又名。Horn 子句，即在正文中没有否定，也不是一般子句，即带有 'negation as失败'在体内)。
(例如，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)).

在这种情况下，没有。