10 Negation-as-failure
Negation as finite failure is implemented. Use ~G to mean
the negation of expression G. G must be ground when ~G
is called; this may be fixed in future implementations. The interaction of
negation as failure and the depth-bound is handled correctly.
There is
a problem with negation and why questions; sometimes the
rule written out omits some negation symbols. This only occurs when
non-atomic formulae are negated.
The interaction of negation as failure with assumables isn't
satisfactory. It is recommended that you don't use both assumables and
negation as failure.
©David
Poole, 1998
