Default method for skolemizing, in which wffs of the form

EXISTS y . M are replaced by M(g(...)). There are three possible ways to

do this:

SK1 is the original method due to Skolem, where the Skolem constants

g take as arguments all the x such that FORALL x occurs in the wff

and EXISTS y . M is in its scope.

SK3 is the method in which the arguments of g are the free variables

of EXISTS y . M.

NIL means don't Skolemize at all; use selection nodes instead.

SKOLEM-DEFAULT takes values of type SYMBOL.

It belongs to subjects MS98-1 MS93-1 MS92-9 MS91-7 MS91-6 MS90-9 MS90-3 MS89 MS88 MATING-SEARCH .

Its default value is SK1

Its current value is SK1.

© 1988-99, Carnegie Mellon University.