SKOLEM-DEFAULT : FLAG

SKOLEM-DEFAULT is a flag or parameter.
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.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage