# 10 Negation-as-failure

Negation as finite failure is implemented. Use `~`

G to mean the
negation of G. G can be any body but must be ground (i.e., contain no
variables) 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
as general as possible; it is only sensible if you make sure that any proof for a negated atom
does not include assumables. Negation as failure does work with probabilities.