Negation

Spindle uses strong (explicit) negation. (not p) needs support from a fact or rule; absence of a proof of p does not establish (not p).

(given (not guilty))
(normally no-flight penguin (not flies))

Positive evidence and unknown results

For example, (always loop p p) supplies no positive or negative proof for p. A literal absent from the theory is not automatically listed in the engine's conclusions. A query can still report its status as unknown.

The negative proof tag -d p does not mean +d ~p. The distinction appears in Conclusions.

Conflicts and definite evidence

(given trigger)
(normally left trigger p)
(normally right trigger (not p))

Without priority, these competing defaults block each other. A definite proof of ~p prevents a merely defeasible proof of p. If p is also definitely proved, both sides retain +D and +d; inconsistency does not prove unrelated literals.

Negated premises

(given (bird eddie))
(given (not (penguin eddie)))
(normally flight
  (and (bird ?x) (not (penguin ?x)))
  (flies ?x))

The negative premise needs its own positive proof. Removing the explicit not-penguin fact leaves the rule without that support.

Explicit defeasible defaults

An empty-body defeasible rule represents a presumption that evidence can override. A fact does not represent this default:

(normally presume () (not guilty))
(normally convict evidence guilty)
(prefer convict presume)

Without evidence, this derives +d ~guilty. Adding (given evidence) lets the preferred rule derive +d guilty. This is an explicit domain default; SPL has no general negation-as-failure operator. A (given (not guilty)) fact remains definitely true and cannot be overridden this way.