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派生できることを意味するわけではありません。あなたの場合、入力から続くという事実は、Otterがそれを導き出さなければならないという意味ではありません。CTCauses($c2,$c1)

于 2012-12-13T16:24:00.553 に答える