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

html5 • • 问答

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

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

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

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

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

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

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

回答

是完整性约束。

虽然在更基于解析的定理证明器中可利用，但您不能在 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)).

在这种情况下，没有。

  • @LiDanyuan Why are there no integrity constraints? Because they do not fit into Prolog's processing principle., which is very "goal directed" and is strongly biased towards "programming" rather than "theorem proving". You would need some kind of general supervisor that gets triggered whenever new facts are labeled true during proof search that cannot be true at the same time. That's rather costly and makes the "programming" part much less attractive.
  • @LiDanyuan I see Wikipedia is classifying the `FALSE <- BODY` clause also as Horn. I would rather not do that. `FALSE <- BODY` is a confusing way of expressing that your query (or goal) is the `BODY`, or in other words, in the higkly idealistic setting of classical logic, that if you add `FALSE <- BODY` to your program, you can derive a logical contradiction (by resolution refutation), and thus BODY must be true. But nobody thinks like that...
  • But yes, apparently this falls under "Horn Clause": [The Semantics of Predicate Logic as a Programming Language](http://www.doc.ic.ac.uk/~rak/papers/kowalski-van_emden.pdf)
以上是不知道能不能用Prolog做解析推理的全部内容。
THE END
分享
二维码
< <上一篇
下一篇>>