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必须派生它。