Boolean logic assumes every rule holds always. The real world is full of defaults, overrides, and specificity. Spindle is a non-monotonic reasoning engine in Rust that handles conflict, priority, and withdrawal — and emits a proof tree you can show to an auditor.
Every interesting rule system — policy, regulation, medical guidelines, pricing logic — is full of "normally X, but if Y." Prolog and Datalog can't express defeat. Rules engines like Drools bolt priority on top of boolean logic and leave you guessing why a conclusion held.
A rules engine with hand-rolled priority ordering, no formal semantics, and no way to explain why conclusion A won out over conclusion B.
Prolog or Datalog that refuse to draw any conclusion when facts conflict, so you end up encoding defeat as negation-as-failure and crossing your fingers.
An LLM that produces a plausible-sounding answer with no derivation, no citations, and no guarantee it follows from the rules you actually wrote.
Defeasible logic with four rule types — facts, strict, defeasible, defeaters — and a superiority relation that resolves conflicts by your own policy.
Proof trees that cite every rule and premise used, rendered as JSON for machines or natural language for humans.
Temporal algebra and arithmetic built in — Allen's 13 interval relations, decimal money math, hypothetical what-if queries, and abduction.
The classic penguin example: birds normally fly, but penguins don't.
Click through a real spindle session.
; penguin.spl — birds normally fly, but penguins don't (given bird) (given penguin) (normally r1 bird flies) (normally r2 penguin (not flies)) (prefer r2 r1) ; penguin-rule beats bird-rule
$ spindle reason penguin.spl Conclusions: +D penguin strictly provable +D bird strictly provable +d ~flies defeasibly provable -d flies defeated by r2 # r1 fires, r2 fires, (prefer r2 r1) breaks the tie. # Non-monotonic: add "penguin" and "flies" retracts.
$ spindle explain "~flies" penguin.spl Explanation for +d ~flies Proven defeasibly and not defeated by any conflicting rule. Derivation: 1. "~flies" was derived defeasibly Using defeasible rule: r2 Prerequisites: 1. "penguin" was established as a fact Using fact: f2 # Every step names the rule and the facts it depends on.
$ spindle why-not "flies" penguin.spl flies is not provable: Would be derived by rule: r1 Blocked by: - Rule r1: contradicted (Contradicted by r2) # The engine names the rule that fired and the rule that blocked it.
$ spindle requires "flies" penguin.spl Verified requirements for (flies): 1. Add facts: {(flies)} # Abduction: what would have to be true for the goal to hold? # Here the penguin rule dominates, so the only route is asserting # flies directly. Useful for diagnosing "why won't this derive?"
Model the real shape of policy: defaults that normally hold, strict rules that must hold, and defeaters that only block. Superiority encodes priority without ambiguity.
Every conclusion carries a derivation. Render it as JSON for pipelines or natural language for humans. Trust-weighted reasoning surfaces how confident each step is.
Ship the same engine to a CLI, a server, a browser, or a Node runtime. SPL (Spindle Lisp) is the source DSL; theories are files you can diff, review, and version.
Spindle compiles SPL into an internal representation, performs forward chaining with defeasible derivation, and emits a labelled proof graph. Labels are the classic DL four: +Δ, −Δ, +∂, −∂.
Adding a fact can retract a conclusion. That's the point: it's how real policy and regulation work.
Defeasible logic terminates. No infinite recursion, no halting problem — just bounded derivation.
Allen's 13 relations (before, meets, overlaps, during, …) are primitives, not library macros.
Three numeric types (Integer, Decimal, Float) with explicit coercions. Decimal math is exact.
S-expressions. No hidden macros, no operator precedence gotchas. Diffable and review-friendly.
WASM build runs in Node and any modern browser. Reason in the page, not on a server.
Install the CLI, write a theory, ask for a proof. Ten minutes from zero to your first defeasible derivation.
cargo install --git https://codeberg.org/anuna/spindle-rust spindle-cli