序言，以合取範式

我有這樣的代碼，我需要轉化爲CNF（這是在準備考試，所以沒有一門功課！）：序言，以合取範式

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

這裏就是我所做的：

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

= r

我的推理是否正確？

這裏有一個問題：

要查詢與R上的數據庫。什麼條款，你應該添加到您的數據庫？

我完全不理解這一點。簡化後的數據庫基本上是r。 r是真的，不是嗎？

在序言多個條款通常是指一個「OR」的關係，所以我想你會想，'（P^Q）V（R V〜Q）...'。然而，目前還不清楚這就是你的表達式列表，因爲它們並不是所有的Prolog子句都是正確的，並且不會在一段時間內結束。 – lurker 2014-11-04 11:22:33

如果你有足夠的時間，我建議你看看SICStus，SWI和其他的'library（clpb）'。 – false 2014-11-04 14:51:41

問題「你想用r。查詢數據庫哪個子句，你應該添加到數據庫中嗎？」指的是所謂的駁斥證明。在反駁證明一個沒有證明：

Database |- Query

而是一個證明：

Database, ~Query |- f

在經典邏輯兩者是相同的。因此，在你的例子中，你需要證明p^q ^（r V〜q）^（〜V〜s）^（s V〜t）^ t ^〜r導致矛盾。

再見

2015-08-18 09:31:12

回答