prolog - 序一阶逻辑

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/

享受!