1

我正在为 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)]，它起作用了。为什么这很重要？

4

1 回答 1

0

我会回答一个问题：你为什么首先使用方括号？

查看 Otter 手册，第 4.3 节，列表符号。方括号用于列表，它是扩展为特殊术语的语法糖。在您的情况下，它扩展到类似

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

为什么 OTTER 不推断 Causes($c2,$c1)？

请注意，分辨率演算并不完整，因为在给定理论中可证明的每个公式都可以通过演算推断出来。这将是非常不可取的！相反，解决方案只是反驳完整的，这意味着如果给定的理论是矛盾的，那么解决方案将找到空子句的证明。因此，即使一个子句C是一组子句的逻辑结果，T也不意味着解析演算可以C从T. 在您的情况下，Causes($c2,$c1)从输入得出的事实并不意味着 Otter 必须派生它。

于 2012-12-13T16:24:00.553 回答