Conclusions

Spindle computes four types of conclusions, representing different levels of provability.

The Four Conclusion Types

Definite Conclusions (+D / -D)

Definite provability uses only facts and strict rules. No defeasible reasoning is involved.

(given bird)
(always r1 bird animal)        ; Strict rule
(normally r2 bird flies)       ; Defeasible rule

Conclusions:

• +D bird — fact
• +D animal — via strict rule r1
• -D flies — no strict path to prove flies

When is +D Useful?

Definite provability represents certainty in domains such as:

• Binding legal requirements
• Safety constraints
• Logical necessities

Defeasible Conclusions (+d / -d)

Defeasible provability extends definite provability with defeasible rules.

(given bird)
(normally r1 bird flies)

Conclusions:

• +d bird — fact (also +D)
• +d flies — via defeasible rule r1

The Relationship

+D implies +d
   If definitely provable, then defeasibly provable

-d implies -D
   If not defeasibly provable, then definitely not provable

Conflict and Ambiguity

When rules conflict without a superiority relation, neither conclusion is provable:

(given trigger)
(normally r1 trigger outcome)
(normally r2 trigger (not outcome))
; No superiority declared

Conclusions:

• +D trigger
• -d outcome — blocked by r2
• -d -outcome — blocked by r1

Both outcomes are ambiguous — neither can be proven.

Resolved Conflict

With superiority, the conflict is resolved:

(given trigger)
(normally r1 trigger outcome)
(normally r2 trigger (not outcome))
(prefer r1 r2)

Conclusions:

• +d outcome — r1 wins
• -d -outcome — r2 is defeated

Example: Multi-Level

(given a)
(always r1 a b)                ; Strict: a implies b
(normally r2 b c)              ; Defeasible: b typically implies c
(normally r3 b (not c))        ; Defeasible: b typically implies (not c)
(prefer r2 r3)                 ; r2 wins

Conclusions:

Negative Conclusions

Negative conclusions (-D, -d) require constructive evidence under the proof conditions. Failure to find a positive proof is not itself a negative proof. For example, (always loop p p) leaves p undecided: neither +D p nor -D p, and neither +d p nor -d p. (normally loop p p) yields -D p, but leaves defeasible provability undecided.

An undecided premise does not justify discarding an attacker. This distinction matters when rules contain cycles. See Algorithms.

Negative tags also differ from strong negation: -d p does not establish +d ~p. If both p and ~p are definite facts, both retain +D and +d; this does not prove unrelated literals.

Reading Spindle Output

The default spindle reason penguin.spl lists proved literals once in SPL syntax. Use --detailed to inspect proof tags:

$ spindle reason --detailed penguin.spl
Conclusions:

  +D (bird)
  +D (penguin)
  +d (bird)
  +d (penguin)
  +d (not (flies))
  -D (flies)
  -d (flies)
  -D (not (flies))

Interpretation:

• bird and penguin are facts (both +D and +d).
• (not (flies)) is defeasibly provable (the penguin rule wins).
• flies is not provable at either level.
• Neither flies nor (not (flies)) is definitely provable.

Filtering Output

The --positive flag filters detailed text or JSON to positive proof tags:

spindle reason --detailed --positive penguin.spl

This retains +D and +d, including the positive proof of (not (flies)). The default concise text view already shows only proved literals and merges multiple proof tags for the same literal.