The Existential Quantifier

The existential quantifier has not yet been implemented in SNePS 2. However, it is not needed, because Skolem functions can be used instead.

Whenever an existentially quantified variable y is bound within the scope of universally quantified variables , y can be replaced by the Skolem function as long as f is used nowhere else. The existential quantifier that binds y can then be eliminated.

So, to represent an existentially quantified variable in SNePS 2, define a set of arcs, say Skf, a1, a2, ..., and replace the variable node by a molecular node with the ai arcs going to the universally quantified variables whose scopes contain the existentially quantified variable, and with the Skf arc going to a new base node that serves as the Skolem function. The Skolem function node may be named mnemonically.

For example to represent the formula

you might do

(assert forall $man
           ant (build member *man class man)
            cq ((build member (build Skf loved-by a1 *man) = thiswoman
                       class  woman)
                (build agent *man act loves object *thiswoman)))