真相维护系统的Prolog实现

Question

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

一个很好的例子看起来像这样（这是不是序言）：

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

我根本不知道如何实现这一点。我不知道如何具体表示模态运算符M（符合）。显然，我可以创建谓词 good_student/1、study_hard/1 和 party_person/1。 study_hard/1 到 good_student 和 ¬study_hard 的链接也是我迷路的地方。

这引出了我的问题：有人知道如何在 prolog 中实现类似的东西吗？

提前致谢。

Answer 1

您知道 Prolog 支持一阶逻辑的子集。你不能使用任意的逻辑句子，甚至不能使用从句，而是使用明确的从句。现在，在该程序中，您有两件事不受支持：子句头部的否定和模态运算符。 如果 M 是我所理解的，则从您的评论中可以看出它是失败的否定。您可以在 Prolog 中免费使用它作为默认否定（\+ 或 not）。对于头脑中的否定，您有两种方法：

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

祝你好运。