要旨
We develop a perfect model semantics for logic programs with negation and
equality. Our approach is based on ordered rewriting, a fundamental technique
used in equational programming. A logic program in our sense is a set of
first-order clauses with equality together with a well-founded ordering on
terms and atoms. We show that any consistent logic program has a unique perfect
model, provided the ordering is total on ground expressions. The key to this
result is a notion of saturation of a set of formulas (under certain inference
rules) together with a related concept of redundancy. Our techniques can be
applied to Prolog-programs (without equality), in which case a class of
programs can be characterized via the notion of stratification up to redundancy
for which unique perfect models exist. This extends previous results on (local
and weak) stratification.
