序一阶逻辑

Question

我正在尝试找到一种将以下一阶逻辑表达式放入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））。这是克拉克斯定理的结果。

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

Answer 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/

享受！