Spindle-Rust

Spindle-Rust is a Rust implementation of the SPINdle defeasible logic reasoning engine.

This project is part of the SPINdle family:

• SPINdle (source) - The original Java implementation by NICTA (now Data61/CSIRO)
• spindle-racket - A comprehensive Racket port of SPINdle Java v2.2.4, with trust-weighted reasoning
• spindle-rust - This Rust port, based on spindle-racket v1.7.0

What is Defeasible Logic?

Defeasible logic is a non-monotonic reasoning system that allows conclusions to be defeated by stronger evidence. Unlike classical logic where adding new information only adds new conclusions, defeasible logic can revise existing conclusions when conflicting evidence appears. Crucially, it is tractable — for propositional theories, inference runs in linear time relative to the size of the theory (Maher, 2001). With first-order variables, a grounding phase instantiates rules against known facts before reasoning begins; the grounding step can be exponential in rule body size (as with Datalog), but reasoning over the ground theory remains polynomial. This makes defeasible logic practical where other non-monotonic formalisms are intractable.

; The classic "Tweety" example
(given bird tweety)              ; Tweety is a bird
(given penguin tweety)           ; Tweety is a penguin

(normally birds-fly              ; Birds typically fly
  (bird ?x) (flies ?x))

(normally penguins-dont-fly      ; Penguins don't fly
  (penguin ?x) (not (flies ?x)))

(prefer penguins-dont-fly birds-fly)  ; Specificity: more specific rule prevails

Result:

Conclusions:

  +D penguin(tweety)
  +D bird(tweety)
  +d penguin(tweety)
  +d bird(tweety)
  +d ~flies(tweety)
  -D flies(tweety)
  -d flies(tweety)
  -D ~flies(tweety)

Tweety is defeasibly proven not to fly (+d ~flies(tweety)), because penguins-dont-fly defeats birds-fly.

Features

• Four rule types: facts, strict rules, defeasible rules, and defeaters
• Reasoning engine: standard DL(d) forward chaining
• Temporal reasoning: Allen interval algebra with 13 temporal relations
• First-order variables: Datalog-style grounding with ?x syntax
• Query operators: what-if, why-not, and abduction
• Trust-aware reasoning: source attribution and weighted conclusions
• SPL format: Lisp-based input with variables, temporal, and trust directives
• WebAssembly support: run in browsers and Node.js

Quick Example

#![allow(unused)]
fn main() {
use spindle_core::prelude::*;

let mut theory = Theory::new();

// Add facts
theory.add_fact("bird");
theory.add_fact("penguin");

// Add defeasible rules
let r1 = theory.add_defeasible_rule(&["bird"], "flies");
let r2 = theory.add_defeasible_rule(&["penguin"], "~flies");

// Penguin rule beats bird rule
theory.add_superiority(&r2, &r1);

// Reason and get conclusions
let conclusions = theory.reason();
}

Installation

CLI

cargo install --path crates/spindle-cli

Library

[dependencies]
spindle-core = { path = "crates/spindle-core" }
spindle-parser = { path = "crates/spindle-parser" }

Crate Structure

References

• SPINdle Project - Original Java implementation by NICTA/Data61
• Nute, D. (1994). "Defeasible Logic" - Foundational paper on defeasible logic
• spindle-racket - Racket implementation this port is based on

License

LGPL-3.0-or-later (same as original SPINdle)

Getting Started

This guide walks you through installing Spindle-Rust and running your first defeasible logic program.

Spindle-Rust is a Rust port of SPINdle, a defeasible logic reasoning system originally developed by NICTA (now Data61/CSIRO). This implementation is based on spindle-racket v1.7.0.

Installation

Building from Source

git clone https://codeberg.org/anuna/spindle-rust
cd spindle-rust
cargo build --release

Installing the CLI

cargo install --path crates/spindle-cli

This installs the spindle command to your Cargo bin directory.

Your First Theory

Create a file called hello.spl:

; Facts
(given bird)

; Rules
(normally r1 bird flies)
(normally r2 bird has_feathers)

Run it:

spindle reason hello.spl

Output:

+D bird
+d bird
+d flies
+d has_feathers
-D flies
-D has_feathers

Understanding the Output

The Penguin Example

Create penguin.spl:

; Tweety is a bird and a penguin
(given bird)
(given penguin)

; Birds typically fly
(normally r1 bird flies)

; Penguins typically don't fly
(normally r2 penguin (not flies))

; Penguin rule is more specific
(prefer r2 r1)

Run it:

spindle reason penguin.spl

Output:

+D bird
+D penguin
+d bird
+d penguin
+d -flies
-D flies
-D -flies
-d flies

Key result: +d -flies - Tweety defeasibly doesn't fly because the penguin rule (r2) beats the bird rule (r1).

CLI Options

# Show only positive conclusions
spindle reason --positive penguin.spl

# Output as JSON
spindle reason --json penguin.spl

# Validate syntax without reasoning
spindle validate penguin.spl

# Show theory statistics
spindle stats penguin.spl

Using as a Library

Add to your Cargo.toml:

[dependencies]
spindle-core = { path = "crates/spindle-core" }

Basic usage:

use spindle_core::prelude::*;

fn main() {
    let mut theory = Theory::new();

    // Add facts
    theory.add_fact("bird");
    theory.add_fact("penguin");

    // Add defeasible rules
    let r1 = theory.add_defeasible_rule(&["bird"], "flies");
    let r2 = theory.add_defeasible_rule(&["penguin"], "~flies");

    // Set superiority
    theory.add_superiority(&r2, &r1);

    // Reason
    let conclusions = theory.reason();

    for c in conclusions {
        println!("{}", c);
    }
}

Next Steps

• Concepts - Understand defeasible logic fundamentals
• SPL Reference - Complete SPL syntax
• Examples - Advanced examples with variables

Concepts

Defeasible logic is a non-monotonic reasoning system. This chapter introduces the core concepts you need to understand Spindle.

Classical vs. Defeasible Logic

Classical (Monotonic) Logic:

• Once proven, always proven
• Adding facts only adds conclusions
• Cannot handle exceptions

Defeasible (Non-Monotonic) Logic:

• Conclusions are tentative
• New evidence can defeat existing conclusions
• Handles exceptions naturally

The Tweety Problem

The motivating example for defeasible logic:

Tweety is a bird. Tweety is a penguin. Birds fly. Penguins don't fly. Does Tweety fly?

Classical logic produces a contradiction. Defeasible logic resolves it by recognizing that "penguins don't fly" is a more specific rule that should override "birds fly."

(given bird)
(given penguin)
(normally r1 bird flies)
(normally r2 penguin (not flies))
(prefer r2 r1)

Result: Tweety doesn't fly.

Key Terminology

Chapters

• Rules and Facts - The four rule types
• Conclusions - Understanding +D, -D, +d, -d
• Superiority - Resolving conflicts
• Negation - Strong negation in Spindle

Rules and Facts

Spindle supports four types of rules, each with different semantics for how conclusions are drawn.

Facts (given)

Facts are unconditional truths. They have no body (antecedent) and are always true.

(given bird)
(given penguin)
(given (not guilty))    ; Negated fact

Facts produce definite conclusions (+D) that cannot be defeated.

Strict Rules (always)

Strict rules express necessary implications. If the body is true, the head must be true.

(always r1 penguin bird)              ; All penguins are birds
(always r2 (and human mortal) dies)   ; All mortal humans die

Strict rules produce definite conclusions (+D). They cannot be defeated by defeasible rules.

When to Use Strict Rules

Use strict rules for:

• Definitional relationships (penguins are birds)
• Logical necessities (modus ponens)
• Constraints that have no exceptions

Defeasible Rules (normally)

Defeasible rules express typical or default behavior that may have exceptions.

(normally r1 bird flies)            ; Birds typically fly
(normally r2 student has-loans)     ; Students typically have loans

Defeasible rules produce defeasible conclusions (+d) that can be defeated by:

• Strict rules proving the opposite
• Superior defeasible rules
• Defeaters

When to Use Defeasible Rules

Use defeasible rules for:

• Default behaviors with exceptions
• Typical properties
• Rules of thumb

Defeaters (except)

Defeaters are special rules that block conclusions without proving anything themselves.

(except d1 broken-wing flies)    ; A broken wing blocks "flies"

Defeater vs. Defeasible Rule

; Defeasible rule: proves (not flies)
(normally r1 penguin (not flies))

; Defeater: only blocks flies, doesn't prove (not flies)
(except d1 sick flies)

The difference:

• r1 can prove (not flies) if its body is satisfied
• d1 can only block flies, it never proves (not flies)

When to Use Defeaters

Use defeaters when:

• You want to express doubt without asserting the opposite
• Evidence should block a conclusion but not prove its negation
• You're modeling uncertainty

Rule Bodies (Antecedents)

Rule bodies can contain:

Single Literal

(normally r1 bird flies)

Multiple Literals (Conjunction)

(normally r1 (and bird healthy) flies)
(normally r2 (and student employed) busy)

Negated Literals

(normally r1 (and bird (not penguin)) flies)   ; Non-penguin birds fly

Rule Heads (Consequents)

Rule heads are single literals that can be:

Positive

(normally r1 bird flies)

Negated

(normally r1 penguin (not flies))

Rule Labels

Every rule has a label (identifier) used for:

• Superiority relations
• Explanations
• Debugging

Labels are optional (auto-generated if omitted):

(normally r1 bird flies)      ; labeled r1
(normally bird flies)         ; auto-labeled

Summary

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?

Use definite provability when you need certainty:

• Legal requirements that must be met
• 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:

• +D a — fact
• +D b — strict from a
• +d a — (implied by +D)
• +d b — (implied by +D)
• +d c — defeasible, r2 wins over r3
• -D c — no strict path
• -D -c — no strict path
• -d -c — r3 defeated

Negative Conclusions

Negative conclusions (-D, -d) indicate unprovability:

-D (Definitely Not Provable)

No chain of facts and strict rules leads to this literal.

-d (Defeasibly Not Provable)

No chain of rules (including defeasible) leads to this literal, OR the literal is blocked by:

• A strict rule proving the complement
• A superior defeasible rule
• A defeater

Reading Spindle Output

$ spindle reason penguin.spl
+D bird
+D penguin
+d bird
+d penguin
+d -flies
-D flies
-D -flies
-d flies

Interpretation:

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

Filtering Output

Show only positive conclusions:

spindle reason --positive penguin.spl

Output:

+D bird
+D penguin
+d bird
+d penguin
+d -flies

Superiority

Superiority relations resolve conflicts between competing rules.

The Problem

When two rules conclude opposite things, we have a conflict:

(given bird)
(given penguin)
(normally r1 bird flies)
(normally r2 penguin (not flies))

Both r1 and r2 fire. Without superiority, we get ambiguity — neither flies nor (not flies) is provable.

Declaring Superiority

(prefer r2 r1)    ; r2 beats r1

Now when both rules fire, r2 wins and (not flies) is provable.

Superiority Chains

Shorthand for multiple superiority relations:

(prefer r3 r2 r1)   ; r3 > r2 > r1

Expands to:

(prefer r3 r2)
(prefer r2 r1)

Transitivity

Superiority is not automatically transitive. If you need r3 > r1, declare it explicitly:

(prefer r3 r2)
(prefer r2 r1)
(prefer r3 r1)    ; Must be explicit

Conflict Resolution Algorithm

When evaluating a defeasible conclusion:

1. Find all rules that could prove the literal
2. Find all rules that could prove the complement (attackers)
3. For each attacker with satisfied body:
   • If no defender is superior to it → blocked
   • If some defender is superior → attack fails
4. If all attacks fail → conclusion is provable

Example: Three-Way Conflict

(given a)
(given b)
(given c)

(normally r1 a result)
(normally r2 b (not result))
(normally r3 c result)

(prefer r1 r2)    ; r1 beats r2
(prefer r3 r2)    ; r3 beats r2

Analysis:

• r2 attacks result
• Both r1 and r3 are superior to r2
• The attack is defeated
• +d result

Symmetric Conflicts

If two rules are equally superior over each other (or neither is superior), ambiguity results:

(given trigger)
(normally r1 trigger a)
(normally r2 trigger (not a))
; No superiority

Result: Neither a nor (not a) is provable.

Defeating Defeaters

Defeaters can be overridden by superiority:

(given bird)
(given healthy)

(normally r1 bird flies)
(except d1 bird flies)          ; Defeater blocks flies
(normally r2 healthy flies)

(prefer r2 d1)                  ; Healthy birds overcome the defeater

If both bird and healthy are true, r2 beats d1 and flies is provable.

Strict Rules and Superiority

Strict rules always win over defeasible rules, regardless of superiority:

(given p)
(always r1 p q)              ; Strict
(normally r2 p (not q))      ; Defeasible
(prefer r2 r1)               ; This has no effect!

Result: +D q (strict rule wins)

Superiority only affects conflicts between:

• Defeasible rules
• Defeasible rules and defeaters
• Defeaters

Best Practices

Use Specificity

More specific rules should be superior:

(normally r1 bird flies)
(normally r2 penguin (not flies))
(prefer r2 r1)    ; Penguin is more specific than bird

Document Reasoning

Use comments to explain why one rule beats another:

; Medical override: confirmed diagnosis beats symptoms
(prefer r-diagnosis r-symptoms)

Avoid Cycles

Don't create circular superiority:

; BAD — creates a cycle
(prefer r1 r2)
(prefer r2 r1)

This leads to undefined behavior.

Negation

Spindle uses strong negation (also called explicit negation), not negation-as-failure.

Strong Negation vs. Negation-as-Failure

Negation-as-Failure (NAF)

Used in Prolog and many logic programming systems:

• "not P" means "P cannot be proven"
• Absence of evidence is evidence of absence

Strong Negation

Used in Spindle:

• (not P) is a separate proposition
• Must be explicitly proven
• Absence of P does not imply (not P)

Syntax

(given (not guilty))
(normally r1 penguin (not flies))

Three-Valued Outcomes

For any literal P, the outcome can be:

Example: Unknown State

(given bird)
(normally r1 bird flies)
; No information about grounded

Conclusions:

• +d flies (via r1)
• -d grounded (no rule proves it)
• -d -grounded (no rule proves its negation either)

The grounded literal is in an unknown state.

Complementary Literals

P and (not P) are complements. They interact in specific ways:

Conflict

If rules prove both P and (not P):

(given a)
(normally r1 a p)
(normally r2 a (not p))

Without superiority, neither is provable (ambiguity).

Definite Blocking

If (not P) is definitely provable, P cannot be defeasibly provable:

(given (not p))              ; Definite fact: (not p)
(normally r1 a p)            ; Tries to prove p

Even if r1's body is satisfied, +d p is blocked because +D -p.

Negation in Rule Bodies

Negated literals can appear in rule bodies:

(normally r1 (and bird (not penguin)) flies)          ; Non-penguin birds fly
(normally r2 (and student (not employed)) needs-loan)

Consistency

Spindle does not enforce consistency. A theory can prove both P and (not P):

(given p)
(given (not p))

Result:

• +D p
• +D -p

This is an inconsistent theory. Spindle reports both conclusions without error.

Detecting Inconsistency

To detect inconsistency, check for literals where both +D P and +D -P (or +d P and +d -P) are concluded.

Closed World Assumption

Spindle does not use the Closed World Assumption by default. If you need it, add explicit rules:

; CWA for 'guilty': if not proven guilty, then not guilty
(given (not guilty))                    ; Default: not guilty
(normally r1 evidence guilty)           ; Can be overridden by evidence
(prefer r1 f1)

This pattern uses a defeatable default.

SPL Format Reference

SPL (Spindle Lisp) is the input language for Spindle. It replaces the earlier DFL syntax with a LISP-based DSL whose s-expression structure makes it straightforward to add new constructs (temporal operators, trust directives, claims blocks, etc.) without grammar ambiguity.

File Extension

.spl

Comments

Semicolon to end of line:

; This is a comment
(given bird)  ; Inline comment

Grammar Overview

theory      = statement*
statement   = fact | rule | prefer | meta
            | claims | trusts | decays | threshold

; Core
fact        = "(given" literal ")"
rule        = "(" keyword label? body head ")"
keyword     = "always" | "normally" | "except"
prefer      = "(prefer" label+ ")"
meta        = "(meta" label property* ")"

; Trust
claims      = "(claims" source claims-meta* statement* ")"
claims-meta = ":at" atom | ":sig" atom | ":id" atom | ":note" atom
trusts      = "(trusts" source number ")"
decays      = "(decays" source decay-model number ")"
decay-model = "exponential" | "linear" | "step"
threshold   = "(threshold" name number ")"

; Temporal
time-expr   = "(moment" rfc3339-string ")" | integer | "inf" | "-inf"
during      = "(during" literal time-expr time-expr ")"

; Literals
literal     = atom | "(" atom arg* ")" | "(not" literal ")"
            | during | modal
modal       = "(" modal-op literal ")"
modal-op    = "must" | "may" | "forbidden"
body        = literal | "(and" body-elem+ ")"
body-elem   = literal | arith-constraint
atom        = identifier | variable
variable    = "?" identifier
source      = atom
number      = float in [0.0, 1.0]

; Arithmetic (body only)
arith-constraint = bind | compare
bind        = "(bind" variable arith-expr ")"
compare     = "(" cmp-op arith-expr arith-expr ")"
cmp-op      = "=" | "!=" | "<" | ">" | "<=" | ">="
arith-expr  = number | variable
            | "(" nary-op arith-expr+ ")"
            | "(" bin-op arith-expr arith-expr ")"
            | "(" unary-op arith-expr ")"
nary-op     = "+" | "-" | "*" | "/" | "min" | "max"
bin-op      = "div" | "rem" | "**"
unary-op    = "abs"

Facts

Simple Facts

(given bird)
(given penguin)
(given (not guilty))

Predicate Facts

(given (parent alice bob))
(given (employed alice acme))

Flat Predicate Syntax

(given parent alice bob)     ; Same as (given (parent alice bob))
(given employed alice acme)

Rules

Strict Rules (always)

(always penguins-are-birds penguin bird)
(always mortals-die (and human mortal) dies)

Defeasible Rules (normally)

(normally birds-fly bird flies)
(normally penguins-dont-fly penguin (not flies))

Defeaters (except)

(except broken-wing-blocks-flight broken-wing flies)

Unlabeled Rules

Labels are optional (auto-generated):

(normally bird flies)        ; Gets label like "r1"
(always penguin bird)        ; Gets label like "s1"

Literals

Simple

bird
flies
has-feathers

Negated

(not flies)
(not (parent alice bob))

Or with prefix:

~flies

Predicates with Arguments

(parent alice bob)
(employed ?x acme)
(ancestor ?x ?z)

Conjunction

Use and for multiple conditions:

(normally healthy-birds-fly (and bird healthy) flies)
(normally busy-students (and student employed) busy)

Why there is no or

Defeasible logic does not support disjunction in rule bodies. This is by design, not a missing feature — the proof theory (Nute/Billington/Antoniou) defines derivation over conjunctive rules only. Adding or would break the well-defined defeat and superiority semantics that make defeasible reasoning tractable.

Instead, express disjunction as separate rules that conclude the same head:

; "If rain or snow, take umbrella"
(normally rain-means-umbrella rain take-umbrella)
(normally snow-means-umbrella snow take-umbrella)

Each rule independently supports the same conclusion. If either rain or snow is provable, take-umbrella follows. This is the standard encoding of disjunctive conditions in defeasible logic, and it preserves per-rule defeat — you can override one path without affecting the other.

Variables

Variables start with ?:

(given (parent alice bob))
(given (parent bob charlie))

; Transitive closure
(normally parent-is-ancestor (parent ?x ?y) (ancestor ?x ?y))
(normally ancestor-chain (and (parent ?x ?y) (ancestor ?y ?z)) (ancestor ?x ?z))

Wildcard

Use _ to match anything:

(normally has-any-parent (parent _ ?y) (has-parent ?y))

Superiority

Two Rules

(prefer penguins-dont-fly birds-fly)

Chain

(prefer emergency-override safety-protocol standard-rule)

Expands to:

(prefer emergency-override safety-protocol)
(prefer safety-protocol standard-rule)

Metadata

Attach metadata to rules:

(meta birds-fly
  (description "Birds normally fly")
  (confidence 0.9)
  (source "ornithology-handbook"))

Properties

(meta rule-label
  (key "string value")
  (key2 ("list" "of" "values")))

Modal Operators

Obligation (must)

(normally contract-requires-payment signed-contract (must pay))

Permission (may)

(normally members-may-access member (may access))

Forbidden (forbidden)

(normally no-entry-unauthorized unauthorized (forbidden enter))

Temporal Reasoning

Time Points

Supported time formats:

(moment "2024-06-15T14:30:00Z")  ; RFC3339 / ISO 8601
1718461800000                    ; Epoch milliseconds
inf                              ; Positive infinity
-inf                             ; Negative infinity

Note: Multi-arity forms like (moment 2024 6 15) are reserved for future extensions.

During

(given (during bird 1 10))
(given (during (employed alice acme)
  (moment "2020-01-01T00:00:00Z")
  (moment "2023-01-01T00:00:00Z")))

Allen Relations

SPL status: Allen relations are implemented in the core Rust API but are not yet usable as SPL predicates. Exposing them requires interval variables (e.g., (during p ?t)), planned for a future release. The Allen during relation (interval containment) is distinct from the during SPL operator described above.

Allen's interval algebra defines exactly 13 mutually exclusive relations between two time intervals X and Y. Every pair of intervals satisfies exactly one.

Relation          X              Y           Inverse
─────────────────────────────────────────────────────────
before            ██████                     after
                              ██████

meets             ██████                     met-by
                        ██████

overlaps          ██████                     overlapped-by
                     ██████

starts            ████                       started-by
                  ██████████

during              ████                     contains
                  ██████████

finishes              ████                   finished-by
                  ██████████

equals            ██████████
                  ██████████                 (self-inverse)

Each relation has a strict inverse (reading the diagram with X and Y swapped), giving 6 symmetric pairs plus equals:

Arithmetic Expressions

Arithmetic expressions can appear in rule bodies as bind constraints, comparison guards, or as arguments to predicates.

Numeric Literals

42          ; Integer
3.14        ; Decimal (arbitrary precision)

Operators

(+ 1 2)           ; => 3
(* 2 3 4)         ; => 24
(- 10 3 2)        ; => 5 (left fold: 10-3-2)
(div 7 2)         ; => 3
(rem 7 2)         ; => 1
(** 2 10)         ; => 1024
(abs (- 3 10))    ; => 7
(min 5 3 8)       ; => 3

Bind Constraints

Bind a variable to the result of an arithmetic expression:

(normally compute-total
  (and (price ?p) (tax-rate ?r)
       (bind ?total (+ ?p (* ?p ?r))))
  (total ?total))

Comparison Guards

Compare two arithmetic expressions:

(normally adult-by-age
  (and (age ?x ?a) (> ?a 18))
  (adult ?x))

(normally failing-score
  (and (score ?x ?s) (<= ?s 50))
  (failing ?x))

Available operators: =, !=, <, >, <=, >=

Arithmetic in Predicate Arguments

Arithmetic expressions can appear as predicate arguments in rule bodies:

