OTTER推論

Question

我正在寫OTTER輸入文件，這是非常簡單的：

set(auto). 

formula_list(usable). 

all x y ([Nipah(x) & Encephalitis(y)] -> Causes(x,y)). 
exists x y (Nipah(x) & Encephalitis(y)). 

end_of_list. 

我得到這個輸出搜索：

given clause #1: (wt=2) 2 [] Nipah($c2). 
given clause #2: (wt=2) 2 [] Encephalitis($c1). 
search stopped because sos empty 

爲什麼不會OTTER推斷Causes($c2,$c1)？

編輯： 我從[Nipah(x) & Encephalitis(x)]刪除方括號，它的工作。爲什麼這很重要？

Answer 1

我會回答一個問題：爲什麼你首先使用方括號？

看看水獺手冊，第4.3節，列表表示法。方括號用於列表，它是擴展成特殊術語的語法糖。在你的情況下，擴大到像

all x y ($cons(Nipah(x) & Encephalitis(y), $nil) -> Causes(x,y)). 

---

爲什麼不會OTTER推斷原因（$ C2，$ C1）？

請注意，分辨率演算並不完整，因爲每個給定理論中可證明的公式都可以通過演算推斷出來。這將是非常不可取的！相反，分辨率只有反駁完成，這意味着如果給定的理論是 矛盾，那麼該決議將找到一個空子句的證明。因此，即使條款C是一組條款T的合乎邏輯的結果，也並不意味着分辨率演算可以從T導出C。在你的情況下，Causes($c2,$c1)從輸入中得出的事實並不意味着Otter必須派生它。