  We give a purely model-theoretic characterization of the semantics of logic
programs with negation-as-failure allowed in clause bodies. In our semantics
the meaning of a program is, as in the classical case, the unique minimum model
in a program-independent ordering. We use an expanded truth domain that has an
uncountable linearly ordered set of truth values between False (the minimum
element) and True (the maximum), with a Zero element in the middle. The truth
values below Zero are ordered like the countable ordinals. The values above
Zero have exactly the reverse order. Negation is interpreted as reflection
about Zero followed by a step towards Zero; the only truth value that remains
unaffected by negation is Zero. We show that every program has a unique minimum
model M_P, and that this model can be constructed with a T_P iteration which
proceeds through the countable ordinals. Furthermore, we demonstrate that M_P
can also be obtained through a model intersection construction which
generalizes the well-known model intersection theorem for classical logic
programming. Finally, we show that by collapsing the true and false values of
the infinite-valued model M_P to (the classical) True and False, we obtain a
three-valued model identical to the well-founded one.
