prolog 一阶逻辑答案

【问题标题】：prolog first order logicprolog 一阶逻辑
【发布时间】：2012-09-20 09:05:57
【问题描述】：

我正在尝试找到一种方法将以下一阶逻辑表达式放入 Prolog：

(p(0) or p(1)) and not (p(0) and p(1))

这意味着它应该以下列方式响应查询：

?- p(0)
Yes.
?- p(1)
Yes.
?- p(0),p(1).
No.

我试图翻译逻辑表达式：

(p(0) or p(1)) and not (p(0) and p(1)) <=>
(not p(0) -> p(1)) and (p(0) -> not p(1)) <=>
p(0) <-> not p(1)

使用 Clarks 补全（这表明每个定义理论都可以通过给出 if-halves 放入一个逻辑程序中），我可以获得：

p(0) :- not p(1).

不幸的是，这个由此产生的理论只是合理的（它不会推导出错误的信息），而不是完整的（例如：p(1) 无法推导出）。这是克拉克定理的结果。

有人知道是否有更好的解决方案吗？谢谢！

【问题讨论】：

您的语言的语义是什么？是“不矛盾”吗？ “可证明”？当你说p(0)时，你是问系统，还是告诉系统？是否所有未指定的东西都被假定为假（就像在 Prolog 的封闭世界中一样）或者它可以具有任何价值？
我使用的语义是Clark´s Completion。查询的逻辑含义是：“是可证明的”，所以?- p(0)相当于问p(0)是否可以从理论上证明。

【解决方案1】：

这很微妙，但实际上你错了。你不应该期望 p(0) 是必然的。蕴含要求 p(0) 在该理论的所有模型中都为真。但是这个理论有两个模型{p(1)}和{p(0)}。

这在文学作品中得到了广泛的研究。正如您正确指出的那样，克拉克的完成无法处理这些情况。更糟糕的是，SLDNF 陷入无限递归

p(0) :- not p(1). 
p(1) :- not p(0).

对于你的理论的确定从句，哪个是最合适的翻译。

我会为您提供有关不同语义定义的指导，但如果您想要一个快速实用的解决方案，我建议您切换到答案集编程。

这是我最喜欢的求解器的链接（该指南也很好，而且是独立的）： http://www.cs.uni-potsdam.de/clasp/

享受吧！

【讨论】：

谢谢！但我不认为我错了，你认为我到底错在哪里？其实一周前我就决定改用 ASP 了，太好了！
我指的是期望 p(1) 和 p(0) 是您的理论的结果。这仅在“勇敢”语义下才是正确的，而不是在 Prolog 的“怀疑”自然语义下。
谢谢，我想我现在明白了。 p(0) 和 p(1) 不是我的理论的结果，因为它们并非在所有模型中都是正确的（持怀疑态度）。相反，它们仅在某些模型中是正确的（勇敢）。

【解决方案2】：

在Prolog中，如果p(0)和p(1)都成功，那么p(0),p(1)不能失败。

这意味着您必须构建自己的小型解释器，设计方法来表示您的目标和规则，并在其中提出您的问题，例如

?- is_true( (p(0),p(1)) ).

【讨论】：

我明白你在说什么，但为什么它成立？
我的意思是它是一个查询，在一个假设的评估器/谓词is_true 中，它将实现您的语义。它会回复，例如Yes 或 No。我认为其他人在这里更具体地回答了您的问题；也尝试询问他们（在答案下方添加评论，以便答案的作者收到）。 :)

【解决方案3】：

逻辑上，已经在命题逻辑中，它不遵循 (A v B) |- A 并且两者都没有（A v B）|- B。情况也没有改变如果您添加〜（A＆B）。

现在的问题是 clark 补全或其他东西是否可以添加更多默认值信息，所以我们最终得到 T |- A 和 T |- B。但是按照逻辑我们然后会有 T |- A&B。

所以我猜在正常情况下这是不可能的，你想做什么。

再见

P.S.：不正常的设置是例如使用轻信结果关系而不是怀疑的结果关系。怀疑的后果关系是：

T |- A iff forall M (if M |- T then M |- A)

轻信的后果关系是：

T |~ A iff exists M (M |- T and M |- A)

可以有 T |~ A 和 T |~ B，但不能有 T |~ A&B，你的 (A v B) & ~(A & B) 没有任何默认信息已经是这样一个理论。

P.S.S.：有一些方法可以滥用 Prolog 系统来轻信推理，尽管 Prologs 的基础是怀疑推理。这诀窍是使用恒等式 T |~ A = ~(T |- ~A)。

但在将其应用于您的示例之前，必须先解决 Prolog 中表示析取的问题。一些析取可以通过以下身份和hypothetical reasoning实现：

(A v B -> C) == (A -> C) & (B -> C)

【讨论】：

我能理解的唯一意义是，如果我们将 OP 给出的响应解释为“不矛盾”或“一致”。因此，声称A 与知识K 即(A v B) ^ ~(A ^ B) 一致，声称B 也是如此，但不是同时声称A ^ B 。但 Prolog 的语义是“蕴含”或者“可证明”，而不是“一致”。
内涵和一致性是相关的。 T |- A 等价于 T，~A 不一致。但你是对的，在非正常设置中，我们可以有 T |- A 和 T |- B 但不是 T |- A&B。查看新的编辑。

【解决方案4】：

如果您的“目标”逻辑中允许引入命名术语，您可以实现一个虚拟 t/0：

t :- p(0), p(1), !, fail.
t :- p(0).
t :- p(1).

如果我们两者都有

p(0).
p(1).

t/0 会失败。

【讨论】：