t_wの輪郭

存在限量子\( \exists \)の除去

論理式から∃をなくす操作

以下のようにする。
\( \forall x \exists y G(x, y)\)
\( = \forall x G(x, F(x)) \)

このときの\(F\)をスコーレム関数と呼ぶ

http://aiweb.cs.ehime-u.ac.jp/~ninomiya/ke/ke-8-slide.pdf