(normally compute-invoice
  (and (price ?item ?p) (tax-rate ?r))
  (invoice ?item (+ ?p (* ?p ?r))))

Type Promotion

Numeric types are promoted during arithmetic: Integer → Decimal → Float.

• Integer + Integer = Integer
• Integer + Decimal = Decimal
• Any + Float = Float
• div and rem require integer operands

Cross-type matching: Integer(2) matches Decimal(2.0) matches Float(2.0).

Reserved Keywords (REQ-008)

The following cannot be used as predicate names or rule labels:

+  -  *  /  div  rem  abs  min  max  **
bind  =  !=  <  >  <=  >=

Future reserved: sum, count, avg, round, floor, ceil

Restrictions

• Arithmetic constraints cannot appear in rule heads or facts (REQ-009)
• Arithmetic constraints cannot be negated with not or ~ (REQ-011)
• Temporal variables cannot be used as arithmetic operands (REQ-006)

Claims

The claims block attributes statements to a named source, with optional metadata.

(claims agent:alice
  :at "2024-06-15T12:00:00Z"
  :sig "abc123"
  :id "claim-001"
  :note "sensor reading"
  (given sunny)
  (normally no-umbrella-when-sunny sunny (not umbrella)))

Syntax

(claims source [:at timestamp] [:sig signature] [:id block-id] [:note annotation]
  statement ...)

• source — an atom identifying the claiming agent (e.g., agent:alice).
• :at — optional RFC3339 timestamp for when the claim was made.
• :sig — optional signature string for verification.
• :id — optional block identifier.
• :note — optional free-text annotation.

Statements inside a claims block are ordinary SPL expressions (given, always, normally, except, prefer) that automatically receive source metadata. See the Trust & Multi-Agent guide for details.

Complete Example

; The Penguin Example

; Facts
(given bird)
(given penguin)

; Strict rule
(always penguins-are-birds penguin bird)

; Defeasible rules
(normally birds-fly bird flies)
(normally birds-have-feathers bird has-feathers)
(normally penguins-dont-fly penguin (not flies))
(normally penguins-swim penguin swims)

; Superiority — specificity
(prefer penguins-dont-fly birds-fly)

; Defeater
(except broken-wing-blocks-flight broken-wing flies)

; Metadata
(meta birds-fly (description "Birds typically fly"))
(meta penguins-dont-fly (description "Penguins are an exception"))

CLI Reference

The spindle command-line tool for reasoning about defeasible logic theories.

Installation

cargo install --path crates/spindle-cli

Synopsis

spindle <COMMAND> [OPTIONS]
spindle reason [OPTIONS] [FILE]
spindle query <LITERAL> [FILE] [OPTIONS]
spindle explain <LITERAL> [FILE] [OPTIONS]
spindle why-not <LITERAL> [FILE] [OPTIONS]
spindle requires <LITERAL> [FILE] [OPTIONS]
spindle capabilities [OPTIONS]
spindle explain-code <CODE>

Commands

reason

Perform defeasible reasoning on a theory.

spindle reason examples/penguin.spl

--v2

Select JSON schema version v2 (spindle.reason.v2) for the JSON output envelope. The v2 schema includes typed term arguments in the literal_struct fields, giving downstream consumers richer structure than the v1 flat-string representation.

spindle reason examples/penguin.spl --json --v2

Without --v2, the default schema is spindle.reason.v1.

--trust

Include trust-weight annotations on each conclusion. When enabled, each conclusion carries a trust_degree (0.0--1.0) and optional trust_sources list.

spindle reason examples/penguin.spl --json --trust

validate

Check syntax without reasoning.

spindle validate examples/penguin.spl
spindle --json validate --stdin < examples/penguin.spl

Output on success:

Valid theory file

With --json success output:

{
  "valid": true,
  "diagnostics": []
}

Output on error:

Error at line 5: could not parse: invalid => syntax

stats

Show theory statistics.

spindle stats examples/penguin.spl
spindle --json stats --stdin < examples/penguin.spl

Output:

Theory Statistics:
  Facts:       2
  Strict:      1
  Defeasible:  4
  Defeaters:   1
  Superiority: 1
  Total rules: 8

With --json success output:

{
  "stats": {
    "total_rules": 8,
    "facts": 2,
    "strict": 1,
    "defeasible": 4,
    "defeaters": 1,
    "superiorities": 1
  },
  "diagnostics": []
}

query

Query if a literal holds in the theory.

spindle query flies examples/penguin.spl
spindle query "~flies" examples/penguin.spl
spindle query "(not flies)" examples/penguin.spl
spindle query flies examples/penguin.spl --json

The literal argument supports multiple formats: p, ~p, (not p), or complex SPL expressions.

Returns a QueryStatus:

Output:

QueryStatus: Provable

With --json:

{"literal":"flies","status":"Refuted"}

explain

Show the derivation proof tree for why a literal holds.

spindle explain "-flies" examples/penguin.spl
spindle explain "-flies" examples/penguin.spl --json

Shows the proof tree detailing how the reasoning engine derived the conclusion.

Output:

Explanation for -flies:
  -flies ← [defeasible] r3: penguin -> -flies
    penguin ← [fact]
  Blocked alternatives:
    r1: bird -> flies (defeated by r3 via superiority)
  Conflict resolutions:
    r3 > r1 (superiority)

With --json, the output is a JSON or JSON-LD structure containing an Explanation with proof nodes, blocked alternatives, and conflict resolutions.

why-not

Explain why a literal is NOT provable.

spindle why-not flies examples/penguin.spl
spindle why-not flies examples/penguin.spl --json

Lists the blocking rules and the reasons they prevent the literal from being derived. Useful for debugging unexpected results. When the literal is provable, the JSON output includes is_provable: true and blocked_by will be empty.

Output:

Why not flies?
  Rule r1: bird -> flies
    Status: Defeated
    Defeated by: r3 (penguin -> -flies) via superiority r3 > r1

Possible blocking reasons:

requires

Abduction: find the minimal sets of facts needed to derive a literal.

spindle requires flies examples/penguin.spl
spindle requires flies examples/penguin.spl --max 5
spindle requires flies examples/penguin.spl --json

The --max option limits the number of solutions returned (defaults to 10).

As of the v2 contract (IMPL-011), requires verifies all candidate solutions by default. Each candidate set of facts is fed back through the reasoning engine to confirm it actually makes the goal provable. The JSON output includes verification_mode: "verified" and a verification object with raw_examined, accepted, and rejected counts. Only accepted solutions appear in the solutions array. The JSON envelope uses schema spindle.requires.v2.

Output:

Verified requirements for flies:
  1. Add facts: {bird, -penguin}
  2. Add facts: {flies}

Each result is a minimal, verified set of assumptions that, if added to the theory, would make the literal provable.

capabilities

Show the commands, features, and JSON schema versions supported by this build of Spindle. Useful for tooling that needs to discover available functionality at runtime.

spindle capabilities
spindle capabilities --json

Output:

Spindle Capabilities:

Commands: reason, query, requires, explain, why-not

Features:
  --stdin: yes
  --at: yes
  --json: yes
  Trust overlay: no
  Given flags: no

Schema versions:
  reason: spindle.reason.v1
  query: spindle.query.v1
  requires: spindle.requires.v2
  explain: spindle.explain.v1
  why-not: spindle.why_not.v1

With --json, the output is a JSON object with schema spindle.capabilities.v1 containing commands, features, and schemas fields.

explain-code

Look up the meaning and common causes of a stable error code.

spindle explain-code RULE_NOT_FOUND
spindle explain-code SPL_PARSE_ERROR

This command does not accept --json; output is always human-readable text. Use it to get guidance when a JSON error envelope contains an unfamiliar error code.

JSON Envelope Schema Versions

Every --json response includes a schema_version field identifying the envelope format. The following schema versions are defined:

Options

--json

Output results in JSON format. Available for all commands, including validate and stats. When --json is present, success and failure paths are machine-readable JSON.

spindle reason examples/penguin.spl --json
spindle query flies examples/penguin.spl --json
spindle explain "-flies" examples/penguin.spl --json
spindle --json validate --stdin < examples/penguin.spl

Parse/usage failures also emit JSON envelopes when --json is present:

spindle --json

--at <TIME>

Set the reference time for temporal ("as-of") reasoning. The value must be an ISO 8601 / RFC 3339 timestamp.

spindle reason --at 2024-06-15T12:00:00Z examples/temporal.spl
spindle query p --at 2024-06-15T12:00:00Z examples/temporal.spl

--stdin

Read the theory from standard input instead of a file. Mutually exclusive with providing a file path.

cat examples/penguin.spl | spindle reason --stdin
spindle --json validate --stdin < examples/penguin.spl

--positive

Show only positive conclusions (+D, +d). Applies to the reason command.

spindle reason --positive examples/penguin.spl

Output:

+D bird
+D penguin
+d bird
+d penguin
+d -flies

--debug-errors

Show full error details including source chains and unredacted file paths. Useful for diagnosing unexpected failures.

spindle reason examples/penguin.spl --debug-errors

File Format Detection

The CLI auto-detects format by extension:

Exit Codes

Examples

Basic Reasoning

# Reason about a theory
spindle reason penguin.spl

Querying and Explaining

# Check if a literal holds
spindle query flies penguin.spl

# Get a proof tree for a derived conclusion
spindle explain "-flies" penguin.spl

# Debug why something is not provable
spindle why-not flies penguin.spl

# Find what facts would make a literal provable
spindle requires flies penguin.spl --max 5

# Get JSON output for scripting
spindle query flies penguin.spl --json

Validate Before Reasoning

spindle validate theory.spl && spindle reason theory.spl

Compare Runs

# Compare two revisions or theories
spindle reason theory-a.spl > run-a.txt
spindle reason theory-b.spl > run-b.txt
diff run-a.txt run-b.txt

Scripting

