
Chapter
1
:
Negation in Logic Programming
Finally we note that the occur axiom, OA,t(x) Φ χ is redundant if DCA is
used, i.e.,
EA U FA U DCA — OA.
This is not true if DCA is replaced by WDCA; e.g., with constants 0,s, the
formula s(x) Φ χ is not provable from EA U FA U WDCA, for this has a
model consisting of the natural numbers together with an element ω such that
s(<o) = ω.
The closed world assumption, as well as possibly having no computable
proof procedure, is often considered to be too strong a presumption in favor of
negative information. And if there is indefinite knowledge about ground atoms,
then cwa(P) is inconsistent; e.g., if Ρ