  Skolem functions play a central role in the study of first order logic, both
from theoretical and practical perspectives. While every Skolemized formula in
first-order logic makes use of Skolem constants and/or functions, not all such
Skolem constants and/or functions admit effectively computable interpretations.
Indeed, the question of whether there exists an effectively computable
interpretation of a Skolem function, and if so, how to automatically synthesize
it, is fundamental to their use in several applications, such as planning,
strategy synthesis, program synthesis etc.
  In this paper, we investigate the computability of Skolem functions and their
automated synthesis in the full generality of first order logic. We first show
a strong negative result, that even under mild assumptions on the vocabulary,
it is impossible to obtain computable interpretations of Skolem functions. We
then show a positive result, providing a precise characterization of
first-order theories that admit effective interpretations of Skolem functions,
and also present algorithms to automatically synthesize such interpretations.
We discuss applications of our characterization as well as complexity bounds
for Skolem functions (interpreted as Turing machines).
