prolog – 与联合范式的推理

2019年8月4日 269次阅读

我有这个代码,我需要将其翻译成CNF(这是为考试做准备,所以不是作业！)：

p,q
r :- q
false :- p , s 
s :- t
t

这是我做的：

p ^ q ^ (r V ~q) ^ (~p V ~s) ^ (s V ~t) ^ t

=  r

我的推理是否正确？

还有一个问题：

You want to query the database with r. What clause, should you add to your database?

我根本不明白这一点.简化后,数据库基本上是r.
r是真的,不是吗？

最佳答案 问题“您想使用r.什么子句查询数据库,是否应该添加到数据库中？”指的是所谓的
refutation proofs.在反驳证据中,不能证明：

 Database |- Query

相反,一个证明：

 Database, ~Query |- f

在经典逻辑中,两者是相同的.所以在你的例子中,你需要证明p ^ q ^(r V~q)^(〜p V~s)^(s V~t)^ t ^ ~r导致矛盾.

再见

编辑14.02.2019：
如果有人对Prolog代码感兴趣,可以将proponal公式转换成CNF,请参见这里https://gist.github.com/jburse/ca8d01e26c7cf176ea65eeb1bf916ea0#file-aspsat-p(第43-87行,需要Prolog Commons列表和ordset),你可以通过调用norm(F,H)将公式F转换为CNF C. ,cnf(H,C).

获得的CNF已经从普通和包含的条款中清除.如果有人对CNF测试用例更感兴趣,请参阅此处http://gist.github.com/jburse/bf99239903847322321fabf6f49a5b84#file-casescls-p,其中包含来自Principia Mathematica的数百个重言式,并且收集了其他十分之一的谬误.

点赞