Skolem function

Skolem functions are CycL functions which are used in the implementation of formulas that use existential quantification. They are instances of #$ReifiableFunction, and are automatically generated. Whenever someone asserts to the Knowledge Base a sentence that contains #$thereExists (in an arg0 position), Cyc automatically creates a new instance of #$SkolemFunction and rewrites the assertion using that Skolem function.

For example, suppose we want Cyc to know that every animal has a birth date. So we assert the following sentence:

(implies
   (isa ?X Animal)
   (thereExists ?Y
     (birthDate ?X ?Y)))

In response, Cyc automatically reifies a new unary instance of #$SkolemFunction (call it “BirthDateFn”) that takes any given animal to its date of birth, and then rewrites our rule using “BirthDateFn” instead of #$thereExists, as

(implies
   (and
     (isa ?X Animal)
     (termOfUnit ?Y (BirthDateFn ?X)))
   (birthDate ?X ?Y))

Note that actual Cyc-generated Skolem function names consist of the prefix “SKF-” follow by a numeral.