#!/bin/bash
for file in theories/*.spl; do
    echo "Processing $file..."
    if spindle validate "$file"; then
        spindle reason --positive "$file"
    else
        echo "Invalid: $file"
    fi
done

Environment Variables

SPINDLE_LOG=debug spindle reason theory.spl

Algorithms

Spindle uses a single reasoning engine: standard DL(d) forward chaining.

Overview

The engine computes conclusions in three phases:

1. Seed facts as both +D and +d.
2. Forward-chain strict and defeasible rules until saturation.
3. Emit negative conclusions (-D, -d) for literals not proven.

Forward Chaining

At a high level:

function reason(theory):
  proven_definite = {}
  proven_defeasible = {}
  worklist = facts + empty-body rule heads

  while worklist not empty:
    lit = pop(worklist)
    for rule triggered by lit:
      if body_satisfied(rule):
        fire(rule)

  emit -D and -d for literals not in proven sets

Strict rules add both +D and +d.
Defeasible rules add +d only if not blocked.

Conflict Handling

For a defeasible rule (normally r body q), attackers are rules for (not q).

r is blocked when:

1. An applicable defeater for ~q exists, and r is not superior to it.
2. An applicable defeasible attacker exists that is explicitly superior to r.

If no superiority relation exists between two applicable defeasible opponents, Spindle does not auto-block ties. Both sides can remain defeasibly derivable unless explicit superiority or defeaters resolve the conflict.

This means superiority declarations are the primary mechanism for deterministic conflict resolution.

Practical Semantics

• Add prefer r1 r2 / r1 > r2 when you want one side to win.
• Without superiority, opposing defeasible rules can yield both +d p and +d ~p.
• -d p means “not defeasibly provable”, not “false”.

Complexity

• Time: roughly O(n * m) where n is rules and m is average body size.
• Space: linear in literals/rules for indexes, worklists, and proven sets.

The implementation relies on indexing and bitsets for fast membership checks during propagation.

Variables and Grounding

Spindle supports first-order variables using Datalog-style bottom-up grounding.

Variable Syntax

Variables are prefixed with ?:

?x
?person
?any_value

Basic Example

; Facts with predicates
(given (parent alice bob))
(given (parent bob charlie))

; Rule with variables
(normally r1 (parent ?x ?y) (ancestor ?x ?y))

The rule r1 matches against facts:

• (parent alice bob) → (ancestor alice bob)
• (parent bob charlie) → (ancestor bob charlie)

Transitive Closure

A classic example - computing ancestors:

; Base facts
(given (parent alice bob))
(given (parent bob charlie))
(given (parent charlie david))

; Base case: parents are ancestors
(normally r1 (parent ?x ?y) (ancestor ?x ?y))

; Recursive case: ancestor of ancestor
(normally r2 (and (parent ?x ?y) (ancestor ?y ?z)) (ancestor ?x ?z))

Results:

• ancestor(alice, bob) - via r1
• ancestor(bob, charlie) - via r1
• ancestor(charlie, david) - via r1
• ancestor(alice, charlie) - via r2
• ancestor(bob, david) - via r2
• ancestor(alice, david) - via r2

How Grounding Works

Step 1: Collect Ground Facts

Extract all predicate instances from facts:

(given (parent alice bob))   →  parent(alice, bob)
(given (parent bob charlie)) →  parent(bob, charlie)

Step 2: Match Rule Bodies

For each rule, find all substitutions that satisfy the body:

(normally r1 (parent ?x ?y) (ancestor ?x ?y))

Substitutions:

• {?x → alice, ?y → bob}
• {?x → bob, ?y → charlie}

Step 3: Generate Ground Rules

Apply substitutions to create ground instances:

; Ground instances of r1
(normally r1_1 (parent alice bob) (ancestor alice bob))
(normally r1_2 (parent bob charlie) (ancestor bob charlie))

Step 4: Forward Chaining

Reason over the ground theory using standard algorithms.

Multiple Variables

(given (edge a b))
(given (edge b c))
(given (edge c d))

(normally path (and (edge ?x ?y) (edge ?y ?z)) (connected ?x ?z))

The join (edge ?x ?y) ∧ (edge ?y ?z) requires matching on ?y:

• {?x→a, ?y→b} joins with {?y→b, ?z→c} → connected(a, c)
• {?x→b, ?y→c} joins with {?y→c, ?z→d} → connected(b, d)

Wildcard Variable

Use _ when you don't care about a value:

(normally r1 (parent _ ?y) (has-parent ?y))

This matches any parent relationship.

Variable Scope

Variables are scoped to their rule:

; ?x in r1 is independent of ?x in r2
(normally r1 (parent ?x ?y) (ancestor ?x ?y))
(normally r2 (friend ?x ?y) (knows ?x ?y))

Safety Requirement

All head variables must appear in the body (range-restricted):

; VALID: ?x and ?y appear in body
(normally r1 (parent ?x ?y) (ancestor ?x ?y))

; INVALID: ?z not in body (unsafe)
(normally r2 (parent ?x ?y) (triple ?x ?y ?z))

Unsafe rules would generate infinite ground instances.

Negation with Variables

Negated predicates in the body:

(given (bird tweety))
(given (penguin tweety))
(given (bird eddie))

; Non-penguin birds fly
(normally r1 (and (bird ?x) (not (penguin ?x))) (flies ?x))

Important: The negated predicate must be ground after substitution. Spindle uses stratified negation.

Grounding with Superiority

Superiority applies to the rule template, affecting all ground instances:

(given (bird tweety))
(given (penguin tweety))

(normally r1 (bird ?x) (flies ?x))
(normally r2 (penguin ?x) (not (flies ?x)))
(prefer r2 r1)

Result: r2 beats r1 for all matching instances, so ¬flies(tweety).

Performance Considerations

Grounding can produce many rules:

Tips:

• Keep rule bodies small
• Use specific predicates to reduce matching
• Add explicit superiority where grounded conflicts should resolve to one side

Arithmetic in Grounded Rules

Arithmetic expressions are evaluated during grounding after variables are substituted.

Bind Constraints

(given (item widget 25))
(given (item gadget 10))
(given (tax-rate 0.1))

(normally r1
  (and (item ?name ?price) (tax-rate ?rate)
       (bind ?total (+ ?price (* ?price ?rate))))
  (total-cost ?name ?total))

Grounding:

1. Match (item widget 25) and (tax-rate 0.1) → {?name→widget, ?price→25, ?rate→0.1}
2. Evaluate (+ 25 (* 25 0.1)) → 27.5
3. Bind ?total → 27.5
4. Produce (total-cost widget 27.5)

Comparison Guards

Guards filter substitutions that don't satisfy the comparison:

(given (score alice 85))
(given (score bob 42))

(normally r1
  (and (score ?name ?s) (>= ?s 50))
  (passing ?name))

Only {?name→alice, ?s→85} satisfies (>= 85 50), so only (passing alice) is derived.

Evaluation Order

Body literals are evaluated left-to-right. Variables must be bound before they are used in arithmetic:

; CORRECT: ?price is bound by (item ...) before (bind ...) uses it
(normally r1
  (and (item ?name ?price)
       (bind ?discounted (* ?price 0.9)))
  (sale-price ?name ?discounted))

; INCORRECT: ?price is not yet bound when (bind ...) tries to use it
(normally r-bad
  (and (bind ?discounted (* ?price 0.9))
       (item ?name ?price))
  (sale-price ?name ?discounted))

Cross-Type Matching

Numeric terms match across types when values are equal:

(given (threshold 100))        ; Integer 100
(given (score alice 100.0))    ; Decimal 100.0

(normally r1
  (and (score ?name ?s) (threshold ?t) (>= ?s ?t))
  (above-threshold ?name))

Integer(100) matches Decimal(100.0) in comparisons, so this works as expected.

Variables vs. Manual Enumeration

SPL supports variables, so you can write a single rule:

; Single rule with variables
(normally r1 (parent ?x ?y) (ancestor ?x ?y))

Without variables, you would need to enumerate all ground instances manually:

(normally r1 (parent alice bob) (ancestor alice bob))
(normally r2 (parent bob charlie) (ancestor bob charlie))

Arithmetic Expressions

Spindle supports arithmetic expressions in rule bodies for numeric computation, variable binding, and comparison guards.

Overview

Arithmetic adds three capabilities to SPL rules:

1. Expressions — compute numeric values from operators and variables
2. Bind constraints — assign computed results to new variables
3. Comparison guards — filter substitutions based on numeric conditions

All arithmetic is restricted to rule bodies. Arithmetic cannot appear in facts, rule heads, or as standalone statements.

Numeric Types

Spindle has three numeric types with automatic promotion:

When Each Type Is Used

The parser chooses the numeric type based on how you write the literal:

• Integer: No decimal point, no exponent. 42, -7, 0.
• Decimal: Contains a decimal point but no exponent (e/E). 3.14, 0.001, -0.5.
• Float: Contains an exponent (e or E). 1.5e2 (= 150.0), 1e-3 (= 0.001), 2.0E10.

Decimal is the default for numbers with a decimal point because it gives exact representation. This matters for financial calculations and precise comparisons: 0.1 + 0.2 equals exactly 0.3 in Decimal, but not in floating point. Use scientific notation only when you specifically need IEEE 754 semantics or very large/small magnitudes.

Promotion Rules

When mixing types in an operation, values are promoted along the chain:

Integer → Decimal → Float

• Integer + Integer = Integer
• Integer + Decimal = Decimal
• Anything + Float = Float

Once a Float enters a computation, the entire result is Float. Keep this in mind if exact precision matters to your use case.

Cross-Type Matching

During grounding, numeric values match across types when equal:

(given (limit 100))          ; Integer
(given (score alice 100.0))  ; Decimal

; ?s (Decimal 100.0) matches ?limit (Integer 100) in the comparison
(normally r1
  (and (score ?name ?s) (limit ?limit) (>= ?s ?limit))
  (at-limit ?name))

Operators

N-ary Operators

These accept two or more arguments:

(+ 1 2 3)       ; => 6
(- 10 3 2)      ; => 5  (left fold: (10-3)-2)
(* 2 3 4)       ; => 24
(/ 100 5 2)     ; => 10 (left fold: (100/5)/2)
(min 5 3 8 1)   ; => 1
(max 5 3 8 1)   ; => 8

Subtraction and division use left fold semantics: (- a b c) = ((a - b) - c).

Binary Operators

These require exactly two arguments:

(div 7 2)    ; => 3   (integer division, floor toward -inf)
(rem 7 2)    ; => 1   (remainder)
(** 2 10)    ; => 1024 (exponentiation)

div and rem require integer operands.

Unary Operator

(abs -5)            ; => 5
(abs (- 3 10))      ; => 7

Nesting

Expressions can be arbitrarily nested:

(+ (* ?base ?rate) (abs (- ?adjustment ?threshold)))

Bind Constraints

bind assigns the result of an expression to a variable:

(bind ?total (+ ?price ?tax))

The variable must be unbound (not previously assigned in this rule). If it is already bound, the bind succeeds only if the existing value equals the computed result.

Example: Computing Derived Values

(given (item widget 25))
(given (item gadget 10))
(given (discount 0.15))

(normally calc-price
  (and (item ?name ?price) (discount ?rate)
       (bind ?savings (* ?price ?rate))
       (bind ?final (- ?price ?savings)))
  (final-price ?name ?final))

Results: (final-price widget 21.25), (final-price gadget 8.50)

Comparison Guards

Comparisons filter substitutions:

(> ?age 18)
(<= ?score 100)
(= ?x ?y)
(!= ?status 0)

Available operators: =, !=, <, >, <=, >=

Example: Filtering by Condition

(given (employee alice 95000))
(given (employee bob 45000))
(given (employee carol 120000))

(normally high-earner
  (and (employee ?name ?salary) (> ?salary 90000))
  (senior-band ?name))

Only alice and carol satisfy (> ?salary 90000).

Comparisons with Expressions

Both sides can be expressions:

(normally r1
  (and (budget ?b) (cost ?item ?c) (tax-rate ?r)
       (> ?b (+ ?c (* ?c ?r))))
  (affordable ?item))

Evaluation Order

Body elements are evaluated left to right. Variables must be bound by a preceding literal or bind before they can be used in arithmetic:

; CORRECT: ?price is bound before bind uses it
(normally r1
  (and (item ?name ?price)
       (bind ?discounted (* ?price 0.9)))
  (sale-price ?name ?discounted))

If an arithmetic expression references an unbound variable, the substitution is silently discarded (the rule does not fire for that ground instance).

Arithmetic in Predicate Arguments

Arithmetic expressions can appear directly as predicate arguments in the body:

(normally r1
  (and (base ?x ?b) (offset ?x ?o))
  (result ?x (+ ?b ?o)))

The expression (+ ?b ?o) is evaluated during grounding and the result becomes a concrete term in the head literal.

Restrictions

Spindle enforces several restrictions on where arithmetic can appear. Each is checked at parse time and produces a clear error message.

No Arithmetic in Heads or Facts (REQ-009)

Arithmetic constraints (bind, comparisons) are for filtering and computing in rule bodies. They cannot appear as conclusions.

; INVALID — bind in head position
(normally r1 (price ?p) (bind ?total (* ?p 1.1)))

; INVALID — bind as a fact
(given (bind ?x 42))

; INVALID — comparison in head position
(normally r1 bird (> 1 0))

Error message:

Arithmetic predicate 'bind' cannot appear in rule head or fact position (REQ-009)

The same message appears for comparison operators (=, !=, <, >, <=, >=) used as head literals.

No Negated Arithmetic (REQ-011)

Arithmetic constraints cannot be wrapped in not. This avoids ambiguity about what "not greater than" means in a defeasible logic context.

; INVALID — cannot negate a comparison
(normally r1 (and (val ?x) (not (> ?x 100))) (low ?x))

; INVALID — cannot negate bind
(normally r1 (and bird (not (bind ?x 10))) flies)

Error message:

Arithmetic predicate '>' cannot be negated (REQ-011). Use the positive form in the rule body instead.

Use the complementary comparison instead:

; CORRECT — use <= instead of (not >)
(normally r1 (and (val ?x) (<= ?x 100)) (low ?x))

No Temporal Variables in Arithmetic (REQ-006)

Variables bound by during expressions represent time points or intervals, not numeric values. They cannot be used as arithmetic operands. If a temporal variable appears in an arithmetic expression, the substitution is silently discarded (the rule does not fire for that ground instance).

; The rule below will never produce "shifted" because ?T is temporal
(given (during (event) 100 200))
(normally r1
  (and (during (event) ?T ?U) (bind ?next (+ ?T 1)))
  (shifted ?next))

Reserved Keywords (REQ-008)

Arithmetic operators and comparison symbols cannot be used as predicate names or rule labels. This prevents confusing programs where + or bind might look like user-defined predicates.

+  -  *  /  div  rem  abs  min  max  **
bind  =  !=  <  >  <=  >=

The following names are also reserved for future use: sum, count, avg, round, floor, ceil.

Error message:

Reserved keyword 'bind' cannot be used as a predicate name (REQ-008)

This also applies to tilde-negated forms (e.g., ~> is rejected because > is reserved) and to rule labels in prefer declarations.

Error Handling

Runtime Errors (During Grounding)

When any of these occur during grounding, the substitution is discarded — the rule simply does not fire for that ground instance. No error is raised to the user; the rule is silently skipped for that particular combination of variable bindings.

Parse-Time Errors

Parse-time errors halt processing and report the line number and a description of the problem.

Temporal Reasoning

Spindle supports timepoint ("as-of") reasoning, allowing you to reason about facts and rules active at a specific moment in time.

Time Points

Time points are represented as milliseconds since the Unix epoch (UTC).

Supported Formats

(moment "2024-06-15T14:30:00Z")    ; RFC3339 / ISO 8601 string (UTC)
1718461800000                      ; Integer epoch milliseconds
inf                                ; Positive infinity (never ends)
-inf                               ; Negative infinity (always existed)

Note: Multi-arity forms (e.g., (moment 2024 6 15)) are not currently supported.

During Operator

The during operator associates a literal with a time interval [start, end].

Syntax: (during literal start end)

Examples

; Alice worked at Acme from 2020 to 2022
(given (during (employed alice acme) (moment "2020-01-01T00:00:00Z") (moment "2022-01-01T00:00:00Z")))

; Alice works at Beta from 2022 onwards
(given (during (employed alice beta) (moment "2022-01-01T00:00:00Z") inf))

"As-Of" Reasoning

When reasoning with a reference time t, Spindle filters the theory:

1. Facts: A fact (during p start end) is active if start <= t <= end.
2. Rules: A rule is active if all its body literals and its head literal are active at t.

This allows querying the system state at any historical or future point.

Temporal Atom Identity (v0.3.0)

Starting in v0.3.0 (SPEC-018), temporal atoms with different time bounds are treated as distinct atoms during reasoning. Previously, p[1,10] and p[20,30] collapsed to the same internal identifier, which caused incorrect behaviour such as premature rule firing and cross-window satisfaction.

How It Works

The internal AtomKey used for indexing now includes temporal bounds as part of atom identity. Two literals that differ only in their temporal intervals produce distinct identifiers:

; These are now three distinct atoms:
(given (during p 1 10))      ; p[1,10]
(given (during p 20 30))     ; p[20,30]
(given p)                    ; p (base, no temporal bounds)

This means a rule that requires p in its body will not fire when only p[1,10] is proven, because they are different atoms. To connect temporal facts to their base predicates, Spindle uses bridging rules (see below).

What Changed

Temporal Bridging Rules

Because temporal atoms are now distinct from their base predicates, Spindle automatically generates synthetic bridging rules that connect temporal facts to their base forms. This ensures backward compatibility: proving a temporal fact still makes the base predicate available to non-temporal rules.

Automatic Bridge Generation

Given a temporal fact like >> p[1,10], the TemporalBridge pipeline stage generates a strict rule:

p[1,10] → p

This means: "if p holds during [1,10], then p holds in general." The bridge is a strict rule (not defeasible), because temporal subsumption is a semantic entailment.

Negation Bridges

For every positive bridge, a coupled negation bridge is also generated:

~p[1,10] → ~p

This ensures that evidence against a predicate in any temporal window propagates to the base level, enabling correct ambiguity blocking under skeptical semantics.

Example

Consider a theory about employment:

; Alice worked at Acme from 2020 to 2022
(given (during (employed alice acme)
               (moment "2020-01-01T00:00:00Z")
               (moment "2022-01-01T00:00:00Z")))

; If employed, then has_income
(rule r1 (=> (employed alice acme) (has_income alice)))

The TemporalBridge stage automatically generates:

; Synthetic bridge (strict):
; (employed alice acme)[2020,2022] → (employed alice acme)

This allows rule r1 to fire, because the bridge proves the base (employed alice acme) from the temporal fact. Without the bridge, r1 would never fire since its body expects the base atom.

Bridge Rule Labels

Bridge rules use a reserved label namespace __bridge:: to avoid collisions with user-defined rules:

• Positive bridge: __bridge::<literal_spl>
• Negation bridge: __bridge::neg::<literal_spl>

User-defined rules must not use labels starting with __bridge::.

Pipeline Placement

The TemporalBridge stage runs after grounding and before temporal variable validation:

Validate → WildcardRewrite → Ground → TemporalBridge → TemporalVarValidation → [TemporalFilter]

It is enabled by default. For theories with no temporal atoms, the stage is a no-op.

Temporal-Aware Query Operators (v0.3.0)

The query operators query, what_if, why_not, and abduce now use temporal-aware matching when comparing a query literal against conclusions.

Matching Behaviour

• Base query (no temporal bounds): Acts as a wildcard, matching any temporal variant of the predicate. This preserves backward compatibility.
• Temporal query (with bounds): Requires an exact temporal match.

; Given these conclusions after reasoning:
;   +d p[1,10]
;   +d p[20,30]
;   +d p         (via bridging)

; Querying "p" (base) matches all three — wildcard behaviour
; Querying "p[1,10]" matches only +d p[1,10] — exact temporal match
; Querying "p[5,15]" matches nothing — no exact match exists

This prevents false positives where querying p[1,10] would previously match p[20,30] because temporal bounds were ignored in comparisons.

Limitations

1. Timepoint only: Currently, Spindle supports reasoning at a timepoint. Interval inference (deriving new intervals from rules) is planned for a future release.
2. No Allen Relations in SPL: All 13 Allen relations are implemented in the core library (available via the Rust API), but are not yet exposed in SPL syntax. This requires interval variables (e.g., (during p ?t)) which are planned for a future release.
3. No Interval Variables: You cannot bind a variable to a time interval (e.g., (during p ?t) is not supported).

Modal Operators (Deontic Logic)

Spindle supports modal operators for deontic reasoning, allowing you to express obligations, permissions, and prohibitions within defeasible logic theories.

Introduction

Deontic logic is a branch of formal logic concerned with normative concepts such as obligation, permission, and prohibition. In defeasible reasoning, deontic modalities are particularly useful because normative rules are often subject to exceptions. For example, a general obligation to pay taxes may be defeated by a specific exemption for non-profit organizations.

Spindle integrates deontic modalities directly into its literal representation. Each literal can carry a modal operator that qualifies the proposition with a normative meaning, and these modal literals participate in the same defeasible reasoning process as ordinary literals -- including conflict resolution, superiority, and defeat.

Note: Modal operators are currently only accessible via the Rust API and WASM bindings. They are not directly supported through the CLI. If you need modal reasoning, use the library or WASM integration.

The Three Standard Operators

Spindle provides three built-in deontic operators:

Obligation (must)

An obligation states that something is required. If (must pay) is concluded, then there is an obligation to pay.

Permission (may)

A permission states that something is allowed. If (may access) is concluded, then access is permitted.

Forbidden (forbidden)

A prohibition states that something is not allowed. If (forbidden enter) is concluded, then entering is forbidden.

SPL Syntax

Modal operators use keyword wrappers:

; Obligation: (must <literal>)
(given (must pay))
(normally r1 signed-contract (must pay))

; Permission: (may <literal>)
(given (may access))
(normally r2 member (may access))

; Forbidden: (forbidden <literal>)
(given (forbidden enter))
(normally r3 unauthorized (forbidden enter))

SPL Negation

Negation of modal literals in SPL uses the not wrapper:

; Negated obligation: not obligated to pay
(normally r4 exemption (not (must pay)))

; Negated permission: not permitted to access
(normally r5 revoked (not (may access)))

; Negated prohibition: not forbidden to enter (i.e., allowed)
(normally r6 authorized (not (forbidden enter)))

Using Modal Operators in Rules

Modal operators can appear in both the body and head of rules, in all rule types.

Examples

; If you signed a contract, you are obligated to pay
(normally r1 signed-contract (must pay))

; If obligated to pay and haven't paid, violation
(normally r2 (and (must pay) (not paid)) violation)

; Members may access resources
(normally r3 member (may access))

; Unauthorized users are forbidden from entering
(normally r4 unauthorized (forbidden enter))

; An exemption defeats the obligation to pay
(normally r5 exemption (not (must pay)))
(prefer r5 r1)

; A defeater: pending review blocks the permission
(except d1 pending-review (may access))

Combining with Predicates and Variables

In SPL, modal operators can be combined with predicates and variables:

; Employees are obligated to report hours
(given (employee alice))
(given (employee bob))
(normally r1 (employee ?x) (must (report-hours ?x)))

; Managers may approve expenses
(given (manager alice))
(normally r2 (manager ?x) (may (approve-expenses ?x)))

; Contractors are forbidden from accessing internal systems
(given (contractor charlie))
(normally r3 (contractor ?x) (forbidden (access-internal ?x)))

Modal Negation and Complements

Every modal operator has a complement, obtained by toggling the negation flag. The complement of [O] (obligation) is [-O] (no obligation). This is distinct from the negation of the underlying proposition.

The distinction between modal negation and literal negation is important:

• Modal negation ([-O]pay): The obligation itself does not hold. You are not required to pay, but you may still choose to.
• Literal negation ([O]~pay): The obligation holds, but over the negated proposition. You are obligated not to pay.

Display Format

Rust API Usage

The Mode struct is in spindle_core::mode and is re-exported through the prelude.

Creating Modes

#![allow(unused)]
fn main() {
use spindle_core::prelude::*;

// Standard deontic operators
let obligation = Mode::obligation();  // [O]
let permission = Mode::permission();  // [P]
let forbidden = Mode::forbidden();    // [F]

// Empty mode (no modal operator)
let empty = Mode::empty();

// Custom mode
let custom = Mode::new("K");  // [K] (e.g., epistemic "known")
}

Complement (Negation Toggle)

#![allow(unused)]
fn main() {
use spindle_core::prelude::*;

let obligation = Mode::obligation();
assert_eq!(format!("{}", obligation), "[O]");

let neg_obligation = obligation.complement();
assert_eq!(format!("{}", neg_obligation), "[-O]");

// Double complement returns to original
let double = neg_obligation.complement();
assert_eq!(format!("{}", double), "[O]");
}

Checking Mode State

#![allow(unused)]
fn main() {
use spindle_core::prelude::*;

let mode = Mode::obligation();
assert!(!mode.is_empty());
assert!(!mode.negation);
assert_eq!(mode.name, Some("O".to_string()));

let empty = Mode::empty();
assert!(empty.is_empty());
}

Creating Modal Literals

#![allow(unused)]
fn main() {
use spindle_core::prelude::*;

// A literal with an obligation mode: [O]pay
let must_pay = Literal::new(
    "pay",
    false,
    Mode::obligation(),
    Temporal::empty(),
    vec![],
);
assert!(must_pay.is_modal());
assert_eq!(format!("{}", must_pay), "[O]pay");

// A negated literal with permission mode: [P]~access
let not_access = Literal::new(
    "access",
    true,
    Mode::permission(),
    Temporal::empty(),
    vec![],
);
assert_eq!(format!("{}", not_access), "[P]~access");

// Modal literal with predicates: [F]enter(restricted_area)
let forbidden_enter = Literal::new(
    "enter",
    false,
    Mode::forbidden(),
    Temporal::empty(),
    vec!["restricted_area".to_string()],
);
assert_eq!(format!("{}", forbidden_enter), "[F]enter(restricted_area)");
}

Modal Literals in Rules

#![allow(unused)]
fn main() {
use spindle_core::prelude::*;
use smallvec::smallvec;

// (normally r1 signed-contract (must pay))
let body = smallvec![Literal::simple("signed_contract")];
let head = smallvec![Literal::new(
    "pay",
    false,
    Mode::obligation(),
    Temporal::empty(),
    vec![],
)];
let rule = Rule::new("r1", RuleType::Defeasible, body, head);

// (normally r2 (and (must pay) (not paid)) violation)
let body = smallvec![
    Literal::new("pay", false, Mode::obligation(), Temporal::empty(), vec![]),
    Literal::negated("paid"),
];
let head = smallvec![Literal::simple("violation")];
let rule = Rule::new("r2", RuleType::Defeasible, body, head);
}

Equality and Hashing

Modal operators participate in literal equality and hashing. Two literals with the same name but different modes are considered distinct:

#![allow(unused)]
fn main() {
use spindle_core::prelude::*;
use std::collections::HashSet;

let pay = Literal::simple("pay");
let must_pay = Literal::new(
    "pay",
    false,
    Mode::obligation(),
    Temporal::empty(),
    vec![],
);

// These are different literals
assert_ne!(pay, must_pay);

let mut set = HashSet::new();
set.insert(pay.literal_id());
// must_pay has a different hash due to the mode
}

Use Cases

Compliance Rules

Model regulatory compliance where obligations can be defeated by exceptions:

; All companies must file annual reports
(normally r1 company (must file-annual-report))

; Small companies are exempt from detailed reporting
(normally r2 (and company small-company) (not (must file-annual-report)))
(prefer r2 r1)

; Public companies must disclose finances
(normally r3 public-company (must disclose-finances))

; Companies in bankruptcy are exempt from disclosure
(normally r4 (and public-company in-bankruptcy) (not (must disclose-finances)))
(prefer r4 r3)

Permission Systems

Model access control with defeasible permissions:

; Employees may access the office
(normally r1 employee (may access-office))

; Suspended employees lose access
(normally r2 (and employee suspended) (not (may access-office)))
(prefer r2 r1)

; Managers may access restricted areas
(normally r3 manager (may access-restricted))

; Even managers are forbidden from the server room without clearance
(normally r4 (and manager (not has-clearance)) (forbidden access-server-room))

Obligation Tracking

Track obligations through chains of reasoning:

; Signing a contract creates an obligation to pay
(normally r1 signed-contract (must pay))

; Obligation to pay and failure to pay results in violation
(normally r2 (and (must pay) (not paid)) in-violation)

; Being in violation creates an obligation to remedy
(normally r3 in-violation (must remedy))

; Payment within grace period removes the violation
(normally r4 (and in-violation paid-within-grace) (not in-violation))
(prefer r4 r2)

Mixed Normative Reasoning

Combine obligations, permissions, and prohibitions in a single theory:

; Citizens must pay taxes
(normally r1 citizen (must pay-taxes))

; Citizens may vote
(normally r2 citizen (may vote))

; Convicted felons are forbidden from voting (in some jurisdictions)
(normally r3 (and citizen convicted-felon) (forbidden vote))
(prefer r3 r2)

; Minors are exempt from taxation
(normally r4 (and citizen minor) (not (must pay-taxes)))
(prefer r4 r1)

; Non-citizens are forbidden from voting
(normally r5 (not citizen) (forbidden vote))

Limitations

1. No CLI support: Modal operators cannot be specified through the command-line interface. Use the Rust API or WASM bindings to construct modal literals.
2. No inter-modal axioms: Spindle does not enforce relationships between operators (e.g., it does not automatically derive [P]a from [O]a). If you need such relationships, encode them as explicit rules.
3. Custom modes are uninterpreted: Custom modes created with Mode::new(name) have no built-in semantics. Their meaning is determined entirely by the rules you write.
4. No modal logic tableau: Spindle performs defeasible reasoning, not modal logic model checking. Modal operators are labels on literals, not Kripke-style accessibility relations.

Best Practices

1. Be explicit about modal relationships

   ; If something is obligatory, it is also permitted
   (always obligation-implies-permission (must ?x) (may ?x))
   

2. Use superiority to handle conflicts between norms

   (normally r1 employee (must attend-meeting))
   (normally r2 (and employee on-leave) (not (must attend-meeting)))
   (prefer r2 r1)
   

3. Separate normative and factual reasoning

   ; Factual rules
   (normally r1 penguin bird)
   (normally r2 bird flies)
   
   ; Normative rules
   (normally r3 (and endangered-species (may hunt)) (not (may hunt)))
   

4. Document the intended interpretation of custom modes

   ; [K] = epistemic "known to be true"
   ; Use metadata to document the mode's meaning
   (meta r1 (description "Agents know their own obligations"))
   (normally r1 (must ?x) (K ?x))
   

Trust-Weighted Reasoning

Spindle supports trust-weighted defeasible reasoning, enabling source attribution, trust-weighted conclusions, partial defeat (diminishment), and multi-perspective evaluation.

Overview

In multi-agent and multi-source environments, not all information is equally reliable. Trust-weighted reasoning extends Spindle's defeasible logic with:

• Source attribution: Track which agents or systems contributed facts and rules
• Trust weighting: Assign trust values to sources and propagate them through derivations
• Weakest-link model: A conclusion's trust degree equals the minimum trust in its derivation chain
• Partial defeat (diminishment): Defeaters can reduce a conclusion's trust without fully defeating it
• Threshold evaluation: Named thresholds determine whether a conclusion is actionable
• Multi-perspective evaluation: Different trust policies can evaluate the same derivation differently
• Trust decay: Time-based trust adjustment with exponential, linear, and step-function models
• Trust directives: Declarative trust configuration in SPL format
• Pipeline integration: Automatic trust-weighted conclusions from the reasoning pipeline
• Trust-filtered queries: Filter reasoning results by source and minimum trust degree
• CLI trust output: Display trust weights alongside conclusions with --trust

Source Attribution and Claims

Source Identifiers

Sources use a category:name format to identify agents, systems, or users:

agent:security    - A security scanning agent
agent:coder       - A code analysis agent
agent:qa          - A QA testing agent
system:policy     - System-level policy rules
user:admin        - An administrative user

SPL Claims Syntax

The claims block attributes statements to a source identity:

(claims agent:security
  :at "2026-01-20T09:00:00Z"
  :note "Automated security scan results"
  (given vulnerability_detected)
  (normally sec1 vulnerability_detected security_risk))

Syntax: (claims source claims-meta? statements...)

Metadata fields (all optional):

Allowed inner statements:

• Facts: (given literal)
• Rules: (normally label body head), (always label body head), (except label body head)
• Superiorities: (prefer label1 label2)

Claims blocks cannot be nested.

Multi-Agent Example

Multiple agents contribute claims about a pull request:

(claims agent:security
  :at "2026-01-20T09:00:00Z"
  :note "Automated security scan results"
  (given vulnerability_detected)
  (normally sec1 vulnerability_detected security_risk))

(claims agent:coder
  :at "2026-01-20T09:30:00Z"
  :note "CI pipeline results"
  (given tests_pass)
  (normally dev1 tests_pass code_compiles))

; Global superiority (outside claims blocks)
(prefer sec1 dev1)

Rust API: Source and SourcedConclusion

#![allow(unused)]
fn main() {
use spindle_core::trust::{Source, SourcedConclusion};
use spindle_core::conclusion::ConclusionType;
use spindle_core::literal::Literal;

// Create sources
let alice = Source::new("agent:alice");
let bob = Source::with_label("agent:bob", "Bob the Reviewer");

// Display formatting
println!("{}", alice);  // "agent:alice"
println!("{}", bob);    // "Bob the Reviewer (agent:bob)"

// Track source attribution on conclusions
let conclusion = SourcedConclusion::new(
        Literal::simple("approved"),
        ConclusionType::DefeasiblyProvable,
    )
    .with_source(Source::new("agent:coder"))
    .with_source(Source::new("agent:reviewer"))
    .with_source(Source::new("agent:security"))
    .with_derivation("r1")
    .with_derivation("r2");

assert_eq!(conclusion.sources.len(), 3);
assert_eq!(conclusion.derivation, vec!["r1", "r2"]);
}

Trust Policies and Configuration

A TrustPolicy defines how much to trust each source, what thresholds to apply, and the default trust for unknown sources.

Creating a Trust Policy

#![allow(unused)]
fn main() {
use spindle_core::trust::TrustPolicy;

let policy = TrustPolicy::new(0.5)              // default trust for unknown sources
    .with_trust("agent:coder", 0.9)              // high trust
    .with_trust("agent:security", 0.95)          // very high trust
    .with_trust("system:policy", 1.0)            // full trust
    .with_trust("external:api", 0.6)             // moderate trust
    .with_threshold("action", 0.7)               // threshold for taking action
    .with_threshold("warn", 0.5)                 // threshold for warnings
    .with_threshold("log", 0.3);                 // threshold for logging
}

Querying Trust

#![allow(unused)]
fn main() {
// Look up trust for a known source
assert_eq!(policy.get_trust("agent:coder"), 0.9);
assert_eq!(policy.get_trust("agent:security"), 0.95);

// Unknown sources fall back to default_trust
assert_eq!(policy.get_trust("unknown_agent"), 0.5);
}

Trust Value Range

Trust values are f64 in the range [0.0, 1.0]:

Trust Directives in SPL

Trust policies can be declared directly in SPL source files using three directive forms.

(trusts source value)

Assigns a trust value to a source identifier:

(trusts agent:security 0.95)
(trusts agent:coder 0.9)
(trusts system:policy 1.0)
(trusts external:api 0.6)

Values must be in the range [0.0, 1.0].

(decays source model param)

Attaches a time-based decay model to a source. The decay model reduces trust as assertions age:

; Trust halves every hour (3600 seconds)
(decays agent:sensor exponential 3600.0)

; Trust decreases at 0.001 per second
(decays agent:temp linear 0.001)

; Trust drops to zero after 24 hours
(decays agent:ephemeral step 86400.0)

See Decay Models for formula details.

(threshold name value)

Defines a named threshold for decision-making:

(threshold action 0.7)
(threshold warn 0.5)
(threshold log 0.3)

Complete SPL Example

; Trust configuration
(trusts agent:security 0.95)
(trusts agent:coder 0.9)
(decays agent:sensor exponential 3600.0)
(threshold action 0.7)
(threshold warn 0.5)

; Claims from sources
(claims agent:security
  :at "2026-01-20T09:00:00Z"
  (given vulnerability_detected)
  (normally sec1 vulnerability_detected security_risk))

(claims agent:coder
  :at "2026-01-20T09:30:00Z"
  (given tests_pass)
  (normally dev1 tests_pass code_compiles))

(prefer sec1 dev1)

Decay Models

Decay models compute a time-dependent multiplier in [0.0, 1.0] that is applied to a source's base trust value. This models the intuition that older assertions become less trustworthy over time.

Exponential Decay

multiplier = 0.5 ^ (age_secs / half_life_secs)

After one half-life, trust is halved. After two half-lives, trust is quartered. Trust approaches zero asymptotically.

#![allow(unused)]
fn main() {
use spindle_core::trust::{DecayModel, TrustPolicy};

let policy = TrustPolicy::new(0.5)
    .with_trust("agent:sensor", 0.9)
    .with_decay("agent:sensor", DecayModel::Exponential { half_life_secs: 3600.0 });

// At age 0: effective trust = 0.9
assert_eq!(policy.get_effective_trust("agent:sensor", 0.0), 0.9);

// At 1 hour: effective trust = 0.9 * 0.5 = 0.45
let at_1h = policy.get_effective_trust("agent:sensor", 3600.0);
assert!((at_1h - 0.45).abs() < 1e-10);
}

Linear Decay

multiplier = max(1.0 - rate_per_sec * age_secs, 0.0)

Trust decreases at a constant rate per second, reaching zero at 1.0 / rate seconds.

#![allow(unused)]
fn main() {
let policy = TrustPolicy::new(0.5)
    .with_trust("agent:temp", 1.0)
    .with_decay("agent:temp", DecayModel::Linear { rate_per_sec: 0.001 });

// At 500 seconds: 1.0 * (1.0 - 0.001 * 500) = 0.5
let at_500s = policy.get_effective_trust("agent:temp", 500.0);
assert!((at_500s - 0.5).abs() < 1e-10);

// At 1500 seconds: fully decayed to 0.0
assert_eq!(policy.get_effective_trust("agent:temp", 1500.0), 0.0);
}

Step Function

multiplier = 1.0 if age_secs < cutoff_secs, else 0.0

Trust is full until the cutoff, then drops to zero instantly. Useful for time-limited credentials or ephemeral assertions.

#![allow(unused)]
fn main() {
let policy = TrustPolicy::new(0.5)
    .with_trust("agent:session", 0.9)
    .with_decay("agent:session", DecayModel::StepFunction { cutoff_secs: 86400.0 });

// Before cutoff: full trust
assert_eq!(policy.get_effective_trust("agent:session", 100.0), 0.9);

// At cutoff: zero trust
assert_eq!(policy.get_effective_trust("agent:session", 86400.0), 0.0);
}

Weakest-Link Trust Model

The trust degree of a derived conclusion equals the minimum trust value encountered along its entire derivation chain. This is the "weakest-link" model: a conclusion is only as trustworthy as the least trusted step that produced it.

How It Works

Given a derivation tree, each node has a trust value from its contributing source. The weakest_link_trust() method recursively computes the minimum:

       root (0.8)
      /         \
branch1 (0.9)   branch2 (0.6)
    |                |
leaf1 (0.95)    leaf2 (0.7)

The weakest link is 0.6 (from branch2).

Rust API: TrustDerivationNode

#![allow(unused)]
fn main() {
use spindle_core::trust::{TrustDerivationNode, Source};
use spindle_core::literal::Literal;

// Build a derivation tree
let leaf1 = TrustDerivationNode::new(Literal::simple("bird"), 0.9)
    .with_source(Source::new("agent:alice"));
let leaf2 = TrustDerivationNode::new(Literal::simple("healthy"), 0.7)
    .with_source(Source::new("agent:bob"));

let root = TrustDerivationNode::new(Literal::simple("flies"), 0.8)
    .with_children(vec![leaf1, leaf2]);

// Weakest link is 0.7 (from "healthy" via agent:bob)
assert_eq!(root.weakest_link_trust(), 0.7);
}

Chain Propagation

In a linear derivation chain, the weakest link propagates upward:

#![allow(unused)]
fn main() {
// Chain: a (0.9) -> b (0.9) -> c (0.5)
let leaf = TrustDerivationNode::new(Literal::simple("a"), 0.9)
    .with_source(Source::new("agent:hightrust"));
let mid = TrustDerivationNode::new(Literal::simple("b"), 0.9)
    .with_children(vec![leaf]);
let root = TrustDerivationNode::new(Literal::simple("c"), 0.5)
    .with_source(Source::new("agent:lowtrust"))
    .with_children(vec![mid]);

// Weakest link is 0.5 (from node "c")
assert_eq!(root.weakest_link_trust(), 0.5);
}

Single Source

When a conclusion comes from a single source with no derivation chain, the degree equals the source's trust value directly:

#![allow(unused)]
fn main() {
let node = TrustDerivationNode::new(Literal::simple("tests_pass"), 0.9)
    .with_source(Source::new("agent:coder"));

assert_eq!(node.weakest_link_trust(), 0.9);
}

Partial Defeat (Diminishment)

Standard defeasible logic uses binary defeat: a conclusion is either proven or not. Trust-weighted reasoning introduces diminishment, where a defeater can reduce a conclusion's trust degree without fully defeating it.

Diminishment Formula

diminishment = min(defeater_degree * target_degree, target_degree)
resulting_degree = (target_degree - diminishment).max(0.0)

If the defeater fully defeats the target, the resulting degree is 0.0.

Example Calculation

Given a target with degree 0.8 and a defeater with degree 0.4:

diminishment = min(0.4 * 0.8, 0.8) = min(0.32, 0.8) = 0.32
resulting_degree = (0.8 - 0.32).max(0.0) = 0.48

The conclusion survives but with reduced trust.

Rust API: DiminisherInfo

#![allow(unused)]
fn main() {
use spindle_core::trust::DiminisherInfo;

// Partial diminishment
let dim = DiminisherInfo::new("defeater_rule", 0.4, 0.8);
assert_eq!(dim.defeater_label, "defeater_rule");
assert_eq!(dim.defeater_degree, 0.4);
assert_eq!(dim.target_degree, 0.8);
assert!(!dim.full_defeat);
// resulting_degree = 0.8 - min(0.4 * 0.8, 0.8) = 0.48
assert!((dim.resulting_degree() - 0.48).abs() < 0.001);

// Full defeat
let full = DiminisherInfo::new("strong_defeater", 0.9, 0.7).as_full_defeat();
assert!(full.full_defeat);
assert_eq!(full.resulting_degree(), 0.0);
}

Diminished Conclusions

A WeightedConclusion tracks all diminishers that affected it:

#![allow(unused)]
fn main() {
use spindle_core::trust::WeightedConclusion;
use spindle_core::conclusion::ConclusionType;
use spindle_core::literal::Literal;

let mut wc = WeightedConclusion::new(
    Literal::simple("approved"),
    ConclusionType::DefeasiblyProvable,
    0.9,
);

assert!(!wc.was_diminished());

// Apply diminishers
wc.diminished_by.push(DiminisherInfo::new("d1", 0.3, 0.9));
wc.diminished_by.push(DiminisherInfo::new("d2", 0.4, 0.9));

assert!(wc.was_diminished());
assert_eq!(wc.diminished_by.len(), 2);
}

Resulting Degree is Never Negative

Even with strong diminishment, the resulting degree is clamped to 0.0:

#![allow(unused)]
fn main() {
let dim = DiminisherInfo::new("strong", 1.0, 0.5);
assert!(dim.resulting_degree() >= 0.0);
}

Threshold-Based Decisions

Named thresholds allow you to make decisions based on trust levels without hardcoding numeric comparisons throughout your application.

Defining Thresholds

#![allow(unused)]
fn main() {
let policy = TrustPolicy::new(0.5)
    .with_threshold("action", 0.7)   // safe to act on
    .with_threshold("warn", 0.5)     // worth a warning
    .with_threshold("log", 0.3);     // worth logging
}

Evaluating Against Thresholds

#![allow(unused)]
fn main() {
// A conclusion with degree 0.6
assert_eq!(policy.is_above_threshold(0.6, "action"), Some(false));  // below action
assert_eq!(policy.is_above_threshold(0.6, "warn"), Some(true));     // above warn
assert_eq!(policy.is_above_threshold(0.6, "log"), Some(true));      // above log

// Unknown thresholds return None
assert_eq!(policy.is_above_threshold(0.9, "unknown"), None);
}

Boundary Behavior

Threshold evaluation uses >= (greater than or equal):

#![allow(unused)]
fn main() {
let policy = TrustPolicy::new(0.5)
    .with_threshold("exact", 0.7);

// Exactly at threshold is considered above
assert_eq!(policy.is_above_threshold(0.7, "exact"), Some(true));
assert_eq!(policy.is_above_threshold(0.69999, "exact"), Some(false));
}

Per-Conclusion Threshold Results

WeightedConclusion stores pre-computed threshold results:

#![allow(unused)]
fn main() {
let mut wc = WeightedConclusion::new(
    Literal::simple("important_fact"),
    ConclusionType::DefeasiblyProvable,
    0.9,
);

wc.above_threshold.insert("action".to_string(), true);
wc.above_threshold.insert("warn".to_string(), true);
wc.above_threshold.insert("critical".to_string(), false);

assert_eq!(wc.is_above_threshold("action"), Some(true));
assert_eq!(wc.is_above_threshold("critical"), Some(false));
assert_eq!(wc.is_above_threshold("unknown"), None);
}

Multi-Perspective Evaluation

The same derivation can be evaluated under different trust policies, yielding different conclusions. This models real-world scenarios where different stakeholders have different trust assessments.

Different Perspectives on the Same Sources

#![allow(unused)]
fn main() {
// Security team perspective: trusts security agents highly
let security_perspective = TrustPolicy::new(0.5)
    .with_trust("agent:security", 0.95)
    .with_trust("agent:coder", 0.6);

// Developer perspective: trusts coders highly
let developer_perspective = TrustPolicy::new(0.5)
    .with_trust("agent:security", 0.5)
    .with_trust("agent:coder", 0.9);

// Same source, different trust values
assert!(
    security_perspective.get_trust("agent:security")
    > security_perspective.get_trust("agent:coder")
);
assert!(
    developer_perspective.get_trust("agent:coder")
    > developer_perspective.get_trust("agent:security")
);
}

Conservative vs. Permissive Policies

#![allow(unused)]
fn main() {
// Conservative: high thresholds, low default trust
let conservative = TrustPolicy::new(0.3)
    .with_threshold("action", 0.9)
    .with_threshold("warn", 0.7);

// Permissive: low thresholds, high default trust
let permissive = TrustPolicy::new(0.8)
    .with_threshold("action", 0.5)
    .with_threshold("warn", 0.3);

let degree = 0.75;

// Conservative: above warn, below action
assert_eq!(conservative.is_above_threshold(degree, "action"), Some(false));
assert_eq!(conservative.is_above_threshold(degree, "warn"), Some(true));

// Permissive: above both
assert_eq!(permissive.is_above_threshold(degree, "action"), Some(true));
assert_eq!(permissive.is_above_threshold(degree, "warn"), Some(true));
}

This enables the same reasoning results to drive different behavior depending on which stakeholder's perspective is applied.

Trust Explanations

TrustExplanation provides a complete explanation of how a conclusion's trust degree was derived, including the derivation tree and any diminishers that affected it.

Generating Explanations

#![allow(unused)]
fn main() {
use spindle_core::trust::{TrustExplanation, TrustDerivationNode, DiminisherInfo, Source};
use spindle_core::literal::Literal;

// Build derivation tree
let leaf = TrustDerivationNode::new(Literal::simple("premise"), 0.9)
    .with_source(Source::with_label("src1", "Source One"));
let root = TrustDerivationNode::new(Literal::simple("conclusion"), 0.85)
    .with_children(vec![leaf]);

// Create explanation
let explanation = TrustExplanation::new(Literal::simple("conclusion"), 0.85)
    .with_tree(root);

println!("{}", explanation.to_natural_language());
}

Natural Language Output

The to_natural_language() method produces human-readable output:

Trust Explanation for "conclusion"
Final trust degree: 0.85

Derivation tree:
  1. "conclusion" (trust: 0.85)
     1. "premise" (trust: 0.90) [source: Source One (src1)]

Explanations with Diminishers

#![allow(unused)]
fn main() {
let dim1 = DiminisherInfo::new("d1", 0.4, 0.9);
let dim2 = DiminisherInfo::new("d2", 0.3, 0.9).as_full_defeat();

let explanation = TrustExplanation::new(Literal::simple("goal"), 0.0)
    .with_diminishers(vec![dim1, dim2]);

println!("{}", explanation.to_natural_language());
}

Output includes diminisher details:

Trust Explanation for "goal"
Final trust degree: 0.00

Diminishers:
  1. Diminished by 'd1' (degree 0.40): 0.90 -> 0.45
  2. Fully defeated by 'd2' (degree 0.30)

Non-Provable Literals

When a literal is not provable, the explanation has a zero degree and no derivation tree:

#![allow(unused)]
fn main() {
let explanation = TrustExplanation::new(Literal::simple("not_provable"), 0.0);
assert_eq!(explanation.final_degree, 0.0);
assert!(explanation.derivation_tree.is_none());
}

Pipeline Integration

The reasoning pipeline can automatically compute trust-weighted conclusions after reasoning. The compute_weighted_conclusions function examines each conclusion's derivation rule, looks up the source metadata, and applies the theory's trust policy.

Rust API

#![allow(unused)]
fn main() {
use spindle_core::pipeline::{prepare, PrepareOptions, compute_weighted_conclusions};

// Parse a theory with trust directives
let theory = spindle_parser::parse_spl(r#"
    (trusts agent:security 0.95)
    (trusts agent:coder 0.9)
    (threshold action 0.7)

    (claims agent:security
      (given vulnerability_detected)
      (normally sec1 vulnerability_detected security_risk))
"#).unwrap();

// Run the pipeline
let opts = PrepareOptions::default();
let result = prepare(&theory, opts).unwrap();

// Reason
let conclusions = spindle_core::reason::reason_prepared(&result.theory).unwrap();

// Compute trust-weighted conclusions
let policy = result.theory.trust_policy();
let weighted = compute_weighted_conclusions(&conclusions, &result.theory, policy);

for wc in &weighted {
    println!("{}: trust={:.2}, sources={:?}",
        wc.literal, wc.degree,
        wc.sources.iter().map(|s| &s.id).collect::<Vec<_>>());
}
}

Each WeightedConclusion contains:

• degree: Trust value from the source's policy entry (or default)
• sources: Set of contributing source identifiers
• above_threshold: Pre-computed pass/fail for each named threshold

CLI Usage

--trust Flag

The reason command accepts a --trust flag that displays trust weights alongside conclusions:

spindle reason --trust theory.spl

Output format:

Conclusions:

  +D bird (trust: 0.95) [agent:security]
  +d flies (trust: 0.90) [agent:coder]
  -d -flies (trust: 0.90) [agent:coder]

Each conclusion shows:

• The provability symbol (+D, -D, +d, -d)
• The literal
• The trust degree in parentheses
• The contributing sources in brackets

Without --trust, conclusions display in the standard format without trust information.

Trust-Filtered Queries

The TrustFilter struct allows filtering reasoning results by minimum trust degree and source pattern.

Rust API

#![allow(unused)]
fn main() {
use spindle_core::query::TrustFilter;
use spindle_core::trust::TrustPolicy;

let policy = TrustPolicy::new(0.5)
    .with_trust("agent:trusted", 0.9)
    .with_trust("agent:untrusted", 0.3);

// Filter: only conclusions from agent: sources with trust >= 0.7
let filter = TrustFilter::new()
    .with_min_degree(0.7)
    .with_source("agent:")
    .with_policy(policy);

// Check if a specific rule's conclusion passes the filter
let passes = filter.passes(&theory, Some("rule_label"));
}

Filter Fields

When no policy is set, all conclusions pass the filter (permissive by default).

Mining Confidence Metrics

When rules are learned from process mining, each rule can be annotated with support and confidence metrics.

LearnedRule

#![allow(unused)]
fn main() {
use spindle_core::mining::{LearnedRule, calculate_support, calculate_confidence};

// Calculate support: number of traces where "submit" directly precedes "review"
let support = calculate_support(&event_log, "submit", "review");

// Calculate confidence: support / total transitions from "submit"
let confidence = calculate_confidence(&event_log, "submit", "review");
}

Filtering by Metrics

#![allow(unused)]
fn main() {
use spindle_core::mining::rules_with_metrics;

// Get only rules with support >= 5 and confidence >= 0.8
let learned = rules_with_metrics(&event_log, &mined_rules, 5, 0.8);

for lr in &learned {
    println!("{}", lr); // "r1 (support: 10, confidence: 0.95)"
}
}

Petri Net Mining with Metrics

#![allow(unused)]
fn main() {
use spindle_core::mining::petri_net_to_rules;

// Mine rules with minimum support=3, confidence=0.7
let learned_rules = petri_net_to_rules(&event_log, 3, 0.7);

for lr in &learned_rules {
    println!("{}: support={}, confidence={:.2}, source={}",
        lr.rule.label, lr.support, lr.confidence, lr.source);
}
}

Use Cases

Multi-Agent Systems

In a code review pipeline, multiple agents contribute assessments with varying trust levels:

; Security scanner has high credibility for vulnerability findings
(claims agent:security
  :at "2026-01-20T09:00:00Z"
  :note "Automated security scan results"
  (given vulnerability_detected)
  (normally sec1 vulnerability_detected security_risk))

; CI pipeline reports test results
(claims agent:coder
  :at "2026-01-20T09:30:00Z"
  :note "CI pipeline results"
  (given tests_pass)
  (normally dev1 tests_pass code_compiles))

; Superiority: security findings override development claims
(prefer sec1 dev1)

A trust policy assigns credibility:

#![allow(unused)]
fn main() {
let policy = TrustPolicy::new(0.5)
    .with_trust("agent:security", 0.95)
    .with_trust("agent:coder", 0.9)
    .with_trust("agent:qa", 0.85)
    .with_threshold("action", 0.7)
    .with_threshold("warn", 0.5);
}

Auditing

Trust explanations provide a full audit trail for every conclusion:

• Which sources contributed
• What derivation chain was followed
• What the trust degree is at each step
• Whether any diminishers reduced the conclusion
• Whether the conclusion meets each named threshold

This is useful for compliance requirements where decisions must be traceable and explainable.

Regulatory Compliance

Different regulatory frameworks can be modeled as different trust policies applied to the same reasoning results:

#![allow(unused)]
fn main() {
// Strict regulatory perspective
let regulatory = TrustPolicy::new(0.3)
    .with_trust("system:policy", 1.0)
    .with_trust("agent:auditor", 0.95)
    .with_trust("external:vendor", 0.4)
    .with_threshold("compliant", 0.9)
    .with_threshold("review_needed", 0.7);

// Internal operations perspective
let operations = TrustPolicy::new(0.7)
    .with_trust("system:policy", 1.0)
    .with_trust("agent:auditor", 0.8)
    .with_trust("external:vendor", 0.7)
    .with_threshold("compliant", 0.6)
    .with_threshold("review_needed", 0.4);

// Same conclusion degree, different compliance outcomes
let degree = 0.75;
assert_eq!(regulatory.is_above_threshold(degree, "compliant"), Some(false));
assert_eq!(operations.is_above_threshold(degree, "compliant"), Some(true));
}

End-to-End Example

This example demonstrates the complete trust workflow from theory definition through CLI output.

1. Define a theory with trust directives (review.spl):

; Trust configuration
(trusts agent:security 0.95)
(trusts agent:coder 0.85)
(trusts agent:qa 0.80)
(decays agent:qa exponential 86400.0)
(threshold deploy 0.8)
(threshold warn 0.5)

; Security agent's findings
(claims agent:security
  :at "2026-02-01T10:00:00Z"
  (given no_vulnerabilities)
  (normally sec1 no_vulnerabilities security_clear))

; Coder agent's results
(claims agent:coder
  :at "2026-02-01T10:30:00Z"
  (given tests_pass)
  (given lint_clean)
  (normally dev1 (and tests_pass lint_clean) code_ready))

; QA agent's assessment
(claims agent:qa
  :at "2026-02-01T11:00:00Z"
  (given manual_review_ok)
  (normally qa1 manual_review_ok qa_approved))

; Deployment rule: attributed to a system policy source
; Every rule must be inside a claims block to participate in trust.
; Rules outside claims blocks have no source and receive trust 0.0.
(trusts system:policy 1.0)
(claims system:policy
  (normally deploy1
    (and security_clear code_ready qa_approved)
    ready_to_deploy))

Important: The default trust for unsourced rules is 0.0. Any rule defined outside a claims block has no source attribution and will receive a trust degree of zero — making it the weakest link in any derivation chain that passes through it. Always wrap rules in a claims block when using trust-weighted reasoning. For structural or policy rules that are axiomatic, attribute them to a fully-trusted system source like system:policy.

2. Run with trust output:

spindle reason --trust review.spl

3. Output:

Conclusions:

  +D lint_clean (trust: 0.85) [agent:coder]
  +D manual_review_ok (trust: 0.80) [agent:qa]
  +D no_vulnerabilities (trust: 0.95) [agent:security]
  +D tests_pass (trust: 0.85) [agent:coder]
  +d lint_clean (trust: 0.85) [agent:coder]
  +d tests_pass (trust: 0.85) [agent:coder]
  +d no_vulnerabilities (trust: 0.95) [agent:security]
  +d manual_review_ok (trust: 0.80) [agent:qa]
  +d code_ready (trust: 0.85) [agent:coder]
  +d security_clear (trust: 0.95) [agent:security]
  +d qa_approved (trust: 0.80) [agent:qa]
  +d ready_to_deploy (trust: 0.80) [agent:coder, agent:qa, agent:security, system:policy]
  -D ready_to_deploy (trust: 0.00)
  -D security_clear (trust: 0.00)
  -D code_ready (trust: 0.00)
  -D qa_approved (trust: 0.00)

The deployment conclusion (ready_to_deploy) has trust 0.80 — the weakest link across the derivation chain: min(1.0, 0.95, 0.85, 0.80) = 0.80. This meets the deploy threshold (0.8) and can proceed.

Limitations

1. Static trust values: Trust values are fixed per policy. Dynamic trust that updates based on track record is not built in (use decay models for time-based adjustment).
2. Weakest-link only: The model uses minimum trust propagation. Alternative models (e.g., weighted average, product) are not supported.
3. No cryptographic verification: The :sig metadata field is stored but not verified against any cryptographic infrastructure.
4. Floating-point precision: Trust values are f64, so standard floating-point precision considerations apply to boundary comparisons.
5. Decay requires reference time: Decay models need the age of assertions to be computed externally; the pipeline does not automatically track assertion timestamps for decay purposes.

Query Operators

Spindle provides three query operators for interactive reasoning: what-if, why-not, and abduction.

What-If Queries

What-if performs hypothetical reasoning: "What would be concluded if these facts were true?"

API

#![allow(unused)]
fn main() {
use spindle_core::query::{what_if, HypotheticalClaim};
use spindle_core::literal::Literal;

let hypotheticals = vec![
    HypotheticalClaim::new(Literal::simple("wounded"))
];
let goal = Literal::negated("flies");
let result = what_if(&theory, hypotheticals, &goal);
}

How It Works

1. Create a copy of the theory
2. Add hypothetical facts
3. Reason over the modified theory
4. Return new conclusions

Example

Original theory:

(given bird)
(normally r1 bird flies)
(normally r2 wounded (not flies))
(prefer r2 r1)

Query: What if wounded is true?

#![allow(unused)]
fn main() {
let hypotheticals = vec![HypotheticalClaim::new(Literal::simple("wounded"))];
let goal = Literal::negated("flies");
let result = what_if(&theory, hypotheticals, &goal);
// result.is_provable() = true
// result.new_conclusions = [Literal("~flies")]
}

Use Cases

• Exploring consequences of decisions
• Scenario analysis
• Testing rule interactions

Why-Not Queries

Why-not explains why a literal is NOT provable.

API

#![allow(unused)]
fn main() {
use spindle_core::query::why_not;
use spindle_core::literal::Literal;

let literal = Literal::simple("flies");
let explanation = why_not(&theory, &literal);
}

How It Works

1. Check if the literal is actually unprovable
2. Find rules that could prove it
3. For each rule, identify what's blocking it:
   • Missing body literals
   • Defeated by superior rules
   • Blocked by defeaters

Example

Theory:

(given bird)
(given penguin)
(normally r1 bird flies)
(normally r2 penguin (not flies))
(prefer r2 r1)

Query: Why is flies not provable?

#![allow(unused)]
fn main() {
let literal = Literal::simple("flies");
let explanation = why_not(&theory, &literal);
// explanation.literal = Literal("flies")
// explanation.would_derive = Some("r1")
// explanation.blocked_by = [BlockingCondition { ... }]
}

Result Structure

#![allow(unused)]
fn main() {
struct WhyNotResult {
    literal: Literal,              // What we're asking about
    would_derive: Option<String>,  // Rule that could prove it
    blocked_by: Vec<BlockingCondition>,  // What's blocking
}

struct BlockingCondition {
    blocking_type: BlockingType,   // Type of blocking
    rule_label: String,            // The blocked rule
    missing_literals: Vec<Literal>, // Missing premises (if applicable)
    blocking_rule: Option<String>, // Blocking rule (if applicable)
    explanation: String,           // Human-readable explanation
}

enum BlockingType {
    MissingPremise,    // Body not satisfied
    Defeated,          // Defeated by defeater
    Contradicted,      // Complement is proven
}
}

Use Cases

• Debugging unexpected results
• Understanding rule interactions
• Explaining decisions to users

Abduction

Abduction finds hypotheses that would make a goal provable.

API

#![allow(unused)]
fn main() {
use spindle_core::query::abduce;
use spindle_core::literal::Literal;

let goal = Literal::simple("goal");
let result = abduce(&theory, &goal, max_solutions);
}

How It Works

1. Start with the goal literal
2. Find rules that could prove it
3. For each rule, identify missing body literals
4. Recursively abduce missing literals
5. Return minimal sets of assumptions

Example

Theory:

(normally r1 bird flies)
(normally r2 penguin (not flies))
(normally r3 (and bird healthy) strong-flyer)
(prefer r2 r1)

Query: What facts would make flies provable?

#![allow(unused)]
fn main() {
let goal = Literal::simple("flies");
let result = abduce(&theory, &goal, 3);
// result.solutions[0].facts = HashSet { Literal("bird") }
}

Solution Structure

#![allow(unused)]
fn main() {
struct AbductionResult {
    goal: Literal,
    solutions: Vec<AbductionSolution>,
}

struct AbductionSolution {
    facts: HashSet<Literal>,      // Facts to assume
    rules_used: HashSet<String>,  // Rules involved
    confidence: f64,              // Trust score (if weighted)
}
}

Handling Conflicts

Abduction considers superiority:

(given penguin)
(normally r1 bird flies)
(normally r2 penguin (not flies))
(prefer r2 r1)

Abducing flies might return:

• ["bird", "healthy"] with a rule (normally r3 (and bird healthy) flies) where r3 > r2
• Or indicate that flies cannot be achieved given penguin

Use Cases

• Diagnosis: What conditions explain symptoms?
• Planning: What actions achieve a goal?
• Debugging: What facts would fix this?

Combined Queries

Debugging Workflow

1. Observe: flies is not provable
2. Why-not: Discover r2 is blocking
3. What-if: Test what_if(["healthy"])
4. Abduce: Find minimal fix

Example Session

#![allow(unused)]
fn main() {
// 1. Check current state
let conclusions = theory.reason();
assert!(!is_provable(&conclusions, "flies"));

// 2. Understand why
let why = why_not(&theory, "flies");
println!("Blocked by: {:?}", why.blockers);

// 3. Explore hypotheticals
let hypo = what_if(&theory, &["super_bird"], "flies");
if hypo.provable {
    println!("Would work if super_bird");
}

// 4. Find minimal solution
let solutions = abduce(&theory, "flies", 3);
println!("Minimal fixes: {:?}", solutions);
}

WebAssembly API

The WASM bindings expose these operators:

import { Spindle } from 'spindle-wasm';

const spindle = new Spindle();
spindle.parseSpl(`
  (given bird)
  (given penguin)
  (normally r1 bird flies)
  (normally r2 penguin (not flies))
  (prefer r2 r1)
`);

// What-if
const whatIf = spindle.whatIf(["healthy"], "flies");
console.log(whatIf);

// Why-not
const whyNot = spindle.whyNot("flies");
console.log(whyNot);

// Abduction
const abduce = spindle.abduce("flies", 3);
console.log(abduce);

Limitations

1. Depth limits: Abduction has a configurable depth limit to avoid infinite search
2. Minimal solutions: Abduction returns minimal sets, not all possible sets
3. Grounded queries: Queries work on grounded theories; variables must be bound
4. Performance: Deep abduction can be expensive for large theories

Explanation System

Spindle provides a comprehensive explanation system for inspecting how and why conclusions are derived in defeasible reasoning. When a reasoner produces a conclusion, understanding the derivation path, the alternatives that were considered and rejected, and the conflicts that were resolved is essential for trust, debugging, and auditability.

Why Explanations Matter

Defeasible reasoning involves rules that can be overridden, conflicts between competing conclusions, and subtle interactions between superiority relations. A bare conclusion like +d ~flies tells you the result but not the story. The explanation system answers questions such as:

• Which rules fired to produce this conclusion?
• Were there competing rules that were defeated?
• How were conflicts resolved -- by superiority, definite priority, or team defeat?
• What is the full derivation chain from facts to conclusion?

This is critical in domains like legal reasoning, medical diagnosis, and access control where decisions must be justified.

Proof Trees

Structure

An explanation is built around a proof tree: a recursive structure that traces the derivation of a literal back to the facts and rules that support it.

The core types are:

• ProofNode -- represents the derivation of a single literal, containing:

  • literal -- the derived literal
  • derivation_type -- Definite (strict rules and facts only) or Defeasible (defeasible rules involved)
  • proof_step -- the rule application that produced this literal
  • blocked_alternatives -- alternative derivations that were considered but rejected
  • conflicts_resolved -- conflict resolutions that occurred at this node

• ProofStep -- represents one application of a rule, containing:

  • rule_label -- which rule was applied
  • rule_type -- Fact, Strict, Defeasible, or Defeater
  • rule_text -- string representation of the rule
  • body_proofs -- recursive ProofNode entries for each body literal
  • annotations -- metadata attached to the rule

• DerivationType -- either Definite or Defeasible

Navigating Proof Trees

A proof tree reads from conclusion down to facts. At each node, the proof_step tells you which rule was used, and the body_proofs within that step give you the sub-trees for each premise.

For example, given a theory where penguin is a fact, (always s1 penguin bird) is strict, and (normally r1 bird flies) is defeasible, the proof tree for flies would look like:

flies [defeasible, r1: bird -> flies]
  bird [definite, s1: penguin -> bird]
    penguin [definite, f1: penguin]

Each level corresponds to a ProofNode whose proof_step.body_proofs contains the children.

Blocked Alternatives and Conflict Resolutions

Blocked Alternatives

When the reasoner considers multiple rules that could derive a literal (or its complement), some may be blocked. A BlockedProof records:

• literal -- what the blocked rule tried to prove
• rule_label -- the label of the blocked rule
• reason -- a BlockReason enum value:
  • Superiority -- blocked by a superior rule
  • Defeater -- blocked by a defeater
  • Conflict -- blocked due to an unresolved conflict
  • BodyUnprovable -- the rule's body could not be satisfied
• blocking_rule -- the label of the rule that caused the blocking (if applicable)
• explanation -- a human-readable description

Conflict Resolutions

When two rules derive contradictory conclusions, the conflict must be resolved. A ConflictResolution records:

• winning_rule -- the rule that prevailed
• losing_rule -- the rule that was defeated
• resolution_type -- a ResolutionType enum value:
  • Superiority -- resolved by an explicit superiority relation
  • DefinitePriority -- resolved because strict rules override defeasible ones
  • TeamDefeat -- resolved by team defeat (a group of rules collectively defeats the attacker)

Together, blocked alternatives and conflict resolutions provide a complete picture of why one derivation was chosen over another.

Output Formats

The Explanation type supports four output formats, each suited to different use cases.

Natural Language

#![allow(unused)]
fn main() {
let text = explanation.to_natural_language();
println!("{}", text);
}

Produces human-readable output with headers, indented proof trees, and numbered lists:

Explanation for +d ~flies
This was proven using defeasible rules and was 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: f1

Blocked Alternatives:
  1. Rule 'r1' was blocked due to superiority: r2 is superior and concludes ~flies

Conflict Resolutions:
  1. 'r2' defeated 'r1' via superiority

Annotations (description and source) are included when present on proof steps.

JSON

#![allow(unused)]
fn main() {
let json = explanation.to_json();
}

Produces a structured JSON value with nested proof trees:

{
  "conclusion_type": "+d",
  "literal": "~flies",
  "proof_tree": {
    "literal": "~flies",
    "derivation_type": "defeasible",
    "proof_step": {
      "rule_label": "r2",
      "rule_type": "defeasible",
      "rule_text": "penguin -> ~flies",
      "body_proofs": [
        {
          "literal": "penguin",
          "derivation_type": "definite",
          "proof_step": {
            "rule_label": "f1",
            "rule_type": "fact",
            "rule_text": "penguin",
            "body_proofs": []
          }
        }
      ]
    }
  },
  "blocked_alternatives": [
    {
      "literal": "flies",
      "rule_label": "r1",
      "reason": "superiority",
      "blocking_rule": "r2",
      "explanation": "r2 is superior and concludes ~flies"
    }
  ],
  "conflicts_resolved": [
    {
      "winning_rule": "r2",
      "losing_rule": "r1",
      "resolution_type": "superiority",
      "superiority_label": "sup1"
    }
  ]
}

JSON-LD

#![allow(unused)]
fn main() {
let jsonld = explanation.to_jsonld();
}

Produces a JSON-LD document with semantic annotations for integration with linked data systems. The output includes:

• @context defining vocabulary prefixes:
  • spindle -- https://spindle.dev/ontology#
  • prov -- http://www.w3.org/ns/prov#
  • rdfs -- http://www.w3.org/2000/01/rdf-schema#
  • xsd -- http://www.w3.org/2001/XMLSchema#
• @type: "spindle:Explanation" on the root document
• @type: "spindle:ProofNode" on proof nodes
• @type: "spindle:ProofStep" on proof steps
• @type: "spindle:BlockedProof" on blocked alternatives
• @type: "spindle:ConflictResolution" on conflict resolutions

Provenance annotations from rule metadata are mapped to standard vocabularies:

• source / prov:wasAttributedTo for attribution
• description / rdfs:comment for descriptions
• confidence / spindle:confidence for trust scores
• @id for linked data identifiers

Graphviz DOT

#![allow(unused)]
fn main() {
let dot = explanation.to_dot();
}

Produces a DOT language graph for visual rendering. The color scheme encodes derivation semantics:

The graph uses bottom-to-top layout (rankdir=BT), so facts appear at the bottom and conclusions at the top. Edges are labeled with rule labels.

Annotations and Metadata

The Annotations Type

Annotations is a metadata container with two fields:

• id -- an optional URI identifier (@id in JSON-LD)
• entries -- a HashMap<String, String> of key-value pairs

Standard Vocabulary Keys

The annotation system recognizes standard vocabulary keys and provides convenience accessors that check multiple equivalent keys:

You can also use get(key) for any arbitrary key, or get_any(keys) to check a list of fallback keys.

Creating Annotations

#![allow(unused)]
fn main() {
use spindle_core::explanation::Annotations;

// Empty annotations
let annots = Annotations::new();

// With entries
let annots = Annotations::with_entries(vec![
    ("description", "Birds typically fly"),
    ("source", "ornithology-textbook"),
    ("confidence", "0.95"),
]);

// With a linked data identifier
let mut annots = Annotations::with_entries(vec![
    ("source", "legal-statute-42-usc-1983"),
]);
annots.id = Some("https://example.org/rules/r1".to_string());
}

Attaching Annotations to Proof Steps

#![allow(unused)]
fn main() {
use spindle_core::explanation::{ProofStep, Annotations};
use spindle_core::rule::RuleType;

let annots = Annotations::with_entries(vec![
    ("source", "expert-knowledge"),
    ("description", "Standard medical practice guideline"),
    ("confidence", "0.85"),
]);

let step = ProofStep::new("med_rule", RuleType::Defeasible, "symptom -> diagnosis")
    .with_annotations(annots);
}

Annotations are preserved across all output formats. In natural language, description and source are printed inline. In JSON-LD, they are mapped to rdfs:comment, prov:wasAttributedTo, and spindle:confidence respectively.

CLI Usage

The explain Command

Show the full derivation proof tree for a provable literal:

spindle explain "~flies" theory.spl

Output includes the derivation chain, blocked alternatives, and conflict resolutions in natural language format.

For machine-readable output:

spindle explain "~flies" theory.spl --json

The why-not Command

Explain why a literal is NOT provable:

spindle why-not flies theory.spl

Lists each rule that could have derived the literal and explains why it was blocked (missing premises, defeated by a stronger rule, or contradicted by a strict derivation).

For machine-readable output:

spindle why-not flies theory.spl --json

The JSON output includes is_provable to indicate whether the literal is actually provable, and would_derive with the rule label when available.

Debugging Workflow

A typical debugging session combines both commands:

# 1. Check what was concluded
spindle reason --positive theory.spl

# 2. A literal you expected is missing -- find out why
spindle why-not flies theory.spl

# 3. A literal you did not expect is present -- inspect its proof
spindle explain "~flies" theory.spl

# 4. Pipe JSON output to other tools for further analysis
spindle explain "~flies" theory.spl --json | jq '.blocked_alternatives'

Rust API Examples

Generating an Explanation

#![allow(unused)]
fn main() {
use spindle_core::explanation::explain;
use spindle_core::literal::Literal;
use spindle_core::theory::Theory;

let mut theory = Theory::new();
theory.add_fact("bird");
theory.add_defeasible_rule(&["bird"], "flies");

let literal = Literal::simple("flies");
if let Some(explanation) = explain(&theory, &literal) {
    // Natural language output
    println!("{}", explanation.to_natural_language());

    // Structured JSON
    let json = explanation.to_json();
    println!("{}", serde_json::to_string_pretty(&json).unwrap());

    // JSON-LD for semantic web
    let jsonld = explanation.to_jsonld();

    // Graphviz DOT for visualization
    let dot = explanation.to_dot();
}
}

The explain function returns None if the literal is not positively provable in the theory.

Building Explanations Manually

For custom explanation construction (useful in testing or when building explanations outside the standard reasoning pipeline):

#![allow(unused)]
fn main() {
use spindle_core::explanation::*;
use spindle_core::conclusion::ConclusionType;
use spindle_core::literal::Literal;
use spindle_core::rule::RuleType;

// Build a proof tree bottom-up
let fact_step = ProofStep::new("f1", RuleType::Fact, "penguin");
let fact_node = ProofNode::new(Literal::simple("penguin"), DerivationType::Definite)
    .with_proof_step(fact_step);

let rule_step = ProofStep::new("r2", RuleType::Defeasible, "penguin -> ~flies")
    .with_body_proofs(vec![fact_node]);
let conclusion_node = ProofNode::new(Literal::negated("flies"), DerivationType::Defeasible)
    .with_proof_step(rule_step);

// Record a blocked alternative
let blocked = BlockedProof::new(
    Literal::simple("flies"),
    "r1",
    BlockReason::Superiority,
    "Rule r2 is superior and concludes ~flies",
).with_blocking_rule("r2");

// Record a conflict resolution
let conflict = ConflictResolution::new("r2", "r1", ResolutionType::Superiority)
    .with_superiority("sup1");

// Assemble the explanation
let explanation = Explanation::new(
    ConclusionType::DefeasiblyProvable,
    Literal::negated("flies"),
)
.with_proof(conclusion_node)
.with_blocked(vec![blocked])
.with_conflicts(vec![conflict]);
}

Inspecting Proof Trees Programmatically

#![allow(unused)]
fn main() {
fn walk_proof(node: &ProofNode, depth: usize) {
    let indent = "  ".repeat(depth);
    let dtype = match node.derivation_type {
        DerivationType::Definite => "definite",
        DerivationType::Defeasible => "defeasible",
    };
    println!("{}{} [{}]", indent, node.literal, dtype);

    if let Some(ref step) = node.proof_step {
        println!("{}  via rule: {}", indent, step.rule_label);

        if let Some(desc) = step.annotations.description() {
            println!("{}  description: {}", indent, desc);
        }

        for child in &step.body_proofs {
            walk_proof(child, depth + 1);
        }
    }
}

if let Some(ref tree) = explanation.proof_tree {
    walk_proof(tree, 0);
}
}

Use Case: Visual Proof Graphs with DOT Output

The DOT output format integrates directly with Graphviz for generating visual proof graphs.

Generating a Graph

# Generate DOT and render to PNG
spindle explain "~flies" theory.spl --json \
  | jq -r '.proof_tree' \
  > /dev/null  # Use the Rust API instead for DOT

# Or from Rust:

#![allow(unused)]
fn main() {
use spindle_core::explanation::explain;
use spindle_core::literal::Literal;
use std::fs;
use std::process::Command;

let literal = Literal::negated("flies");
if let Some(explanation) = explain(&theory, &literal) {
    let dot = explanation.to_dot();

    // Write DOT file
    fs::write("proof.dot", &dot).unwrap();

    // Render with Graphviz
    Command::new("dot")
        .args(["-Tpng", "proof.dot", "-o", "proof.png"])
        .status()
        .unwrap();

    // Or render to SVG for web embedding
    Command::new("dot")
        .args(["-Tsvg", "proof.dot", "-o", "proof.svg"])
        .status()
        .unwrap();
}
}

Reading the Graph

The generated graph uses a consistent visual language:

• Blue boxes at the bottom represent facts and strict derivations. These are the foundation of the proof and cannot be defeated.
• Green boxes represent defeasible derivations. These are the conclusions that could potentially be overridden by new information.
• Red dashed boxes in the "Blocked Alternatives" cluster show derivations that were considered but rejected. The label includes the rule label and the reason for blocking.
• Orange diamonds in the "Conflict Resolutions" cluster show how conflicts between competing rules were resolved, including the winning and losing rules and the resolution mechanism.

Edges flow upward from premises to conclusions, labeled with the rule that was applied.

Example DOT Output

For a penguin theory with r2 > r1:

digraph Explanation {
  rankdir=BT;
  node [fontname="Helvetica"];
  edge [fontname="Helvetica"];

  title [label="+d ~flies" shape=plaintext fontsize=14 fontcolor=black];

  n1 [label="~flies\n[defeasible: r2]" shape=box style=filled fillcolor="#d4edda"];
  n2 [label="penguin\n[fact: f1]" shape=box style=filled fillcolor="#cce5ff"];
  n2 -> n1 [label="r2"];
  title -> n1 [style=invis];

  // Blocked alternatives
  subgraph cluster_blocked {
    label="Blocked Alternatives";
    style=dashed;
    color=red;
    b3 [label="flies\n(rule: r1)\nblocked: superiority" shape=box style="dashed,filled" fillcolor="#ffcccc"];
  }

  // Conflict resolutions
  subgraph cluster_conflicts {
    label="Conflict Resolutions";
    style=dashed;
    color=orange;
    c4 [label="r2 > r1\n(superiority)" shape=diamond style=filled fillcolor="#ffe0b3"];
  }
}

Use Case: Semantic Web Integration with JSON-LD

The JSON-LD output allows Spindle explanations to participate in the linked data ecosystem.

Publishing Explanations as Linked Data

#![allow(unused)]
fn main() {
use spindle_core::explanation::{explain, Annotations, ProofStep};
use spindle_core::literal::Literal;

let literal = Literal::simple("liable");
if let Some(explanation) = explain(&theory, &literal) {
    let jsonld = explanation.to_jsonld();

    // Serialize for publication
    let output = serde_json::to_string_pretty(&jsonld).unwrap();
    println!("{}", output);
}
}

The resulting JSON-LD document can be:

• Consumed by any JSON-LD processor (e.g., jsonld.js, Apache Jena)
• Expanded, compacted, or flattened using standard JSON-LD algorithms
• Converted to RDF triples for storage in a triple store
• Queried with SPARQL alongside other linked data

Provenance Tracking

When rules carry annotations with source and confidence information, the JSON-LD output maps these to standard provenance vocabulary:

{
  "@context": {
    "spindle": "https://spindle.dev/ontology#",
    "prov": "http://www.w3.org/ns/prov#",
    "rdfs": "http://www.w3.org/2000/01/rdf-schema#",
    "xsd": "http://www.w3.org/2001/XMLSchema#"
  },
  "@type": "spindle:Explanation",
  "conclusionType": "+d",
  "literal": "liable",
  "proofTree": {
    "@type": "spindle:ProofNode",
    "literal": "liable",
    "derivationType": "defeasible",
    "proofStep": {
      "@type": "spindle:ProofStep",
      "@id": "https://example.org/rules/r1",
      "ruleLabel": "r1",
      "ruleType": "defeasible",
      "wasAttributedTo": "legal-statute-42-usc-1983",
      "rdfs:comment": "Civil rights violation implies liability",
      "spindle:confidence": "0.9"
    }
  }
}

Linking to External Ontologies

By using standard vocabulary keys in annotations, you can link Spindle explanations to domain ontologies:

#![allow(unused)]
fn main() {
let mut annots = Annotations::with_entries(vec![
    ("dc:source", "https://www.law.cornell.edu/uscode/text/42/1983"),
    ("prov:wasAttributedTo", "https://example.org/agents/legal-expert"),
    ("rdfs:comment", "Section 1983 civil rights liability"),
]);
annots.id = Some("https://example.org/rules/civil-rights-liability".to_string());
}

This enables downstream systems to dereference rule sources, look up agent information, and integrate the explanation into a broader knowledge graph.

Limitations

1. Positive proofs only: The explain function returns None for literals that are not positively provable. Use the why-not CLI command or the query module for negative explanations.
2. Grounded theories: Explanations work on grounded theories. Variables must be bound before explanation generation.
3. No incremental updates: Explanations are generated from a full reasoning pass. Changes to the theory require re-running the reasoner.
4. Annotation attachment: Annotations must be attached to proof steps manually when building explanations programmatically. The explain function does not yet automatically populate annotations from rule metadata.

Process Mining

Spindle includes a process mining module that discovers defeasible logic rules from event logs. It implements the Alpha algorithm for Petri net discovery, footprint matrix construction, conflict detection, and SPL rule extraction with support/confidence metrics.

Note: Process mining is currently available through the Rust API only. It is not exposed via the CLI or the WebAssembly bindings.

Overview

Process mining bridges the gap between observed behavior (event logs) and formal models (defeasible logic rules). The pipeline works as follows:

EventLog -> Footprint -> PetriNet -> LearnedRules
               |                         |
               v                         v
         Relation analysis       SPL rules with
         (causal, parallel,      support/confidence
          unrelated)             metrics

Given a set of recorded process executions (cases), Spindle can:

1. Analyze activity relationships via a footprint matrix
2. Discover a Petri net process model using the Alpha algorithm
3. Detect conflicts (choice and mutex patterns)
4. Extract defeasible logic rules with statistical support

Event Logs

Structure

An event log consists of cases (process executions), each containing a sequence of events.

• Event -- a single activity execution with a timestamp, activity name, variable bindings, optional actor, and annotations
• Case -- a complete process trace identified by a unique ID, containing events sorted by timestamp
• EventLog -- the collection of cases with optional metadata

Creating Events

#![allow(unused)]
fn main() {
use spindle_core::mining::{Event, Case, EventLog};
use std::collections::HashMap;

// Simple event with timestamp, activity, and bindings
let mut bindings = HashMap::new();
bindings.insert("entity".to_string(), "order-42".to_string());

let event = Event::new("2026-01-17T10:00:00Z", "submitted", bindings);

// Event with an actor
let event = Event::new("2026-01-17T10:05:00Z", "reviewed", HashMap::new())
    .with_actor("alice");

// Event with annotations
let mut annotations = HashMap::new();
annotations.insert("priority".to_string(), "high".to_string());

let event = Event::new("2026-01-17T10:10:00Z", "approved", HashMap::new())
    .with_actor("bob")
    .with_annotations(annotations);
}

Creating Cases and Logs

Events within a case are automatically sorted by timestamp:

#![allow(unused)]
fn main() {
use spindle_core::mining::{Event, Case, EventLog};
use std::collections::HashMap;

// Build a case from events
let events = vec![
    Event::new("2026-01-17T12:00:00Z", "complete", HashMap::new()),
    Event::new("2026-01-17T10:00:00Z", "start", HashMap::new()),
    Event::new("2026-01-17T11:00:00Z", "process", HashMap::new()),
];
let case = Case::new("case-1", events);

// Events are sorted: start, process, complete
assert_eq!(case.activities(), vec!["start", "process", "complete"]);

// Build a log from cases
let log = EventLog::new(vec![case]);
}

Log Inspection

#![allow(unused)]
fn main() {
// All unique activities across the log
let activities = log.activities();  // HashSet<&str>

// Total number of events
let count = log.total_events();
}

Helper Functions

For testing and quick prototyping, helper functions simplify log construction:

#![allow(unused)]
fn main() {
use spindle_core::mining::{make_sequential_trace, make_log_from_traces, make_repeated_log};

// Single sequential trace
let case = make_sequential_trace("case-1", &["start", "process", "end"]);

// Log from multiple trace patterns
let log = make_log_from_traces(&[
    &["start", "a", "b", "end"],
    &["start", "b", "a", "end"],
    &["start", "a", "b", "end"],
]);

// Log with n identical traces
let log = make_repeated_log(10, &["submit", "review", "approve"]);
}

Footprint Matrix

The footprint matrix captures directly-follows relationships between activities. It is the foundation for the Alpha algorithm.

Relations

Given two activities a and b, the footprint matrix assigns one of four relations:

Building a Footprint

#![allow(unused)]
fn main() {
use spindle_core::mining::{Footprint, EventLog, make_repeated_log, make_log_from_traces};

// Sequential pattern: a -> b -> c
let log = make_repeated_log(5, &["a", "b", "c"]);
let fp = Footprint::from_log(&log);

// Check relations
assert!(fp.is_causal("a", "b"));   // a -> b
assert!(fp.is_causal("b", "c"));   // b -> c
assert!(fp.is_unrelated("a", "c")); // a # c (never directly adjacent)

// Parallel pattern
let log = make_log_from_traces(&[
    &["a", "b"],
    &["b", "a"],
]);
let fp = Footprint::from_log(&log);
assert!(fp.is_parallel("a", "b")); // a || b
}

Querying the Matrix

#![allow(unused)]
fn main() {
use spindle_core::mining::Relation;

// Get a specific relation
let rel = fp.relation("a", "b");
match rel {
    Relation::Causality => println!("a causes b"),
    Relation::Reverse   => println!("b causes a"),
    Relation::Parallel  => println!("a and b are concurrent"),
    Relation::Unrelated => println!("a and b are unrelated"),
}

// Bulk queries
let causal = fp.causal_pairs();     // Vec<(String, String)>
let parallel = fp.parallel_pairs(); // Vec<(String, String)>
}

What the Matrix Reveals

The footprint matrix answers key questions about a process:

• Sequencing: Which activities always follow others? (Causality)
• Concurrency: Which activities can happen in either order? (Parallel)
• Independence: Which activities are never adjacent? (Unrelated)
• Reverse flow: Which activities are preceded by others? (Reverse)

Alpha Algorithm and Petri Net Discovery

The Alpha algorithm transforms a footprint matrix into a Petri net, a formal model of the process.

Petri Net Structure

A Petri net consists of:

• Place -- a passive element with an ID and label (represents conditions/states)
• Transition -- an active element representing an activity
• Arc -- a directed connection between a place and a transition (or vice versa), using ArcNode::Place and ArcNode::Transition variants

Running the Alpha Miner

#![allow(unused)]
fn main() {
use spindle_core::mining::{AlphaMiner, EventLog, make_repeated_log};

let log = make_repeated_log(10, &["a", "b", "c"]);

let mut miner = AlphaMiner::new();
let net = miner.mine(&log);

// Inspect the discovered net
println!("Places: {}", net.places.len());
println!("Transitions: {}", net.transitions.len());
println!("Arcs: {}", net.arcs.len());

// Find a transition by activity name
if let Some(trans) = net.find_transition("b") {
    println!("Found transition: {} ({})", trans.id, trans.activity);
}

// All activities in the net
let activities = net.activities(); // HashSet<&str>
}

How It Works

The Alpha algorithm performs these steps:

1. Compute footprint from the event log's directly-follows pairs
2. Identify start/end activities (first/last in each trace)
3. Find maximal pairs (A, B) where all activities in A causally lead to all activities in B, and both sets are internally unrelated
4. Build the net: create transitions for each activity, places for start/end and each maximal pair, and arcs connecting them

Building a Petri Net Manually

#![allow(unused)]
fn main() {
use spindle_core::mining::{PetriNet, Place, Transition, Arc, ArcNode};

let mut net = PetriNet::new();

net.add_place(Place::new("p1", "start"));
net.add_place(Place::new("p2", "end"));

net.add_transition(Transition::new("t1", "submit"));
net.add_transition(Transition::new("t2", "approve"));

net.add_arc(Arc::new(
    ArcNode::Place("p1".to_string()),
    ArcNode::Transition("t1".to_string()),
));
net.add_arc(Arc::new(
    ArcNode::Transition("t1".to_string()),
    ArcNode::Place("p2".to_string()),
));
}

Conflict Detection

Conflicts arise when activities are mutually exclusive or represent choices in the process.

Conflict Types

Detecting Conflicts

#![allow(unused)]
fn main() {
use spindle_core::mining::{detect_conflicts, AlphaMiner, make_log_from_traces};

let log = make_log_from_traces(&[
    &["start", "a", "end"],
    &["start", "a", "end"],
    &["start", "b", "end"],
    &["start", "b", "end"],
]);

let mut miner = AlphaMiner::new();
let net = miner.mine(&log);
let conflicts = detect_conflicts(&log, &net);

for conflict in &conflicts {
    println!("Conflict: {:?}", conflict.activities);
    match conflict.conflict_type {
        spindle_core::mining::ConflictType::Choice => {
            println!("  Type: XOR choice (from Petri net structure)");
        }
        spindle_core::mining::ConflictType::Mutex => {
            println!("  Type: Mutex (never co-occur in traces)");
        }
    }
    // Evidence explains the source of the conflict
    if let Some(source) = conflict.evidence.get("source") {
        println!("  Evidence: {}", source);
    }
}
}

Choice vs Mutex

Choice conflicts are structural -- they come from XOR-split points in the Petri net where a place has multiple outgoing transitions. Only one transition can fire.

Mutex conflicts are behavioral -- two activities are never observed together in the same trace, but the relationship is not already captured by a choice conflict. This can indicate implicit exclusion rules.

Rule Learning

The module extracts defeasible logic rules from causal relationships in the event log, annotated with statistical metrics.

Support and Confidence

• Support: the number of traces where a is directly followed by b
• Confidence: the ratio of a -> b transitions to all transitions from a

For example, if a appears 10 times as a non-final activity and a -> b occurs 8 times, the confidence is 0.8.

Extracting Rules

#![allow(unused)]
fn main() {
use spindle_core::mining::{petri_net_to_rules, make_repeated_log};

let log = make_repeated_log(10, &["submit", "review", "approve"]);

// Extract rules with minimum support of 5 and confidence of 0.7
let rules = petri_net_to_rules(&log, 5, 0.7);

for lr in &rules {
    println!("Rule: {}", lr.rule.label);
    println!("  Body: {:?}", lr.rule.body.iter().map(|l| l.name()).collect::<Vec<_>>());
    println!("  Head: {:?}", lr.rule.head.iter().map(|l| l.name()).collect::<Vec<_>>());
    println!("  Support: {}", lr.support);
    println!("  Confidence: {:.2}", lr.confidence);
    println!("  Source: {}", lr.source);  // "mined"
}
}

Each LearnedRule contains:

• rule -- a defeasible logic Rule (type Defeasible, labeled r_mined_N)
• support -- trace count supporting the causal pair
• confidence -- ratio of supporting transitions
• source -- origin of the rule (defaults to "mined")

Filtering by Thresholds

Rules below the minimum support or confidence thresholds are excluded:

#![allow(unused)]
fn main() {
// Strict thresholds: only high-confidence rules
let strict_rules = petri_net_to_rules(&log, 10, 0.9);

// Relaxed thresholds: discover more patterns
let relaxed_rules = petri_net_to_rules(&log, 1, 0.0);
}

Complete Mining Pipeline

The mine_rules function runs the entire pipeline in a single call.

Usage

#![allow(unused)]
fn main() {
use spindle_core::mining::{mine_rules, make_log_from_traces};

let log = make_log_from_traces(&[
    &["start", "a", "b", "end"],
    &["start", "a", "b", "end"],
    &["start", "a", "c", "end"],
    &["start", "a", "b", "end"],
]);

let result = mine_rules(&log, 2, 0.5);
}

MiningResult Structure

The result bundles all outputs from the pipeline:

#![allow(unused)]
fn main() {
// Learned SPL rules
for lr in &result.rules {
    println!("{}: support={}, confidence={:.2}", lr.rule.label, lr.support, lr.confidence);
}

// Detected conflicts
for c in &result.conflicts {
    println!("Conflict {:?}: {:?}", c.conflict_type, c.activities);
}

// Discovered Petri net
println!("Net: {} places, {} transitions, {} arcs",
    result.petri_net.places.len(),
    result.petri_net.transitions.len(),
    result.petri_net.arcs.len(),
);

// Footprint matrix
for (a, b) in result.footprint.causal_pairs() {
    println!("{} -> {}", a, b);
}

// Mining metadata
println!("Traces: {}", result.metadata.get("trace_count").unwrap());
println!("Events: {}", result.metadata.get("event_count").unwrap());
println!("Min support: {}", result.metadata.get("min_support").unwrap());
println!("Min confidence: {}", result.metadata.get("min_confidence").unwrap());
}

Pipeline Steps

mine_rules performs the following steps internally:

1. Build the footprint matrix from the event log
2. Run the Alpha miner to discover the Petri net
3. Detect conflicts from the net structure and trace analysis
4. Extract SPL rules from causal pairs, filtered by support and confidence
5. Package everything into a MiningResult with metadata

Use Cases

Workflow Analysis

Discover the actual execution patterns from system logs:

#![allow(unused)]
fn main() {
use spindle_core::mining::{Event, Case, EventLog, mine_rules};
use std::collections::HashMap;

// Build log from real workflow events
let case1 = Case::new("ticket-101", vec![
    Event::new("2026-01-17T09:00:00Z", "opened", HashMap::new())
        .with_actor("user"),
    Event::new("2026-01-17T09:30:00Z", "triaged", HashMap::new())
        .with_actor("support"),
    Event::new("2026-01-17T10:00:00Z", "assigned", HashMap::new())
        .with_actor("manager"),
    Event::new("2026-01-17T14:00:00Z", "resolved", HashMap::new())
        .with_actor("engineer"),
]);

let case2 = Case::new("ticket-102", vec![
    Event::new("2026-01-17T10:00:00Z", "opened", HashMap::new())
        .with_actor("user"),
    Event::new("2026-01-17T10:15:00Z", "triaged", HashMap::new())
        .with_actor("support"),
    Event::new("2026-01-17T10:30:00Z", "assigned", HashMap::new())
        .with_actor("manager"),
    Event::new("2026-01-17T16:00:00Z", "resolved", HashMap::new())
        .with_actor("engineer"),
]);

let log = EventLog::new(vec![case1, case2]);
let result = mine_rules(&log, 1, 0.5);

// Discovered rules describe the standard ticket workflow
for lr in &result.rules {
    println!("{}: {} -> {}  (support={}, confidence={:.0}%)",
        lr.rule.label,
        lr.rule.body.iter().map(|l| l.name()).collect::<Vec<_>>().join(", "),
        lr.rule.head.iter().map(|l| l.name()).collect::<Vec<_>>().join(", "),
        lr.support,
        lr.confidence * 100.0,
    );
}
}

Compliance Checking

Identify process deviations by comparing mined rules against expected patterns:

#![allow(unused)]
fn main() {
use spindle_core::mining::{Footprint, make_log_from_traces};

let log = make_log_from_traces(&[
    &["submit", "review", "approve"],
    &["submit", "review", "approve"],
    &["submit", "approve"],           // Skipped review
    &["submit", "review", "approve"],
]);

let fp = Footprint::from_log(&log);

// Check if review always precedes approval
if fp.is_causal("review", "approve") {
    println!("Compliant: review always directly precedes approve");
} else {
    println!("Violation: review does not always precede approve");
}

// Check for unauthorized shortcuts
if fp.is_causal("submit", "approve") {
    println!("Warning: direct submit-to-approve path detected");
}
}

Process Discovery

Combine mining with Spindle's reasoning engine to build executable rule sets:

#![allow(unused)]
fn main() {
use spindle_core::mining::{mine_rules, make_log_from_traces};

let log = make_log_from_traces(&[
    &["init", "process", "validate", "complete"],
    &["init", "process", "reject"],
    &["init", "process", "validate", "complete"],
    &["init", "skip", "complete"],
]);

let result = mine_rules(&log, 1, 0.0);

// The learned rules can be added to a theory for further reasoning
println!("Discovered {} rules from {} traces",
    result.rules.len(),
    result.metadata.get("trace_count").unwrap(),
);

// Conflicts reveal decision points in the process
for c in &result.conflicts {
    println!("Decision point: {:?} ({:?})", c.activities, c.conflict_type);
}
}

Limitations

1. Alpha algorithm scope: The Alpha miner handles sequential, parallel, and choice patterns. It does not support loops, invisible transitions, or duplicate activities.
2. Directly-follows only: The footprint matrix considers only directly adjacent activities, not long-range dependencies.
3. Timestamp ordering: Events within a case are sorted lexicographically by timestamp string. Use ISO-8601 format to ensure correct ordering.
4. Rust API only: Process mining is not yet available through the CLI or WebAssembly bindings.
5. No incremental mining: The entire log must be provided upfront; streaming or incremental updates are not supported.

Performance Tuning

This guide covers performance optimization for Spindle.

Reasoning Engine

Standard DL(d)

Spindle uses the standard DL(d) forward-chaining engine.

spindle reason theory.spl

Benchmark Your Theory

# Time a representative run
time spindle reason theory.spl > /dev/null

Theory Design

Minimize Rule Bodies

Larger bodies = more matching work:

; Slower: 5-way join
(normally r1 (and a b c d e) result)

; Faster: chain of 2-way joins
(normally r1 (and a b) ab)
(normally r2 (and ab c) abc)
(normally r3 (and abc d) abcd)
(normally r4 (and abcd e) result)

Use Specific Predicates

; Slower: matches all 'thing' facts
(normally r1 (thing ?x) (processed ?x))

; Faster: matches only relevant facts
(normally r1 (unprocessed-item ?x) (processed ?x))

Reduce Grounding Explosion

Variables can cause combinatorial explosion:

; If there are 100 'node' facts, this creates 10,000 ground rules
(normally r1 (and (node ?x) (node ?y)) (pair ?x ?y))

; Add constraints to reduce matching
(normally r1 (and (node ?x) (node ?y) (edge ?x ?y)) (connected ?x ?y))

Memory Optimization

Note: During reasoning, the proven literal set now uses a BitSet instead of HashSet<LiteralId>, providing O(1) membership tests with significantly better cache locality. See Recent Optimizations for details.

String Interning

Spindle uses string interning internally. You can benefit by:

#![allow(unused)]
fn main() {
// Reuse literal names
let bird = "bird";
theory.add_fact(bird);
theory.add_defeasible_rule(&[bird], "flies");
}

Stream Large Results

For large result sets:

#![allow(unused)]
fn main() {
// Instead of collecting all conclusions
let conclusions: Vec<Conclusion> = theory.reason();

// Process incrementally (future API)
for conclusion in theory.reason_iter() {
    process(conclusion);
}
}

Theory Cloning

Avoid unnecessary cloning:

#![allow(unused)]
fn main() {
// Expensive: clones the whole theory
let copy = theory.clone();

// Better: reuse the indexed theory
let indexed = IndexedTheory::build(theory);
// Use indexed for multiple queries
}

Conflict Optimization

Minimize Conflicts

Fewer conflicts = faster resolution:

; Many potential conflicts
(normally r1 a result)
(normally r2 b ~result)
(normally r3 c result)
(normally r4 d ~result)

; Better: restructure to reduce conflicts
(normally supports a supports-result)
(normally supports c supports-result)
(normally opposes b opposes-result)
(normally opposes d opposes-result)
(normally conclusion supports-result result)
(normally conclusion opposes-result ~result)
(prefer conclusion ...)

Explicit Superiority

Unresolved conflicts cause ambiguity propagation:

; Bad: no superiority, causes ambiguity checks
(normally r1 a q)
(normally r2 b ~q)

; Good: explicit resolution
(normally r1 a q)
(normally r2 b ~q)
(prefer r1 r2)  ; or (prefer r2 r1)

Indexing Benefits

Spindle indexes rules by:

• Head literal → O(1) lookup
• Body literal → O(1) lookup
• Superiority → O(1) lookup

The indexed theory is built once and reused:

#![allow(unused)]
fn main() {
let indexed = IndexedTheory::build(theory);

// Fast: O(1) lookups
for rule in indexed.rules_with_head(&literal) { ... }
for rule in indexed.rules_with_body(&literal) { ... }
}

Profiling

Theory Statistics

spindle stats theory.spl

Look for:

• High rule count → check grounding and rule-body fanout
• Many defeaters → potential blocking overhead
• Complex bodies → grounding overhead

Rust Profiling

# Build with profiling
cargo build --release

# Profile with flamegraph
cargo flamegraph -- spindle reason theory.spl

Memory Profiling

# Use heaptrack
heaptrack spindle reason large-theory.spl
heaptrack_print heaptrack.spindle.*.gz

Recent Optimizations

Several targeted optimizations have been applied to Spindle's internals. These are transparent to end users but can significantly reduce runtime and memory overhead, especially for larger theories.

SmallVec for Rule Bodies/Heads

Commit [9bee7a3]

Rule body and head storage was changed from Vec<Literal> to SmallVec<[Literal; 4]>. This means that rules with four or fewer body/head literals avoid heap allocation entirely -- the data is stored inline on the stack.

Most real-world defeasible rules have 1-3 body literals, so the common case is covered without any heap allocation. This reduces allocation pressure during both grounding and reasoning.

#![allow(unused)]
fn main() {
// Before
struct Rule {
    head: Vec<Literal>,
    body: Vec<Literal>,
}

// After
use smallvec::SmallVec;
struct Rule {
    head: SmallVec<[Literal; 4]>,
    body: SmallVec<[Literal; 4]>,
}
}

BitSet for Proven Literals

Commit [82ae834]

The set of proven literals during reasoning was changed from HashSet<LiteralId> to a compact BitSet. Since LiteralId is a u32, bitmap indexing is a natural fit:

• O(1) contains and insert operations (bit test / bit set).
• Better cache locality -- the entire proven set fits in a contiguous allocation rather than being scattered across hash buckets.
• Significant improvement for theories with many literals, where hash collisions and bucket traversal previously added up.

FxHash for Internal HashMaps

Commit [4fbe1fd]

All internal HashMap / HashSet instances were switched from the default SipHash hasher to FxHash (provided by the rustc-hash crate).

• FxHash is considerably faster for small keys (u32, u64) that are common throughout Spindle's indexing and reasoning structures.
• It is not cryptographically secure, but Spindle's internal maps are never exposed to untrusted input, so this is not a concern.
• This is the same hasher used inside the Rust compiler itself.

Pre-allocation Strategies

Commit [2e92b84]

Worklists, intermediate buffers, and result vectors are now pre-allocated based on the size of the theory before reasoning begins:

• The conclusion vector is allocated with an estimate of rules.len() * avg_head_size.
• Worklists are sized to the number of rules to avoid repeated reallocation during the fixed-point loop.

This avoids the cost of incremental Vec growth (repeated allocate-copy-deallocate cycles) and reduces peak memory usage by avoiding over-allocation.

Benchmarks

Run the built-in benchmarks:

cd crates/spindle-core
cargo bench

Key benchmarks:

• reason_penguin - basic conflict resolution
• reason_long_chain - forward chaining depth
• reason_wide - parallel independent rules

Performance Checklist

1. Use explicit superiority in conflicts

   • Conflicting defeasible rules are intentionally unresolved unless ordered
   • Add superiority relations where one side must win

2. Optimize theory design

   • Keep rule bodies small
   • Use specific predicates
   • Control grounding size

3. Resolve conflicts

   • Add superiority relations
   • Avoid unnecessary ambiguity

4. Monitor resources

   • Check spindle stats output
   • Profile if needed
   • Benchmark representative theories

Troubleshooting

Common issues and how to resolve them.

Parse Errors

"Unknown keyword" Error

SPL parse error: Unknown keyword: defeasible

Cause: Wrong keyword.

Fix: Use correct SPL keywords:

• given (not fact)
• normally (not defeasible)
• always (not strict)
• except (not defeater)

Unexpected Conclusions

Expected Conclusion Missing

Symptom: A literal you expected to be +d is -d.

Debugging steps:

1. Check if the rule exists:

   spindle stats theory.spl
   

2. Check if the body is satisfied:

   ; Is 'bird' actually proven?
   (normally r1 bird flies)
   

3. Check for conflicts:

   # Look for rules proving the complement
   grep "(not flies)" theory.spl
   

4. Check superiority:

   # Is there a superior rule blocking?
   grep "prefer" theory.spl
   

Unexpected Conclusion Present

Symptom: A literal is +d when it shouldn't be.

Debugging steps:

1. Find which rule proves it:

   grep "literal" theory.spl
   

2. Check if a defeater is missing:

   ; Add a defeater to block
   (except d1 exception unexpected-literal)
   

Both Literals Unprovable (Ambiguity)

Symptom: Neither q nor (not q) is +d.

Cause: Conflicting rules without superiority.

Fix: Add superiority:

(normally r1 a q)
(normally r2 b (not q))
(prefer r1 r2)    ; or (prefer r2 r1)

Superiority Issues

Superiority Not Working

Symptom: Declared (prefer r1 r2) but r2 still wins.

Check:

1. Rule labels match exactly:

   (normally r1 bird flies)
   (normally r2 penguin (not flies))
   (prefer r1 r2)                      ; Must match labels exactly
   

2. Rule type compatibility:

   • Superiority only affects defeasible rules and defeaters
   • Strict rules always win regardless of superiority

3. Both rules actually fire:

   # Both bodies must be satisfied
   spindle reason --positive theory.spl | grep "bird\|penguin"
   

Circular Superiority

; BAD: creates undefined behavior
(prefer r1 r2)
(prefer r2 r1)

Fix: Remove one declaration or restructure rules.

Grounding Issues

Variables Not Matching

Symptom: Rules with variables don't produce expected results.

Check:

1. Facts use predicates:

   ; Wrong: not a predicate
   (given parent-alice-bob)
   
   ; Right: predicate with arguments
   (given (parent alice bob))
   

2. Variable positions match:

   ; Fact: (parent alice bob)
   ;              ?x    ?y
   
   ; Rule must match positions
   (normally r1 (parent ?x ?y) (ancestor ?x ?y))
   

3. All head variables appear in body:

   ; INVALID: ?z not in body
   (normally r1 (parent ?x ?y) (triple ?x ?y ?z))
   

Grounding Explosion

Symptom: Memory exhaustion or very slow reasoning.

Cause: Too many variable combinations.

Fix:

• Add constraints to rule bodies
• Break large joins into smaller rules
• Add explicit superiority where conflicts are expected

File Format Issues

Wrong Format Detection

Symptom: File parses incorrectly.

Fix: Use .spl extension for SPL format.

Encoding Issues

Symptom: Special characters cause errors.

Fix: Use UTF-8 encoding.

Conflict Expectations

Conflicting Defeasible Rules Both Show As Provable

Symptom: You see both +d p and +d ~p.

Cause: No superiority relation resolves the conflict.

Fix:

1. Add an explicit superiority declaration between the conflicting rules.
2. Re-run reasoning and verify only the preferred side remains +d.

Performance Issues

Slow Reasoning

Check:

1. Theory size: spindle stats theory.spl
2. Conflict graph: add superiority to resolve high-conflict hotspots
3. Grounding: check for variable explosion
4. Conflicts: add superiority to reduce ambiguity

Memory Exhaustion

Causes:

• Too many ground rules (variable explosion)
• Very long inference chains
• Large number of conflicts

Fixes:

• Reduce variable combinations
• Restructure theory

Debugging Tips

Validate First

Always validate before reasoning:

spindle validate theory.spl && spindle reason theory.spl

Minimal Reproduction

Create a minimal theory that reproduces the issue:

; Start with just the failing rules
(given bird)
(normally r1 bird flies)
; Add rules until issue appears

Use Positive Output

Focus on what IS proven:

spindle reason --positive theory.spl

Check Statistics

spindle stats theory.spl

Look for unexpected counts.

Enable Logging

SPINDLE_LOG=debug spindle reason theory.spl 2>&1 | less

Getting Help

If you can't resolve an issue:

1. Create a minimal reproduction
2. Include the theory file
3. Show expected vs actual output
4. Report at: https://codeberg.org/anuna/spindle-rust/issues

Changelog

All notable changes to Spindle-Rust are documented here. For the full changelog with migration notes, see CHANGELOG.md in the repository root.

v0.3.0 (2026-03-04)

Added

• SPEC-017 Arithmetic Module: full arithmetic expression support in rule bodies.
  • Three numeric term types: Integer, Decimal (arbitrary-precision via rust_decimal), Float (FiniteFloat wrapper rejecting NaN/Inf).
  • Automatic type promotion chain: Integer -> Decimal -> Float.
  • ArithExpr AST with n-ary ops (+, -, *, /, min, max), binary ops (div, rem, **), and unary ops (abs).
  • bind variable binding and comparison guards (=, !=, <, >, <=, >=) in rule bodies.
  • Cross-type numeric matching in grounding (e.g., Integer(2) matches Decimal(2.0)).
  • SPL parser extended with arithmetic expression, numeric literal, and guard parsing.
  • Parse-time rejection of arithmetic in heads, negated arithmetic, and reserved keywords.
• SPEC-018 Temporal Atom Identity: atoms with different temporal bounds are now treated as distinct during reasoning.
  • Synthetic bridging rules connect temporally-scoped variants.
  • Core query operators (what_if, why_not, requires) upgraded to temporal-aware matching.
• v2 JSON output (REQ-012): --v2 CLI flag and reasonV2 WASM method emitting typed Term arguments in schema spindle.reason.v2.

Changed

• Breaking: From<NumericValue> for Term replaced with TryFrom; non-finite floats now return errors.
• Literal::predicate_ids and Substitution::terms migrated from SymbolId to Term.
• RuleBody migrated from SmallVec<[Literal; 4]> to SmallVec<[BodyLiteral; 4]>.

Fixed

• FiniteFloat serde deserialization validates invariants, preventing non-canonical or non-finite values.
• SPL round-trip for arithmetic expressions preserved correctly.
• Tilde-negated reserved keywords (~>, ~bind, etc.) rejected in list-form literals.
• Negative base with fractional exponent rejected in decimal_pow.
• Temporal bounds preserved in body normalization.

v0.2.0 (2026-02-26)

Added

• IMPL-011 Verified requires: requires command now verifies abduction solutions by default.
  • New core API: requires_with_options(theory, goal, options) with RequiresOptions, RequiresResult, RequiresSearchStatus, RequiresVerificationStats.
  • New CLI contract schema: spindle.requires.v2.
• Release tooling: release.sh script with pre-flight validation checks and make release target.
• Pre-1.0 semver policy documented.

Changed

• requires --json emits spindle.requires.v2 schema only.
• spindle capabilities --json advertises schemas.requires = spindle.requires.v2.
• Core requires() compatibility wrapper delegates to verified logic.

Fixed

• Eliminated false-positive requires candidates that fail under full defeasible reasoning.
• Corrected BudgetExhausted classification for duplicate raw-candidate edge cases.
• Defensive collision handling for injected verification fact labels.

Rust Library Guide

This guide covers using Spindle as a Rust library.

Installation

Add to your Cargo.toml:

[dependencies]
spindle-core = { git = "https://codeberg.org/anuna/spindle-rust", package = "spindle-core" }
spindle-parser = { git = "https://codeberg.org/anuna/spindle-rust", package = "spindle-parser" }

Basic Usage

use spindle_core::prelude::*;

fn main() -> Result<()> {
    let mut theory = Theory::new();

    // Add facts
    theory.add_fact("bird");
    theory.add_fact("penguin");

    // Add defeasible rules
    let r1 = theory.add_defeasible_rule(&["bird"], "flies");
    let r2 = theory.add_defeasible_rule(&["penguin"], "~flies");

    // Set superiority
    theory.add_superiority(&r2, &r1);

    // Reason
    let conclusions = theory.reason()?;

    for c in &conclusions {
        if c.conclusion_type.is_positive() {
            println!("{}", c);
        }
    }

    Ok(())
}

Creating Theories

Programmatic Construction

#![allow(unused)]
fn main() {
use spindle_core::prelude::*;

let mut theory = Theory::new();

// Facts
theory.add_fact("bird");
theory.add_fact("~guilty");  // Negated fact

// Strict rules
theory.add_strict_rule(&["penguin"], "bird");

// Defeasible rules
let r1 = theory.add_defeasible_rule(&["bird"], "flies");
let r2 = theory.add_defeasible_rule(&["penguin"], "~flies");

// Defeaters
theory.add_defeater(&["broken_wing"], "flies");

// Superiority
theory.add_superiority(&r2, &r1);
}

Parsing SPL

#![allow(unused)]
fn main() {
use spindle_parser::parse_spl;

let spl = r#"
    (given bird)
    (given penguin)
    (normally r1 bird flies)
    (normally r2 penguin (not flies))
    (prefer r2 r1)
"#;

let theory = parse_spl(spl)?;
}

Reasoning

Reasoning API

#![allow(unused)]
fn main() {
use spindle_core::reason::reason;

let conclusions = reason(&theory)?;
}

Convenience Method

#![allow(unused)]
fn main() {
// Uses standard algorithm
let conclusions = theory.reason()?;
}

Working with Conclusions

Conclusion Types

#![allow(unused)]
fn main() {
use spindle_core::conclusion::ConclusionType;

for c in &conclusions {
    match c.conclusion_type {
        ConclusionType::DefinitelyProvable => {
            println!("+D {}", c.literal);
        }
        ConclusionType::DefinitelyNotProvable => {
            println!("-D {}", c.literal);
        }
        ConclusionType::DefeasiblyProvable => {
            println!("+d {}", c.literal);
        }
        ConclusionType::DefeasiblyNotProvable => {
            println!("-d {}", c.literal);
        }
    }
}
}

Filtering Conclusions

#![allow(unused)]
fn main() {
// Positive conclusions only
let positive: Vec<_> = conclusions
    .iter()
    .filter(|c| c.conclusion_type.is_positive())
    .collect();

// Defeasibly provable only
let defeasible: Vec<_> = conclusions
    .iter()
    .filter(|c| c.conclusion_type == ConclusionType::DefeasiblyProvable)
    .collect();
}

Checking Specific Literals

#![allow(unused)]
fn main() {
fn is_provable(conclusions: &[Conclusion], name: &str) -> bool {
    conclusions.iter().any(|c| {
        c.conclusion_type == ConclusionType::DefeasiblyProvable
            && c.literal.name() == name
            && !c.literal.negation
    })
}

if is_provable(&conclusions, "flies") {
    println!("It flies!");
}
}

Terms

The Term enum represents typed values that appear as arguments in literals and as results of arithmetic expressions. Four variants cover the value space:

#![allow(unused)]
fn main() {
use spindle_core::term::{Term, FiniteFloat, NumericValue};
use spindle_core::intern::{SymbolId, intern};
use rust_decimal::Decimal;

// Symbol — an interned string identifier
let sym = Term::Symbol(intern("alice"));

// Integer — a 64-bit signed integer
let int = Term::Integer(42);

// Decimal — an arbitrary-precision decimal (exact representation)
let dec = Term::Decimal(Decimal::new(314, 2)); // 3.14

// Float — a canonicalized finite IEEE 754 f64
let flt = Term::Float(FiniteFloat::new(2.718).unwrap());
}

Convenience Conversions

Terms implement From for common types, so you can use .into():

#![allow(unused)]
fn main() {
let t: Term = 42i64.into();               // Term::Integer(42)
let t: Term = Decimal::ONE.into();         // Term::Decimal(1)
let t: Term = intern("bob").into();        // Term::Symbol(...)
let t: Term = FiniteFloat::new(1.0)
    .unwrap().into();                      // Term::Float(1.0)
}

Numeric Checks and Cross-Type Equality

Term::is_numeric() returns true for Integer, Decimal, and Float variants. Term::numeric_eq() supports cross-type comparison with widening promotion (Integer -> Decimal -> Float):

#![allow(unused)]
fn main() {
let a = Term::Integer(2);
let b = Term::Decimal(Decimal::new(20, 1)); // 2.0
assert!(a.numeric_eq(&b)); // true — same mathematical value

let c = Term::Float(FiniteFloat::new(2.0).unwrap());
assert!(a.numeric_eq(&c)); // true
}

Symbols are never numerically equal to anything (including other symbols).

NumericValue

NumericValue is a guaranteed-numeric counterpart to Term (no Symbol variant). Convert with Term::to_numeric_value():

#![allow(unused)]
fn main() {
let term = Term::Integer(10);
if let Some(nv) = term.to_numeric_value() {
    println!("Numeric: {}", nv); // "10"
}

// Convert back (Float variant rejects NaN/Inf)
let back: Term = NumericValue::Integer(10).try_into().unwrap();
}

FiniteFloat

FiniteFloat wraps f64 with two invariants: it rejects NaN and infinity, and normalizes -0.0 to +0.0. This makes it safe to use as a hash-map key with stable Eq and Hash implementations.

#![allow(unused)]
fn main() {
let f = FiniteFloat::new(3.14).unwrap();
assert_eq!(f.value(), 3.14);

// NaN and infinity are rejected
assert!(FiniteFloat::new(f64::NAN).is_none());
assert!(FiniteFloat::new(f64::INFINITY).is_none());

// Negative zero normalizes to positive zero
let a = FiniteFloat::new(0.0).unwrap();
let b = FiniteFloat::new(-0.0).unwrap();
assert_eq!(a, b);
}

Literals

Creating Literals

#![allow(unused)]
fn main() {
use spindle_core::literal::Literal;

let simple = Literal::simple("bird");
let negated = Literal::negated("flies");
let with_args = Literal::new(
    "parent",
    false,  // not negated
    Default::default(),  // no mode
    Default::default(),  // no temporal
    vec!["alice".to_string(), "bob".to_string()],
);
}

Literal Properties

#![allow(unused)]
fn main() {
let lit = Literal::negated("flies");

println!("Name: {}", lit.name());           // "flies"
println!("Negated: {}", lit.is_negated());  // true
println!("Canonical: {}", lit.canonical_name()); // "~flies"

let complement = lit.complement();  // Literal::simple("flies")
}

Rules

Creating Rules Directly

#![allow(unused)]
fn main() {
use spindle_core::rule::{Rule, RuleType};

let rule = Rule::new(
    "r1",
    RuleType::Defeasible,
    vec![Literal::simple("bird")],
    vec![Literal::simple("flies")],
);

theory.add_rule(rule);
}

Inspecting Rules

#![allow(unused)]
fn main() {
for rule in theory.rules() {
    println!("Label: {}", rule.label);
    println!("Type: {:?}", rule.rule_type);
    println!("Body: {:?}", rule.body);
    println!("Head: {:?}", rule.head);
}
}

Pipeline

The preparation pipeline transforms a raw Theory into a form ready for reasoning. It is built from composable stages assembled via PipelineBuilder.

Default Pipeline

The simplest way to prepare a theory uses prepare() with default options:

#![allow(unused)]
fn main() {
use spindle_core::pipeline::{prepare, PrepareOptions};

let result = prepare(&theory, PrepareOptions::default())?;
let prepared_theory = result.theory;
}

PipelineBuilder

For fine-grained control, build a custom pipeline from individual stages:

#![allow(unused)]
fn main() {
use spindle_core::pipeline::{Pipeline, Validate, WildcardRewrite, Ground};

let pipeline = Pipeline::builder()
    .stage(Validate::default())
    .stage(WildcardRewrite)
    .stage(Ground::default())
    .build();

let (prepared_theory, ctx) = pipeline.run(theory)?;
}

Stages run left-to-right. Each stage receives the theory produced by the previous stage and a shared PipelineContext.

You can insert a stage at a specific position with stage_at():

#![allow(unused)]
fn main() {
use spindle_core::pipeline::{Pipeline, Validate, WildcardRewrite, Ground, TemporalFilter};
use spindle_core::temporal::TimePoint;

let pipeline = Pipeline::builder()
    .stage(Validate::default())
    .stage(WildcardRewrite)
    .stage(Ground::default())
    .stage_at(0, TemporalFilter { reference_time: TimePoint::Moment(1700000000000) })
    .build();
}

Built-in Stages

Configuring Stages

#![allow(unused)]
fn main() {
use spindle_core::pipeline::{Validate, Ground};

// Disable range restriction check
let validate = Validate {
    enforce_range_restricted: false,
    reject_wildcard_in_head: true,
};

// Increase grounding limits
let ground = Ground {
    max_iterations: 200,
    max_instances: 50000,
};
}

Implementing Custom Stages

Any type implementing the PipelineStage trait can be added to a pipeline:

#![allow(unused)]
fn main() {
use spindle_core::pipeline::{PipelineStage, PipelineContext, Severity, Diagnostic};
use spindle_core::theory::Theory;
use spindle_core::error::Result;

#[derive(Debug)]
struct LogRuleCount;

impl PipelineStage for LogRuleCount {
    fn name(&self) -> &'static str { "LogRuleCount" }

    fn apply(&self, theory: Theory, ctx: &mut PipelineContext) -> Result<Theory> {
        ctx.diagnostics.push(Diagnostic {
            severity: Severity::Info,
            stage: self.name(),
            message: format!("Theory has {} rules", theory.rules().len()),
        });
        Ok(theory)
    }
}
}

PipelineContext and Diagnostics

A PipelineContext is threaded through all stages, collecting diagnostics and inter-stage metadata.

#![allow(unused)]
fn main() {
use spindle_core::pipeline::{Pipeline, Validate, WildcardRewrite, Ground, Severity, MetadataVal};

let pipeline = Pipeline::builder()
    .stage(Validate::default())
    .stage(WildcardRewrite)
    .stage(Ground::default())
    .build();

let (prepared, ctx) = pipeline.run(theory)?;

// Inspect diagnostics
for diag in &ctx.diagnostics {
    match diag.severity {
        Severity::Error   => eprintln!("[{}] ERROR: {}", diag.stage, diag.message),
        Severity::Warning => eprintln!("[{}] WARN:  {}", diag.stage, diag.message),
        Severity::Info    => println!("[{}] INFO:  {}", diag.stage, diag.message),
    }
}

// Read metadata set by stages (e.g., grounding statistics)
if let Some(MetadataVal::Usize(n)) = ctx.metadata.get("grounding_instances") {
    println!("Grounding produced {} instances", n);
}
if let Some(MetadataVal::Bool(true)) = ctx.metadata.get("grounding_limit_hit") {
    eprintln!("Warning: grounding limit was reached");
}
}

PrepareOptions

The prepare() function builds a full pipeline from PrepareOptions, including optional temporal filtering and grounding configuration:

#![allow(unused)]
fn main() {
use spindle_core::pipeline::{prepare, PrepareOptions, GroundingOptions, ValidationOptions};
use spindle_core::temporal::TimePoint;

let opts = PrepareOptions {
    reference_time: Some(TimePoint::Moment(1700000000000)),
    grounding: GroundingOptions {
        enabled: true,
        max_iterations: 100,
        max_instances: 10000,
    },
    validation: ValidationOptions {
        enforce_range_restricted: true,
        reject_wildcard_in_head: true,
    },
    trust_policy: None,
};

let result = prepare(&theory, opts)?;

// Access the prepared theory and grounding statistics
let theory = result.theory;
println!("Grounded: {}", result.grounding_report.performed);
println!("Instances: {}", result.grounding_report.instances);
if result.grounding_report.limit_hit {
    eprintln!("Grounding stopped early due to limits");
}
}

Query Operators

What-If

#![allow(unused)]
fn main() {
use spindle_core::query::{what_if, HypotheticalClaim};
use spindle_core::literal::Literal;

let hypotheticals = vec![
    HypotheticalClaim::new(Literal::simple("wounded"))
];
let goal = Literal::negated("flies");

let result = what_if(&theory, hypotheticals, &goal)?;
if result.is_provable() {
    println!("Would be provable with those facts");
}
for lit in result.newly_provable() {
    println!("Newly provable: {}", lit);
}
}

Why-Not

#![allow(unused)]
fn main() {
use spindle_core::query::why_not;
use spindle_core::literal::Literal;

let literal = Literal::simple("flies");
let explanation = why_not(&theory, &literal)?;
for blocker in &explanation.blocked_by {
    println!("Blocked by: {}", blocker.explanation);
}
}

Abduction

#![allow(unused)]
fn main() {
use spindle_core::query::abduce;
use spindle_core::literal::Literal;

let goal = Literal::simple("goal");
let result = abduce(&theory, &goal, 3)?;
for solution in &result.solutions {
    println!("Solution: {:?}", solution.facts);
}
}

Error Handling

#![allow(unused)]
fn main() {
use spindle_core::error::{SpindleError, Result};
use spindle_parser::parse_spl;

fn load_theory(path: &str) -> Result<Theory> {
    let content = std::fs::read_to_string(path)?;

    if path.ends_with(".spl") {
        parse_spl(&content).map_err(|e| SpindleError::Parse(e.to_string()))
    } else {
        Err(SpindleError::Parse("Unknown format".to_string()))
    }
}
}

Advanced: Indexed Theory

For multiple queries, build an indexed theory once:

#![allow(unused)]
fn main() {
use spindle_core::index::IndexedTheory;

let indexed = IndexedTheory::build(theory.clone());

// O(1) lookups
for rule in indexed.rules_with_head(&literal) {
    // Process rules that conclude this literal
}

for rule in indexed.rules_with_body(&literal) {
    // Process rules that have this literal in body
}
}

Thread Safety

Theory and Conclusion are Send + Sync. You can:

#![allow(unused)]
fn main() {
use std::sync::Arc;
use rayon::prelude::*;

let theory = Arc::new(theory);

let results: Vec<_> = queries
    .par_iter()
    .map(|query| {
        let t = theory.clone();
        process_query(&t, query)
    })
    .collect();
}

Example: Complete Application

use spindle_core::prelude::*;
use spindle_parser::parse_spl;
use std::fs;

fn main() -> Result<()> {
    // Load theory
    let content = fs::read_to_string("rules.spl")?;
    let mut theory = parse_spl(&content)?;

    // Add runtime facts
    theory.add_fact("current_user_admin");

    // Reason
    let conclusions = theory.reason()?;

    // Check permissions
    let can_delete = conclusions.iter().any(|c| {
        c.conclusion_type == ConclusionType::DefeasiblyProvable
            && c.literal.name() == "can_delete"
    });

    if can_delete {
        println!("User can delete");
    } else {
        println!("Permission denied");
    }

    Ok(())
}

WebAssembly Integration

Spindle compiles to WebAssembly for use in browsers and Node.js.

Building

Prerequisites

cargo install wasm-pack

Build for Web

cd crates/spindle-wasm
wasm-pack build --target web --release

Build for Node.js

wasm-pack build --target nodejs --release

Build for Bundlers (webpack, etc.)

wasm-pack build --target bundler --release

Installation

npm/yarn

npm install spindle-wasm
# or
yarn add spindle-wasm

From Local Build

// Point to your build output
import init, { Spindle } from './pkg/spindle_wasm.js';

Browser Usage

ES Modules

<script type="module">
import init, { Spindle } from './pkg/spindle_wasm.js';

async function main() {
    await init();

    const spindle = new Spindle();
    spindle.addFact("bird");
    spindle.addFact("penguin");
    spindle.addDefeasibleRule(["bird"], "flies");
    spindle.addDefeasibleRule(["penguin"], "~flies");
    spindle.addSuperiority("r2", "r1");

    const conclusions = spindle.reason();
    console.log(conclusions);
}

main();
</script>

With Bundler (Vite, webpack)

import init, { Spindle } from 'spindle-wasm';

async function setup() {
    await init();
    return new Spindle();
}

const spindle = await setup();

Node.js Usage

const { Spindle } = require('spindle-wasm');

const spindle = new Spindle();

spindle.parseSpl(`
    (given bird)
    (given penguin)
    (normally r1 bird flies)
    (normally r2 penguin (not flies))
    (prefer r2 r1)
`);

const conclusions = spindle.reason();
console.log(conclusions);

API Reference

Constructor

const spindle = new Spindle();

Creates a new empty theory.

Adding Facts

spindle.addFact("bird");
spindle.addFact("~guilty");  // Negated fact

Adding Rules

// Defeasible rules
spindle.addDefeasibleRule(["bird"], "flies");
spindle.addDefeasibleRule(["bird", "healthy"], "strong_flyer");

// Strict rules
spindle.addStrictRule(["penguin"], "bird");

// Defeaters
spindle.addDefeater(["broken_wing"], "flies");

Superiority

spindle.addSuperiority("r2", "r1");  // r2 > r1

Parsing

// Parse SPL
spindle.parseSpl(`
    (given bird)
    (normally r1 bird flies)
`);

Reasoning

const conclusions = spindle.reason();
// Returns: Array of conclusion objects

// Each conclusion:
{
    conclusion_type: "+D" | "-D" | "+d" | "-d",
    literal: string,
    positive: boolean
}

Query

// Check if a literal is provable
const result = spindle.query("flies");
// Returns: { status: "provable" | "not_provable", literal, conclusion_type }

What-If

const result = spindle.whatIf(["wounded"], "~flies");
// Returns: { provable: boolean, new_conclusions: Array, changed_conclusions: Array }

Why-Not

const explanation = spindle.whyNot("flies");
// Returns: { literal, is_provable, would_derive, blockers: Array }

Abduction

const solutions = spindle.abduce("goal", 3);
// Returns: { goal, solutions: Array<{ facts: string[], rules_used: string[], confidence: number }> }

Reset

spindle.clear();  // Clear all rules and facts

TypeScript Types

interface Conclusion {
    conclusion_type: "+D" | "-D" | "+d" | "-d";
    literal: string;
    positive: boolean;
}

interface QueryResult {
    status: "provable" | "not_provable";
    literal: string;
    conclusion_type?: string;
}

interface WhatIfResult {
    provable: boolean;
    new_conclusions: Conclusion[];
    changed_conclusions: ChangedConclusion[];
}

interface WhyNotExplanation {
    literal: string;
    is_provable: boolean;
    would_derive: string | null;
    blockers: Blocker[];
}

interface Blocker {
    blocking_type: "MissingPremise" | "Defeated" | "Contradicted";
    rule_label: string;
    blocking_rule: string | null;
    explanation: string;
}

interface AbductionResult {
    goal: string;
    solutions: AbductionSolution[];
}

interface AbductionSolution {
    facts: string[];
    rules_used: string[];
    confidence: number;
}

interface ChangedConclusion {
    literal: string;
    old_type: string;
    new_type: string;
}

Complete Example

import init, { Spindle } from 'spindle-wasm';

async function reasonAboutPenguins() {
    await init();

    const spindle = new Spindle();

    // Build theory
    spindle.parseSpl(`
        (given bird)
        (given penguin)

        (normally r1 bird flies)
        (normally r2 bird has-feathers)
        (normally r3 penguin (not flies))
        (normally r4 penguin swims)

        (prefer r3 r1)
    `);

    // Reason
    const conclusions = spindle.reason();

    // Filter positive conclusions
    const positive = conclusions.filter(c =>
        c.conclusion_type === "+D" || c.conclusion_type === "+d"
    );

    console.log("Provable:", positive.map(c => c.literal));

    // Query specific literal
    const fliesResult = spindle.query("flies");
    console.log("Does it fly?", fliesResult.status);

    // What-if analysis
    const whatIf = spindle.whatIf(["super_bird"], "flies");
    console.log("With super_bird:", whatIf.provable);

    // Explain why not
    if (fliesResult.status === "not_provable") {
        const explanation = spindle.whyNot("flies");
        console.log("Why not flies:", explanation.blockers);
    }
}

reasonAboutPenguins();

React Integration

import { useState, useEffect } from 'react';
import init, { Spindle } from 'spindle-wasm';

function useSpindle() {
    const [spindle, setSpindle] = useState<Spindle | null>(null);
    const [loading, setLoading] = useState(true);

    useEffect(() => {
        init().then(() => {
            setSpindle(new Spindle());
            setLoading(false);
        });
    }, []);

    return { spindle, loading };
}

function ReasoningComponent() {
    const { spindle, loading } = useSpindle();
    const [conclusions, setConclusions] = useState([]);

    const reason = () => {
        if (!spindle) return;

        spindle.reset();
        spindle.addFact("bird");
        spindle.addDefeasibleRule(["bird"], "flies");

        const result = spindle.reason();
        setConclusions(result);
    };

    if (loading) return <div>Loading WASM...</div>;

    return (
        <div>
            <button onClick={reason}>Reason</button>
            <ul>
                {conclusions.map((c, i) => (
                    <li key={i}>{c.conclusion_type} {c.literal}</li>
                ))}
            </ul>
        </div>
    );
}

Performance Notes

1. Initialize once: Call init() once at startup
2. Reuse Spindle instances: Create once, reset between uses
3. Batch operations: Add all rules before reasoning
4. Use explicit superiority for conflict-heavy theories to avoid unresolved ties

Bundle Size

Approximate sizes (gzipped):

• Core WASM: ~150KB
• JavaScript bindings: ~10KB

Browser Compatibility

Requires WebAssembly support:

• Chrome 57+
• Firefox 52+
• Safari 11+
• Edge 16+
• Node.js 8+

Architecture

This document describes the internal architecture of Spindle-Rust.

Crate Structure

spindle-rust/
├── crates/
│   ├── spindle-core/     # Core reasoning engine
│   ├── spindle-parser/   # SPL parser
│   ├── spindle-cli/      # Command-line interface
│   └── spindle-wasm/     # WebAssembly bindings

spindle-core

The core reasoning engine with these modules:

spindle-core/src/
├── lib.rs              # Crate root, prelude
├── intern.rs           # String interning (SymbolId, LiteralId)
├── literal.rs          # Literal representation
├── mode.rs             # Modal operators
├── temporal.rs         # Temporal reasoning (Allen relations, TimePoint)
├── term.rs             # Terms (Symbol, Numeric: Integer/Decimal/Float)
├── rule.rs             # Rule types
├── body.rs             # Body literals (BodyLogicLiteral, BodyArg, ArithConstraint)
├── superiority.rs      # Superiority relations
├── theory.rs           # Theory container
├── conclusion.rs       # Conclusion types (+D, -D, +d, -d)
├── claims.rs           # Claims blocks (provenance metadata)
├── index.rs            # Theory indexing (AtomKey, LitId)
├── arith.rs            # Arithmetic expressions and constraints
├── grounding.rs        # Variable grounding (bottom-up Datalog)
├── worklist.rs         # Worklist data structures
├── trust.rs            # Trust-weighted reasoning
├── mining.rs           # Process mining (alpha algorithm)
├── error.rs            # Error types
├── analysis/           # Theory analysis
│   ├── mod.rs          #   Shared types (ValidationDiagnostic, ConflictReport)
│   ├── conflicts.rs    #   Conflict detection
│   ├── superiority.rs  #   Superiority suggestion
│   └── validation.rs   #   Semantic validation
├── explanation/        # Explanation system
│   ├── mod.rs          #   Proof/derivation tree structures
│   ├── types.rs        #   Core explanation types
│   └── format/         #   Output formats
│       ├── mod.rs
│       ├── natural_language.rs
│       ├── json.rs
│       ├── jsonld.rs
│       └── dot.rs
├── pipeline/           # Composable preparation pipeline
│   ├── mod.rs          #   PipelineStage trait, PipelineBuilder, prepare()
│   ├── validate.rs     #   Validate stage
│   ├── wildcard.rs     #   WildcardRewrite stage
│   ├── ground.rs       #   Ground stage
│   └── temporal.rs     #   TemporalFilter, TemporalVarValidation stages
├── query/              # Query operators
│   ├── mod.rs          #   QueryOperator trait
│   ├── what_if.rs      #   Hypothetical reasoning
│   ├── why_not.rs      #   Failure explanation
│   ├── abduce.rs       #   Abduction (hypothesis finding)
│   └── requires.rs     #   Dependency queries
└── reason/             # Reasoning engine
    ├── mod.rs          #   Reasoner trait, StandardReasoner
    ├── state.rs        #   ReasoningState (worklist, proven sets, counters)
    ├── facts.rs        #   Fact initialization phase
    ├── definite.rs     #   Definite (+D/-D) forward chaining
    └── defeasible.rs   #   Defeasible (+d/-d) forward chaining

Data Flow

Input (SPL)
      │
      ▼
┌─────────────┐
│   Parser    │  spindle-parser
└─────────────┘
      │
      ▼
┌─────────────┐
│   Theory    │  Rules, facts, superiority
└─────────────┘
      │
      ▼
┌─────────────────────────────────────────┐
│  Pipeline  (composable stages)          │
│  ┌──────────────────┐                   │
│  │ TemporalFilter   │ (optional as-of)  │
│  ├──────────────────┤                   │
│  │ Validate         │ range restriction │
│  ├──────────────────┤                   │
│  │ WildcardRewrite  │ _ → ?_wN          │
│  ├──────────────────┤                   │
│  │ Ground           │ variable inst.    │
│  ├──────────────────┤                   │
│  │ TemporalVarValid.│ reject unresolved │
│  ├──────────────────┤                   │
│  │ TemporalFilter   │ (optional re-filt)│
│  └──────────────────┘                   │
└─────────────────────────────────────────┘
      │
      ▼
┌─────────────┐
│   Index     │  Build lookup tables (AtomKey, LitId)
└─────────────┘
      │
      ▼
┌─────────────┐
│  Reasoning  │  StandardReasoner — DL(d)
└─────────────┘
      │
      ▼
┌─────────────┐
│ Conclusions │  +D, -D, +d, -d
└─────────────┘

Pipeline Architecture

The preparation pipeline transforms a raw Theory into a form ready for reasoning. It is built from composable stages, each implementing the PipelineStage trait.

PipelineStage Trait

#![allow(unused)]
fn main() {
pub trait PipelineStage: std::fmt::Debug {
    /// Human-readable name used in diagnostics and tracing.
    fn name(&self) -> &'static str;

    /// Apply this stage, returning a (possibly transformed) theory.
    /// Returning Err aborts the pipeline.
    fn apply(&self, theory: Theory, ctx: &mut PipelineContext) -> Result<Theory>;
}
}

Stages are assembled with PipelineBuilder and run left-to-right:

#![allow(unused)]
fn main() {
use spindle_core::pipeline::{Pipeline, Validate, WildcardRewrite, Ground};

let pipeline = Pipeline::builder()
    .stage(Validate::default())
    .stage(WildcardRewrite)
    .stage(Ground::default())
    .build();

let (prepared_theory, ctx) = pipeline.run(theory)?;
}

Built-in Stages

PipelineContext

A PipelineContext is threaded through all stages, carrying:

• diagnostics: Vec<Diagnostic> — Info, Warning, and Error messages emitted by stages. Each diagnostic records the stage name and a human-readable message.
• metadata: HashMap<String, MetadataVal> — Arbitrary key-value data for inter-stage communication (e.g., grounding_instances, grounding_limit_hit, evaluated_at).

Default Pipeline

Pipeline::default_pipeline() returns Validate → WildcardRewrite → Ground. The higher-level prepare() function builds a richer pipeline from PrepareOptions, optionally inserting TemporalFilter (before and after grounding) and TemporalVarValidation.

Key Design Decisions

String Interning

All literal names are interned to reduce memory and enable O(1) comparisons.

#![allow(unused)]
fn main() {
// intern.rs
pub struct SymbolId(u32);   // Interned string ID
pub struct LiteralId(u32);  // Interned literal (name + negation)

// Convert string to ID (only allocates once per unique string)
let id = intern("bird");

// Compare IDs (O(1), no string comparison)
if id1 == id2 { ... }

// Resolve back to string when needed
let name = resolve(id);
}

Benefits:

• HashSetLiteralId uses 4 bytes per entry vs ~24+ for String
• No heap allocation in hot reasoning loops
• O(1) equality checks

Indexed Theory

Rules are indexed by head and body literals for O(1) lookup.

#![allow(unused)]
fn main() {
// index.rs
pub struct IndexedTheory {
    theory: Theory,
    by_head: HashMap<LiteralId, Vec<&Rule>>,
    by_body: HashMap<LiteralId, Vec<&Rule>>,
}

// O(1) lookup instead of O(n) scan
indexed.rules_with_head(&literal)
indexed.rules_with_body(&literal)
}

LiteralId Design

A LiteralId packs symbol ID and negation into a single u32:

#![allow(unused)]
fn main() {
pub struct LiteralId(u32);

impl LiteralId {
    // High bit = negation flag
    // Lower 31 bits = symbol ID

    pub fn is_negated(&self) -> bool {
        (self.0 & 0x8000_0000) != 0
    }

    pub fn symbol(&self) -> SymbolId {
        SymbolId(self.0 & 0x7FFF_FFFF)
    }

    pub fn complement(&self) -> LiteralId {
        LiteralId(self.0 ^ 0x8000_0000)
    }
}
}

This allows:

• O(1) negation check
• O(1) complement computation
• Efficient hash set storage

Superiority Index

Superiority relations are indexed for O(1) lookup:

#![allow(unused)]
fn main() {
pub struct SuperiorityIndex {
    // superior -> set of inferior rules
    superiors: HashMap<RuleLabel, HashSet<RuleLabel>>,
}

// O(1) check
theory.is_superior("r1", "r2")
}

Algorithm Implementation

Reasoner Trait

The Reasoner trait abstracts over reasoning backends. One concrete implementation is provided:

• StandardReasoner — the standard DL(d) forward-chaining algorithm (the default and only built-in backend).

Use select_reasoner("standard") to obtain a boxed trait object for runtime backend selection. Additional backends can be added by implementing the Reasoner trait.

Standard DL(d) (reason/)

The reasoning state (worklist, proven sets, body counters, conclusions) is consolidated into ReasoningState in reason/state.rs. The algorithm proceeds in three phases, each in its own submodule:

Phase 1: Fact initialization (reason/facts.rs)
  ├── Add to definite_proven
  ├── Add to defeasible_proven
  └── Add to worklist

Phase 2: Definite forward chaining (reason/definite.rs)
  while worklist not empty:
    ├── Pop literal
    ├── Find rules with literal in body
    ├── Decrement body counters
    └── If counter = 0:
        ├── Strict → add +D, +d
        ├── Defeasible → (handled in phase 3)
        └── Defeater → (no conclusion)

Phase 3: Defeasible forward chaining (reason/defeasible.rs)
  for defeasible rules with all body literals proven:
    ├── Check ambiguity blocking (complement, team defeat)
    ├── Check superiority relations
    └── If unblocked → add +d

Phase 4: Negative conclusions
  for each literal:
    ├── If not in definite_proven → -D
    └── If not in defeasible_proven → -d

Uses LitId (4-byte Copy type) and BitSet for O(1) proven literal checks, eliminating heap allocations and hash computations in the hot reasoning loop.

Memory Layout

Theory

#![allow(unused)]
fn main() {
pub struct Theory {
    rules: Vec<Rule>,
    superiorities: Vec<Superiority>,
    meta: HashMap<String, Meta>,
}

pub struct Rule {
    label: String,
    rule_type: RuleType,     // 1 byte + padding
    body: SmallVec<[Literal; 4]>,  // inline for ≤4 elements
    head: SmallVec<[Literal; 4]>,
}

pub struct Literal {
    name: String,            // 24 bytes (String)
    negation: bool,          // 1 byte + padding
    mode: Option<Mode>,      // 1-2 bytes + padding
    temporal: Option<...>,   // Variable
    predicates: Vec<String>, // 24 bytes (Vec)
}
}

Optimized Representation (reasoning)

#![allow(unused)]
fn main() {
// During reasoning, we use IDs instead of strings
proven: BitSet  // bitmap indexed by LiteralId
worklist: VecDeque`LiteralId`
}

Extension Points

Adding a Pipeline Stage

1. Implement the PipelineStage trait
2. Add the struct to pipeline/ (new file or existing)
3. Re-export from pipeline/mod.rs
4. Insert into pipelines with PipelineBuilder::stage() or stage_at()

Adding a New Rule Type

1. Add variant to RuleType enum
2. Update parser (spl.rs)
3. Update reasoning logic in reason/
4. Add tests

Adding a New Query Operator

1. Implement the QueryOperator trait in a new file under query/
2. Re-export from query/mod.rs
3. Add to WASM bindings if needed
4. Document in guides/queries.md

Adding a Reasoning Backend

1. Implement the Reasoner trait
2. Register in select_reasoner() for runtime dispatch
3. Add tests

Process Mining Pipeline

The mining module provides:

• Event log → Footprint matrix → Petri net discovery (alpha algorithm)
• Conflict detection (choice/mutex patterns)
• Rule learning with support/confidence metrics

Adding Temporal Features

1. Extend temporal.rs
2. Update literal matching in grounding.rs
3. Update parsers for new syntax

Testing Strategy

tests/
├── Unit tests (per module, inline #[cfg(test)])
│   ├── reason/ - phase-isolated tests
│   ├── pipeline/ - per-stage tests
│   ├── query/ - operator tests
│   └── ...
├── Integration tests (crates/spindle-core/tests/)
│   ├── difftest.rs - proptest random theory gen (500 cases)
│   └── ...
├── Parser tests
│   └── spl.rs
└── WASM tests
    └── Basic functionality

Key Test Categories

1. Basic reasoning: facts, rules, chains
2. Conflict resolution: superiority, defeaters
3. Edge cases: cycles, empty, self-reference
4. Pipeline stages: validation, grounding, temporal filtering
5. Differential testing: proptest-generated random theories

Performance Characteristics

Where:

• n = number of rules
• m = average body size

Dependencies

Core dependencies:

• rustc-hash - Fast hash function for internal HashMaps
• smallvec - Inline storage for small vectors (rule body/head)

Parser dependencies:

• nom - Parser combinator library

WASM dependencies:

• wasm-bindgen - Rust/JavaScript interop
• serde - JSON serialization

Optimization Notes

This document records optimization attempts and findings for future reference.

Lattice-Based Memoization (February 2026)

Motivation

The is_blocked_by_superior function in reason.rs checks if a defeasible rule is blocked by attacking rules. The hypothesis was that:

1. Multiple rules deriving the same head would check the same attackers
2. Caching attacker status could avoid repeated O(body_size) checks
3. A lattice-based approach (inspired by Ascent) could formalize memoization

Approaches Tried

1. ProofStatus Lattice with Memoization

Created a ProofStatus enum representing lattice positions:

#![allow(unused)]
fn main() {
enum ProofStatus {
    Unknown,           // ⊥
    BlockedByDelta,    // Terminal false
    NotInLambda,       // Terminal false
    NoSupport,         // Pending
    HasSupport,        // Pending
    AllAttacksDefeated,// Ready to prove
    ProvedInPartial,   // ⊤
}
}

Result: Correct semantically, but added 5-15% overhead due to HashMap operations.

2. BlockedByChecker with Conservative Invalidation

Cached active attackers per complement literal, clearing cache when proven set grew.

Result: Cache was cleared too often, providing no benefit.

3. Incremental Invalidation

Tracked pending_body_literals for each cache entry, only invalidating when relevant literals were proven.

Result: Reduced unnecessary invalidation, but overhead still exceeded savings. Cloning the proven HashSet for snapshot tracking was expensive.

4. Lazy Attacker Tracking

Tracked attacker activation incrementally (like rule body counters), avoiding body satisfaction checks entirely.

#![allow(unused)]
fn main() {
struct LazyAttackerTracker {
    attacker_remaining: FxHashMap<String, usize>,
    active_attackers: FxHashMap<LiteralId, Vec<String>>,
    attacker_heads: FxHashMap<String, LiteralId>,
}
}

Result: 10-80% slower due to HashMap operations and string allocations.

Benchmark Results

multi_target_blocked (M targets × N defenders):
  5x10:   standard ~44µs,  lazy ~53µs (+20%),  memoized ~51µs (+16%)
  10x10:  standard ~88µs,  lazy ~100µs (+14%), memoized ~106µs (+20%)
  20x10:  standard ~164µs, lazy ~299µs (+82%), memoized ~228µs (+39%)
  10x20:  standard ~180µs, lazy ~215µs (+19%), memoized ~230µs (+28%)

Why All Approaches Failed

The original is_blocked_by_superior is already well-optimized:

#![allow(unused)]
fn main() {
for attacker in attacking_rules {           // O(1) lookup via IndexedTheory
    let satisfied = attacker.body.iter()    // Small vector (~1-3 elements)
        .all(|b| proven.contains(&b));      // O(1) HashSet lookup
    // Superiority check is O(1) via SuperiorityIndex
}
}

Key factors:

1. Operation is already cheap - Small vectors, O(1) lookups
2. Single-pass algorithm - Each literal checked once, no reuse opportunity
3. Cache overhead exceeds savings - HashMap ops, allocations, tracking state

When Memoization Would Help

Existing Optimizations (Already Effective)

1. LiteralId - 4-byte interned identifier, O(1) comparison
2. SuperiorityIndex - O(1) superiority lookup
3. IndexedTheory - O(1) rule lookup by head/body
4. HashSet<LiteralId> - 4 bytes per entry vs ~24 for String

Alternative Optimizations (Not Tried)

If future profiling shows is_blocked_by_superior as a bottleneck:

1. Bit vectors - Replace HashSet with bit vector for proven literals
2. Arena allocation - Pre-allocate rules in contiguous memory
3. Rule ordering - Process rules in topological order
4. SIMD body checks - Vectorize body satisfaction for large bodies

Lessons Learned

1. Profile before optimizing - The target operation was already efficient
2. Single-pass algorithms resist caching - No repeated queries means no cache hits
3. Cache overhead matters - HashMap operations can exceed saved computation
4. Simple code is often fastest - Direct iteration beats fancy data structures

Code Location

The experimental code is on branch feature/lattice-proof-memoization:

8af967a feat(lattice): add lattice-based proof status memoization
9dd60e0 feat(lattice): add BlockedByChecker for is_blocked_by_superior
33e9923 perf(lattice): implement incremental cache invalidation
241d5e9 bench: add memoization comparison benchmarks
270aa98 experiment: add reason_lazy with lazy attacker tracking

The lattice module (lattice.rs) and memoized/lazy functions remain available for reference but are not used in production.