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
(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.