用CNF表示知识库并在prolog中解析

Question

我有一个CNF的知识库，我想用prolog来做一个解决方案，但是我无法思考如何在prolog中解决这个问题。

我有过

KB = { P v Q, Q => (R ^ S), (P v R) => U }

我把CNF作为：

KB = { P v Q, not(Q) v R, not(Q) v S, not(P) v U, not(R) v U }

我想证明KB包含U ( KB |= U )。

我可以通过反驳来手动证明，但是我想知道如何使用prolog来完成这个任务？

Thx

Answer 1

答案是:这是不可能的。

not(Q) v，not(Q) v，not(P) v，not( R ) v

可以用r:-q.，s:-q.，u:-p.和u:-r.来表达。

质疑? u.就等于通过反驳来要求证据。

然而，

P v q

不能将表示为prolog程序中的事实/规则。Prolog仅限于霍恩子句，即最多包含一个正字元的文字的中断。