真理维护系统的Prolog实现

Question

真理维护系统(TMS)存储推理的正当性，从而在给定的知识库中得出特定的结论。

下面是一个很好的例子(这不是prolog)：

∀ X good_student(X) ∧ M study_hard(X) → study_hard (X)
∀ Y party_person(Y)  → ¬study_hard (Y)
good_student(pat)

我根本想不出如何实现这一点。我不知道如何具体地表示模态运算符M(与之一致)。显然，我可以创建好_study/1、study_hard/1和party_person/1的谓词。学习_hard/1与good_student和¬study_hard的链接也是我迷路的地方。

这就引出了我的问题:有人知道如何在prolog中实现这样的东西吗？

提前谢谢。

Answer 1

您知道，Prolog支持一阶逻辑的子集。你不能用任意的逻辑句子，甚至不能用从句，而是要用定句。现在，在这个程序中，您有两个不受支持的东西:一个子句头上的否定和一个情态运算符。如果M是我从你的评论中理解的，那就是否定为失败。在Prolog中，作为默认否定(\+或not)是免费的。对于头脑中的否定，您有两种方法：

1. 你可以尝试用逻辑变换推导出由定句构成的逻辑等价理论。我太懒了，现在不能试这个，但你可以试一试。
2. 嘿，你不是第一个想用否定的人。有不同的框架来处理这个问题。Abductive编程系统可以处理完整性约束，并且可以给您这种否定，也可以免费使用其他模态运算符。更好的是，尝试答案集编程。许多ASP解决程序可以处理您的程序。

祝好运。