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.