  Logic programming, as exemplified by datalog, defines the meaning of a
program as the canonical smallest model derived from deductive closure over its
inference rules. However, many problems call for an enumeration of models that
vary along some set of choices while maintaining structural and logical
constraints -- there is no single canonical model. The notion of stable models
has successfully captured programmer intuition about the set of valid solutions
for such problems, giving rise to a family of programming languages and
associated solvers collectively known as answer set programming. Unfortunately,
the definition of a stable model is frustratingly indirect, especially in the
presence of rules containing free variables.
  We propose a new formalism, called finite-choice logic programing, for which
the set of stable models can be characterized as the least fixed point of an
immediate consequence operator. Our formalism allows straightforward expression
of common idioms in both datalog and answer set programming, gives meaning to a
new and useful class of programs, enjoys a constructive and direct operational
semantics, and admits a predictive cost semantics, which we demonstrate through
our implementation.
