λx,z,E.y F(x,y),F(y,z)→F(x,z)

clause形に変換するとき、違うclauseの変数は独立になる。

λx,z,E.y F(x,y),F(y,z)→F(x,z)

は、全順序のようにも見えるが本当は、友達の友達は友達の関係。

ここでは、yが存在すればF(x,z)であるということで、存在が重要。

存在を全称にしてしまってこれをclauseにすると

¬F(x,y),¬F(y,z),F(x,z)

となり、これの否定は

F(x,y),F(y,z),¬F(x,z)

になる。

この否定が矛盾を導けば、元の主張は正しいということになる。

Fact1={F(a,b), F(b,c),F(a,c)}

のとき、確かに反証できる。

しかし、

Fact2={F(a,b), F(d,c), F(a,c)}

でも成り立ってしまうのはおかしい。

これはおそらく、yは存在なのでclauseを超えて同じ値にならなくてはならないということではないだろうか。

もともとclause formにするとき存在変数は定数に置き換えられることになるので、同一性は必要とされる。しかし、定数では代入ができないのでこの問題が解決できない。

mguを代入とだけ考えるのではなく、{x←t}を{x=t}という条件と考えれば、対処できるとは思う。

いずれにせよ、存在変数(とは呼ばないと思うが)は、clauseを超えた変数の同一性と考えればいいのではないか。

あるいは問題の視点が間違っているかも。