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 (later Data61/CSIRO, now CSIRO Technology)
• 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. Stronger evidence can defeat its conclusions. Classical logic only adds conclusions when new information arrives. Defeasible logic can revise conclusions when conflicting evidence appears.

Tractable inference makes defeasible logic practical where other non-monotonic formalisms are intractable. Algorithms explains theoretical complexity and the separate cost of grounding first-order variables.

; 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

• Rules and reasoning: facts, strict rules, defeasible rules, and defeaters. The engine implements traditional ambiguity-blocking DL(∂) with constructive negative tags.
• Variables and time: Datalog-style grounding with ?x syntax; Allen interval algebra with 13 temporal relations.
• Queries: status queries, what-if, why-not, abduction, and verified requirements.
• Aggregation and extensions: grouped sum, count, minimum, and maximum over completed predicates; host-registered pure functions and named aggregators.
• Vocabulary and verification: predicate declarations, metadata, and non-semantic shape diagnostics. Lean models and Rust/Lean differential tests cover supported fragments.
• Trust-aware reasoning: source attribution and weighted conclusions.
• Input and integration: Lisp-based SPL with variable, temporal, and trust directives; WebAssembly support for browsers and Node.js.

The linked pages describe current behavior and supported boundaries.

Entry Points

Getting Started covers CLI installation and a first theory. The Rust Library API describes library dependencies. Its basic example constructs the penguin theory, sets superiority, and obtains conclusions with Theory::reason().

Crate Structure

References

• SPINdle Project - Original Java implementation by NICTA (later Data61/CSIRO, now CSIRO Technology)
• 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 tutorial installs Spindle-Rust and runs a theory where a penguin exception defeats the usual bird rule.

Installation

Use Rust 1.87 or newer (edition 2024).

Building from Source

git clone https://git.anuna.io/anuna-research/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).

Next steps

The result +d ~flies completes this tutorial: the explicit priority resolves the conflict.

• Inspect the theory with CLI filters, JSON output, syntax checks, and statistics.
• Rust library covers programmatic theory construction.
• Concepts explains the proof tags and rule types.
• SPL reference describes the complete syntax.
• Variables and grounding explains rules 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. The declared priority makes "penguins don't fly" override "birds fly." Spindle does not infer this priority automatically from specificity.

(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 implication also makes the head 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) when every premise is definitely proved. With only defeasible support, a strict rule can instead contribute +d, subject to conflict checks. Aggregate snapshot premises also carry defeasible evidence. A definite conclusion cannot be defeated by a defeasible rule.

When to Use Strict Rules

Strict rules represent:

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

Defeasible Rules (normally)

Defeasible rules express typical or default behavior with possible 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

Defeasible rules represent:

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

Defeaters (except)

Defeaters are special rules that attack the complement of their head without proving the head. A defeater with head (not flies) blocks flies. An applicable defeater can itself be overcome by superiority.

(except d1 broken-wing (not 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 (not 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

Defeaters represent:

• Doubt without an assertion of the opposite
• Evidence that blocks a conclusion without proving its negation
• 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

When labels are omitted, Spindle generates them automatically:

(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?

Definite provability represents certainty in domains such as:

• Binding legal requirements
• Safety constraints
• Logical necessities

Defeasible Conclusions (+d / -d)

Defeasible provability extends definite provability with defeasible rules.

(given bird)
(normally r1 bird flies)

Conclusions:

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

The Relationship

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

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

Conflict and Ambiguity

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

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

Conclusions:

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

Both outcomes are ambiguous — neither can be proven.

Resolved Conflict

With superiority, the conflict is resolved:

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

Conclusions:

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

Example: Multi-Level

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

Conclusions:

Negative Conclusions

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

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

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

Reading Spindle Output

$ 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

The --positive flag restricts output to 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. The relation r3 > r1 needs its own explicit declaration:

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

Conflict Resolution Algorithm

When evaluating a defeasible conclusion:

1. The engine identifies all rules that can prove the literal.
2. The engine identifies all rules that can prove the complement (attackers).
3. Each attacker with a satisfied body faces a superiority check:
   • 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 neither opposing rule has priority, 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 (not 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

A definite proof wins over merely defeasible opposition, regardless of superiority. A strict rule has this protection when its premises are definitely proved:

(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 does not overturn definite proofs. It resolves defeasible conflicts, including strict rules used with only defeasible premises. Common cases include:

• Defeasible rules
• Defeasible rules and defeaters
• Defeaters

Priority Design

Specificity

Explicit priority lets a more specific rule override a general rule:

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

Priority Rationale

Comments explain why one rule beats another:

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

Cycles

Circular superiority creates a cycle:

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

This leads to undefined behavior.

Negation

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

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

Positive evidence and unknown results

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

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

Conflicts and definite evidence

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

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

Negated premises

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

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

Explicit defeasible defaults

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

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

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

Disjunctive Conditions

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 breaks the well-defined defeat and superiority semantics that make defeasible reasoning tractable.

Separate rules with the same head express disjunctive conditions:

; "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 standard encoding of disjunctive conditions preserves per-rule defeat. Overriding one path does not affect the other.

SPL Format Reference

SPL (Spindle Lisp) is the input language for Spindle. It replaces the earlier DFL syntax with a LISP-based DSL. Its s-expression structure supports new constructs without grammar ambiguity. These include temporal operators, trust directives, and claims blocks.

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 | predicate-decl
            | claims | trusts | decays | threshold

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

; Predicate declarations (SPEC-024)
predicate-decl   = "(predicate" functor argument-list ")"
argument-list    = "(" argument-decl* ")"
argument-decl    = "(" arg-name primitive-sort ")"
primitive-sort   = "symbol" | "integer" | "decimal" | "float" | "number" | "any"
predicate-target = "(predicate" functor arity ")"
arity            = "0" | non-zero-digit digit*

; 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 (not flies))

Unlabeled Rules

When labels are omitted, Spindle generates them automatically:

(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

The and form combines multiple conditions:

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

Disjunctive conditions

Rule bodies do not support or. Separate rules with the same head express disjunctive conditions. Disjunctive Conditions explains the rationale and gives an example.

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

The wildcard _ matches any value:

(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)

Predicate Declarations

A predicate declaration records the structure of a predicate: its ordered argument names and primitive sorts. This structure is independent of predicate usage. Declarations are not mandatory: undeclared predicates parse and reason exactly as before. A declaration adds no fact or rule; it only populates the theory's vocabulary.

(predicate assign-to
  ((task  symbol)
   (agent symbol)))

(predicate emergency ())        ; zero-arity predicate emergency/0

The number of argument declarations determines the arity, so assign-to/2 above has two positions and emergency/0 has none.

Inline Metadata

A declaration can carry trailing meta properties inline. This syntax replaces a separate (meta (predicate ...) ...) statement in the common case:

(predicate assign-to
  ((task  symbol)
   (agent symbol))
  (description "Assign a task to an agent.")
  (tags ("planning" "scheduling")))

Inline properties are exact sugar for the separate metadata target. Both forms populate the same predicate metadata store. The example equals a declaration plus a (meta (predicate assign-to 2) ...) statement with the same properties. Inline and separate metadata for the same predicate merge (later values win per key).

Primitive Sorts

Each argument declares one primitive sort. Sorts describe the value space only; they carry no domain meaning and do not affect inference.

The parser checks declarations. Argument names need non-empty, unique values; an unknown sort causes a parse error.

Predicate Indicators

For display and CLI interoperability, predicates use Prolog-style functor/arity notation, such as assign-to/2 or emergency/0. When a functor contains /, its display includes quotes: "rate/limit"/2. This notation is presentation only — the machine representation always keeps functor and arity as separate structured fields, never a parsed string.

Metadata

Metadata attaches to a rule by label or to a predicate by structured target:

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

Properties

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

Predicate Metadata Targets

A meta target can be a structured (predicate functor arity) selector instead of a label. This attaches metadata to one predicate symbol without overloading a rule label or parsing a predicate-indicator string:

(predicate assign-to ((task symbol) (agent symbol)))

(meta (predicate assign-to 2)
  (description "Assign a task to an agent."))

The metadata store distinguishes predicate targets from labels and other arities. Metadata for (predicate assign-to 2) never collides with a rule labelled assign-to, nor with assign-to/1. Predicate descriptions do not have to be declared — they can annotate any predicate the theory uses.

The Predicate Vocabulary

Declarations, predicate metadata, and observed rule usage together form a derived, read-only vocabulary. This catalogue uses predicate symbols as keys. Each entry carries a signature, a description, observed argument kinds per position, and the rule occurrences that reference the predicate. The vocabulary is a tooling projection — it never changes conclusions. See the Rust Library guide for the API (TheorySignature, Vocabulary).

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 supports interval variables such as (during p ?T) and all 13 Allen constraints in rule bodies. The within keyword names Allen's During relation, distinct from the during SPL wrapper. For example:

(given (during p 1 10))
(given (during q 20 30))
(normally sequence
  (and (during p ?T) (during q ?S) (before ?T ?S))
  ordered)

See Temporal Reasoning for interval propagation, state constraints, family matching, and as-of filtering.

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 (fixed 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

A bind assigns an arithmetic expression’s result to a variable:

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

Comparison Guards

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

Arithmetic promotes numeric types: 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 metadata when supplied.

(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 — RFC3339 timestamp for when the claim was made.
• :sig — signature string for verification.
• :id — block identifier.
• :note — 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

; Predicate declaration + metadata (optional structural documentation)
(predicate flies ())
(meta (predicate flies 0) (description "Capable of flight."))

; 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 (not flies))

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

Aggregation and extension calls

(given (payment alice first 10))
(given (payment alice second 10))
(normally total
  (agg ?total sum ?amount (payment ?person ?id ?amount))
  (total-payment ?total))

This derives (total-payment 20). Named aggregators are sum, count, min-of, and max-of. The output and contribution are variables; the contribution needs to occur in the single row pattern. For grouped results, earlier ordinary premises bind grouping variables. Separate helper predicates can express joins/filters.

Explicit folds remain available:

(normally total
  (bind ?total (fold + ?amount :from (payment ?person ?id ?amount) :initial 0))
  (total-payment ?total))

A fold appears directly in bind and has one :from pattern and either :initial expression or :require-nonempty. Nested folds require separate rules/strata. Aggregation is a rule premise, never a fact, head, or negated premise. The current bridge supports checked integer/symbol values; decimal/float, modal, temporal, and trust-weighted aggregate programs are unsupported.

bind also accepts registered extension calls. Unknown functions and invalid arities are preparation errors; parsing does not load host code. See Aggregation and Extension Functions for scoping, empty inputs, snapshot evidence, custom registries, and limits.

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

reason performs defeasible reasoning on a theory.

spindle reason examples/penguin.spl

--v2

--v2 selects 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

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

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

validate

validate checks 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

stats shows 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 reports whether 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

explain shows the derivation proof tree for a literal.

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

why-not explains 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

requires finds minimal sets of facts needed to derive a literal through abduction.

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. The reasoning engine checks each candidate set of facts to verify that it 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. Adding those assumptions to the theory makes the literal provable.

capabilities

capabilities lists the commands, features, and JSON schema versions this Spindle build supports. 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

explain-code reports 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. It provides guidance for unfamiliar error codes in JSON error envelopes.

JSON Envelope Schema Versions

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

Options

--json

--json outputs results in JSON format, including for validate and stats. The explain-code command does not accept this option. 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>

--at sets 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

--stdin reads 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

--positive shows 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

--debug-errors shows 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

Aggregate programs and query matching

spindle reason examples/aggregation.spl --json --v2
spindle query '(total-payment alice 20)' examples/aggregation.spl

Aggregation uses the normal reason and query commands without an extra flag. The CLI supplies the builtin function prelude. Registering custom functions is a Rust embedding API, not a CLI plugin-loading facility.

Bounded temporal goals match identical windows, including in requires. A containing window is not an exact match. Atemporal goals match any family member. See Query Operators.

Aggregation benchmark measurements

The suite measures prepare (including aggregate snapshots and grounding) and reason (preparation plus final reasoning) separately. Parsing, fixture creation, and expected-result assertions run outside the timed loops. These are pipeline measurements, not isolated reducer timings; allocation and result destruction are included. Each fixture checks the complete set of positive aggregate outputs through both entry points.

Coverage includes these fixture families:

Unique row IDs preserve repeated equal contributions. Chained stages consume derived results.

Sampling and output

Defaults use 10 samples, 0.5 seconds of warmup, and a 1-second measurement target per case. Expensive cases take longer when their iterations exceed that target. Criterion reports and local baselines reside under target/criterion/.

Initial local baseline

The initial run used an Apple M2, rustc 1.95.0, and the optimized bench profile on 2026-09-13. It used the defaults above with --save-baseline initial. All 50 timed cases passed their output checks. Selected Criterion mean estimates (milliseconds):

These short local measurements are a starting point, not portable performance thresholds. Row and unrelated-fact scaling warrant profiling. The measurements include grounding and reasoning costs, so they do not establish that fold scans alone cause the growth. Increasing group count also adds group facts and outputs; increasing stage count adds rules and intermediate outputs.

Benchmarking aggregation describes fixture checks, baseline comparisons, and longer measurements.

Algorithms

Spindle's built-in engine implements traditional ambiguity-blocking DL(∂) with team defeat and four constructive proof tags. StandardReasoner is the backend selected by select_reasoner("standard").

Proof propagation

Facts establish +D and therefore +d. Strict rules propagate definite proofs. Defeasible reasoning combines supported rules, negative definite evidence for the complement, and checks against opposing rules. A strict rule whose premises are only defeasibly proved can also contribute defeasible support.

The engine derives negative tags through their own proof conditions. Absence of +D or +d is not enough to emit -D or -d. The engine propagates evidence until no further tags can be established.

Conflict handling

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

With no priority, neither side is defeasibly provable: this is ambiguity blocking. Adding (prefer left right) lets p win. Under team defeat, different supporting rules can defeat different attackers; a single rule need not outrank every opponent. Defeaters can attack the complementary conclusion but cannot establish their own heads. When a premise is disproved, the engine discards the attacker. An unproved premise alone does not justify discarding it.

Cycles and inconsistency

(always strict-loop p p)
(normally defeasible-loop q q)

The strict self-loop leaves p undecided at both levels. The defeasible self-loop has -D q, but neither +d q nor -d q. A rule depending on such an undecided premise can continue to block an opponent.

If both p and (not p) are facts, both receive +D and +d. This strict inconsistency does not establish unrelated literals. See Conclusions for how to read the tags.

Grounding and aggregation

Grounding instantiates variables before ordinary reasoning. Grounding can grow combinatorially; its budgets constrain large theories. Aggregate programs infer strata, complete earlier reasoning, and lower aggregate results with snapshot premises before continuing. The engine accepts ordinary cycles but rejects cycles through an aggregate dependency. See Aggregation.

Theoretical complexity and grounding

For propositional theories, defeasible inference runs in linear time relative to theory size (Maher, 2001). With first-order variables, grounding instantiates rules against known facts before reasoning begins. As with Datalog, grounding can be exponential in rule body size. Reasoning over the ground theory remains polynomial. This tractability makes defeasible logic practical where other non-monotonic formalisms are intractable.

Measuring performance

Indexes, worklists, and bitsets reduce repeated lookup and propagation work. End-to-end cost also includes grounding, conflict checks, and, for aggregates, repeated prefix reasoning. The make bench and make bench-aggregation targets measure representative theories. A propositional complexity bound does not bound the whole pipeline.

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

Grounding Stages

Ground Facts

The grounder extracts all predicate instances from facts:

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

Rule Body Matching

For each rule, the grounder finds all substitutions that satisfy the body:

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

Substitutions:

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

Ground Rule Generation

The grounder applies 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))

Forward Chaining

Standard algorithms reason over the ground theory.

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

The wildcard _ matches any value:

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

This matches any parent relationship.

Variable Scope

Each rule has its own variable scope:

; ?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 appear in the body of a safe rule (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 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: This is strong negation, not negation-as-failure. The rule needs explicit support for (not (penguin ?x)); merely omitting a penguin fact does not make Eddie fly. The fact (given (not (penguin eddie))) supplies that premise. Stratification handles aggregate dependencies. It does not turn ordinary negation into a test for missing evidence.

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:

Small rule bodies and specific predicates reduce matching. Explicit superiority resolves grounded conflicts in favor of one side.

Arithmetic in Grounded Rules

After substituting variables, the grounder evaluates arithmetic expressions.

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. The grounder matches (item widget 25) and (tax-rate 0.1) → {?name→widget, ?price→25, ?rate→0.1}
2. The grounder evaluates (+ 25 (* 25 0.1)) → 27.5
3. The grounder binds ?total → 27.5
4. The grounder produces (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

The grounder evaluates body literals left-to-right. Arithmetic expressions need existing variable bindings:

; 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, each ground instance needs a separate rule:

(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

SPL accepts arithmetic constraints and expression arguments in rule bodies. It rejects arithmetic in facts, rule heads, and standalone statements. Numeric values and variables bound by body expressions remain valid head arguments.

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. Scientific notation selects IEEE 754 semantics and supports very large or small magnitudes.

Promotion Rules

When an operation mixes types, it promotes values 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. This affects calculations that need exact precision.

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))

A new binding assigns an unbound variable (one without a previous assignment 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

The grounder evaluates body elements left to right. Arithmetic expressions need variables bound by a preceding literal or bind:

; 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 grounder silently discards the substitution. The rule does not fire for that ground instance.

Arithmetic in Predicate Arguments

Arithmetic expressions can appear as predicate arguments in the body, but SPL rejects them in head arguments. This head-expression example is invalid:

; INVALID — arithmetic expression in a head argument
(normally r1
  (and (base ?x ?b) (offset ?x ?o))
  (result ?x (+ ?b ?o)))

A body bind computes the result for a head variable:

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

The grounder evaluates (+ ?b ?o) in the body. The bound ?total becomes a concrete term in the head literal.

Restrictions

Spindle enforces several restrictions on where arithmetic can appear. The parser checks each restriction and produces an error message.

No Arithmetic in Heads or Facts (REQ-009)

Arithmetic constraints (bind, comparisons) filter and compute in rule bodies. They cannot appear as conclusions. SPL also rejects expression arguments in heads and facts, as the preceding example illustrates.

; 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)

The not wrapper rejects arithmetic constraints. 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.

The complementary comparison expresses the opposite condition:

; 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 an arithmetic expression contains a temporal variable, the grounder silently discards the substitution. 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 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 grounder discards the substitution. The rule does not fire for that ground instance. The grounder reports no error to the user. It silently skips the rule 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.

Rounding, value bindings, and aggregates

The builtin prelude includes (round value decimal-places) with half-to-even rounding, (floor value), and (ceil value). Host applications can register additional pure functions. bind can carry integer or symbol results from these functions; builtin numeric guards still require numeric operands.

The agg form and explicit fold expressions in bind compute reductions across predicates. The aggregate bridge currently uses checked integer arithmetic, even though ordinary arithmetic supports decimals and floats. See Aggregation and Extension Functions.

Aggregation and extension functions

SPL uses a direct output-binding aggregate premise, following Skein: (agg ?total sum ?amount (payment ?id ?amount)). A named aggregator defines its combining operation and empty-input behavior. Ordinary calculations still use bind. Both use the extension registry introduced by PRs #26 and #27.

(given (person alice))
(given (person bob))
(given (payment alice 1 10))
(given (payment alice 2 10))
(normally total
  (and (person ?person)
       (agg ?total sum ?cost (payment ?person ?id ?cost)))
  (total-payment ?person ?total))

Commands for the complete example:

spindle reason examples/aggregation.spl --json
spindle query '(total-payment alice 20)' examples/aggregation.spl

Syntax and scope

(agg ?total sum ?amount (payment ?person ?id ?amount))
(agg ?number count ?id (payment ?person ?id ?amount))
(agg ?smallest min-of ?amount (payment ?person ?id ?amount))
(agg ?largest max-of ?amount (payment ?person ?id ?amount))

The result and contribution are variables. The contribution variable occurs in the row pattern. The current form accepts one row pattern. Helper relations express joins or filters. Aggregation is only valid as a rule premise, not as a fact, head, or negated premise.

The explicit fold syntax remains supported:

(bind ?result (fold reducer extraction :from pattern empty-policy))
empty-policy = :initial expression | :require-nonempty

The syntax requires exactly one :from and one empty-input policy. Their order is flexible. Supported reducers are +/sum, min, and max. Counting uses 1 as the extraction. The seed contributes once, including on empty input; it need not be an identity. :require-nonempty makes the condition unsatisfied on empty input. A fold appears directly in bind. Further calculations use another binding or rule. Nested folds require separate rules/strata.

Variables occurring in ordinary premises, rule heads, other bindings/comparisons, fold result bindings, or seed expressions belong to the outer scope. Variables confined to a fold's row pattern are local to each matching row. Extraction variables absent from its pattern are also outer variables. A variable shared only between two fold patterns is local to each fold, not an implicit join.

In the example, ?person selects a group; ?id and ?cost are row-local. Distinct whole rows contribute separately even when their extracted values are equal. Multiple proofs of an identical row do not multiply its contribution.

agg and bind introduce their result variable. For an already bound variable, the computed value matches the existing value. Earlier ordinary premises bind grouping variables. Row-local variables stay inside the aggregate. Head variables and expression inputs need a binding source. Unsafe variables are preparation errors.

Inputs can be derived predicates. For example:

(given (purchase alice first 30))
(given (purchase alice second 45))
(normally eligible
  (purchase ?person ?id ?cost)
  (payment ?person ?id ?cost))
(normally total
  (agg ?total sum ?cost (payment ?person ?id ?cost))
  (all-payments ?total))

This derives (all-payments 75). No fact or declaration enumerates 75.

Execution and evidence

SPL -> value AST -> source schemas -> inferred strata
                                         |
                    full earlier rule prefix + priorities
                                         |
                                  ordinary reasoner
                                         |
                                  completed +D/+d rows
                                         |
                            match -> extract -> reduce
                                         |
                     lowered rules with snapshot premises
                                         |
                              normal reasoning / CLI

A stratum is a group of predicates at one dependency level. Ordinary dependencies have non-strict stratum ordering; fold dependencies require a strictly earlier stratum. Cycles through a fold are rejected. Strong negation shares its predicate's stratum. Earlier attackers and priorities are retained.

A strict aggregate rule retains its kind but receives a fresh defeasible snapshot premise. This prevents automatic +D from aggregate evidence. Independent strict proofs can still establish the head definitely. Internal snapshot predicates are hidden from conclusions; lowered rules retain source labels as template labels for diagnostics. The prepared theory contains those internal premises for audit.

Functions and reducers

FunctionRegistry::with_prelude() supplies arithmetic and rounding functions. prepare() injects this prelude and merges PrepareOptions::function_registry. Custom registry entries override same-named expression functions. Registries are cloneable and preserve their functions through query options.

A host implements ExtensionFunction with a signature and eval(&[Term]) -> Result<Term, EvalError>, then registers it with registry.register(Box::new(function)). Functions receive evaluated values, including symbols. The host contract requires pure, deterministic functions. They have no theory-query argument. The CLI ships the builtin prelude; this is an embedding API, not a runtime plugin loader.

(bind ?day (day-of-week ?date))
(bind ?total
  (fold + (adjust-cost ?cost)
    :from (payment ?person ?cost)
    :initial 0))

These examples depend on host registrations for day-of-week and adjust-cost. Unknown functions and invalid arities are validation errors. Ordinary grounding retains its existing behavior of discarding a substitution when a function fails; aggregate snapshot evaluation reports expression failures as errors.

FunctionRegistry also has a separate aggregator namespace. register_aggregator(name, definition) registers a named AggregatorDefinition. Its fields are the binary reducer name, an integer identity or None, and whether to count rows rather than use their selected values. The identity is both the starting accumulator and the empty result; None requires a nonempty input. Host registries can override aggregator definitions without changing ordinary same-named functions.

The reducer can be the engine-controlled +/sum, min or max, or a registered binary extension function returning an integer. The host contract requires custom reducers to be pure, associative, and commutative over accepted inputs. Registration does not prove those laws. Builtin reducer names retain their kernel meanings even if an ordinary arithmetic function with that name is overridden. There is no foldl/foldr because relations supply no user-defined iteration order.

Limits and verification

No aggregate-domain is needed. The old declaration is accepted for source compatibility but does not restrict SPL input rows or computed outputs. The typed finite-domain reference API retains its explicit domain contract.

Grounding joins potential predicate instances; completed proofs determine the aggregate rows. Ordinary cyclic support and attackers are retained even when undecided. Cyclic predicates are conservatively instantiated over source and computed constants, and completed strata are replayed when new constants appear. This can be exponential. The configured max_instances budget bounds grounding work, including repeated passes. Exhaustion (including unbounded value-generating recursion) is an error, never a partial answer. Grounding cannot be disabled.

The aggregate bridge currently rejects decimal/float values, modal or temporal constructs, trust-weighted snapshots, schematic predicates, wildcards, and arithmetic inside ordinary predicate arguments (bind provides a separate expression binding). Expressions and fold results use checked i64 arithmetic; overflow is an error. Extensions in aggregate programs return supported integer/symbol values. General arithmetic outside aggregation still supports the existing numeric types.

The Lean model uses exact integers. Checked overflow can depend on intermediate reduction order, so the implementation's deterministic row traversal is not a machine-arithmetic refinement proof. Custom extension implementations and general symbol bindings are also outside the current proof fragment.

Builtin named aggregates lower to the existing typed fold model. Differential checks compare all tagged conclusions with the independent Lean evaluator, including grouping, empty inputs, duplicate contributions, conflicts and traditional DL(∂) cycle behavior. Any disagreement fails the differential check. Custom reducer functions remain outside the Lean proof fragment. Parsing and extension registration are tested integrations, not themselves verified Lean code. See the proof guide.

Spindle/Aggregation/Binding.lean proves the domain-free aggregate operation against independent unordered predicate semantics. It also proves agreement with the finite reference model when its domain contains the result. The Rust predicate grounder itself is differentially tested, not formally verified.

Related pages

• Architecture explains completed prefixes and snapshot evidence.
• Benchmarking aggregation gives the measurement workflow.
• Benchmark measurements records coverage and the initial local baseline.

Temporal Reasoning

Spindle supports bounded temporal literals, whole-interval variables, Allen constraints, and “as-of” filtering when requested.

Time points and intervals

Time points are milliseconds since the Unix epoch (UTC). Accepted bounds include integers, (moment "2024-06-15T14:30:00Z"), or -inf / inf. Multi-argument calendar forms such as (moment 2024 6 15) are unsupported.

(given (during (employed alice acme) 100 200))
(given (during (employed alice beta) 201 inf))

The explicit endpoint form is (during literal start end). Concrete bounds are inclusive for active-at filtering.

Interval variables and constraints

The premise (during literal ?T) binds a whole interval:

(given (during (p a) 1 10))
(given (during (q b) 20 30))
(normally sequence
  (and (during (p ?x) ?T)
       (during (q ?y) ?S)
       (before ?T ?S))
  (ordered ?x ?y))

This derives (ordered a b). SPL supports all 13 Allen constraints:

• before, after, meets, met-by
• overlaps, overlapped-by, starts, started-by
• within, contains, finishes, finished-by, equals within names Allen's During relation, avoiding collision with SPL's during literal wrapper. Constraints filter interval bindings during grounding.

Intervals can also be carried into rule heads:

(given (during (p a) 1 10))
(normally copy (during (p ?x) ?T) (during (q ?x) ?T))

This derives q(a) with bounds [1,10]. Endpoint variables in (during literal ?start ?end) are also supported. Temporal variables cannot be used as numeric arithmetic operands. Default preparation validation rejects unresolved temporal expressions.

active-at, past-at, and future-at are also available as body constraints, for example (active-at ?T 150) after binding ?T.

Exact atoms and family matching

Temporal bounds are part of indexed atom identity: p@[1,10], p@[20,30], and atemporal p are distinct. An atemporal body premise can nevertheless consume positive evidence from a temporal member of its family:

(given (during p 1 10))
(always consume p q)

This establishes q without creating a positive atemporal p conclusion. The current engine uses family-aware body matching and projection tokens; it does not insert synthetic TemporalBridge rules or reserve __bridge:: labels for such a stage. Repeated members satisfying one body slot count once.

Query matching

Atemporal queries use family matching. Bounded queries require identical windows: a goal for p@[1,10] does not match p@[20,30], atemporal p, or even the containing window p@[0,20]. The same distinction applies to requires, what_if, and abduce; why_not diagnoses the grounded goal.

The CLI accepts temporal literals in SPL form:

spindle query '(during p 1 10)' theory.spl --json

Explicit family-wide matching in Rust uses query_with_match_mode(&theory, &goal, QueryMatchMode::Family).

As-of filtering

spindle reason theory.spl --at '2026-09-17T12:00:00Z'

Preparation keeps rules whose own interval, head literals, and logical body literals are active at the reference point. Arithmetic premises have no temporal window. Filtering runs around grounding to check bound temporal expressions. Without --at, preparation does not filter temporal evidence to “now”.

Temporal reasoning and aggregation are currently separate supported paths: the aggregate bridge rejects temporal constructs and temporal preparation options.

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 can 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. Modal literals undergo ordinary defeasible reasoning, including conflict resolution, superiority, and defeat.

CLI support: SPL theories accept (must ...), (may ...), and (forbidden ...) wrappers through the CLI. The Rust API and WASM bindings also provide modal reasoning.

The Three Standard Operators

Spindle provides three built-in deontic operators:

Obligation (must)

An obligation states a normative duty. 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

Toggling the negation flag produces the complement of a modal operator. 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. Payment carries no obligation, but remains a choice.
• 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. Spindle treats literals with the same name but different modes as 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

Regulatory compliance rules express obligations subject to 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

Access control rules express 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

Chains of reasoning track obligations:

; 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

A single theory combines obligations, permissions, and prohibitions:

; 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. CLI syntax: Modal operators use SPL wrappers in theory files. The CLI reasons over these literals without a separate modal flag.
2. No inter-modal axioms: Spindle does not enforce relationships between operators (e.g., it does not automatically derive [P]a from [O]a). Explicit rules encode these relationships.
3. Custom modes are uninterpreted: Custom modes created with Mode::new(name) have no built-in semantics. The theory’s rules entirely determine their meaning.
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.

Modal Rule Patterns

1. Explicit modal relationships

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

2. Superiority resolves 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 rules

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

4. Metadata records 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 API and SPL Directives

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 (each can be omitted):

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]. Multiplying the source’s base trust by this value gives its decayed trust. 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.

Automatic diminishment in the pipeline

After computing weakest-link credibility, the trust pass detects defeaters whose heads complement a surviving +d conclusion and whose premises are positively provable. These applicable but overruled challenges reduce its degree in rule order: degree *= 1 - defeater_degree. The defeater degree is the weakest link of its own derivation. Unfired defeaters do not diminish, and +D conclusions are exempt. The trust pass evaluates thresholds after this fold, and diminished_by records the contributing challenges.

For example, degree 0.9 challenged by degrees 0.3 and 0.4 becomes 0.9 * 0.7 * 0.6 = 0.378. This affects credibility; it does not retract the positive logical conclusion. The aggregate snapshot bridge currently excludes trust-weighted inputs.

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

Different trust policies can evaluate the same derivation, 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 supports compliance requirements for traceable, explainable decisions.

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.

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. A claims block supplies the source attribution for trust-weighted reasoning. A fully trusted source such as system:policy represents axiomatic structural or policy rules.

CLI invocation with trust output:

spindle reason --trust review.spl

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: Each policy fixes its trust values. Dynamic trust based on track record is not built in. Decay models provide 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: Spindle stores the :sig metadata field without checking it against 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: Callers compute assertion ages externally for decay models. The pipeline does not automatically track assertion timestamps for decay purposes.

Query Operators

query checks a literal, why_not identifies blockers, and what_if evaluates hypothetical facts. requires_with_options verifies proposed facts by rerunning the reasoner. abduce supplies raw candidates.

Rust example

use spindle_core::{Literal, Theory};
use spindle_core::query::{
    query, why_not, what_if, HypotheticalClaim,
    requires_with_options, RequiresOptions,
};

fn main() -> spindle_core::error::Result<()> {
    let mut theory = Theory::new();
    theory.add_defeasible_rule(&["bird"], "flies");
    let goal = Literal::simple("flies");

    let current = query(&theory, &goal)?;
    println!("Status: {}", current.status);
    let why = why_not(&theory, &goal)?;
    println!("Blockers: {:?}", why.blocked_by);

    let hypothetical = what_if(
        &theory,
        vec![HypotheticalClaim::new(Literal::simple("bird"))],
        &goal,
    )?;
    assert!(hypothetical.is_provable());

    let required = requires_with_options(&theory, &goal, RequiresOptions {
        max_solutions: 3,
        max_raw_candidates: 1000,
    })?;
    for solution in &required.solutions {
        println!("Assume: {:?}", solution.facts);
    }
    println!("Search: {:?}", required.search_status);
    Ok(())
}

query returns Provable, Refuted (the complement is provable), or Unknown. These statuses summarize positive evidence; Unknown does not mean the engine has proved a negative tag. See Conclusions.

Hypothetical reasoning

what_if clones the theory, adds the supplied facts, and compares the new result with the baseline. new_conclusions contains newly provable literals without repeating a literal proved at both +D and +d. Distinct temporal windows and typed terms are preserved. The original theory is unchanged.

Explaining missing conclusions

why_not examines grounded rules, so a query such as (flies opus) can find a rule written with (flies ?x) in its head. Its blocked_by entries identify missing premises, defeat, contradiction, or undetermined conditions. Superiority uses source template labels. The explanation system also resolves grounded labels to templates when constructing proof trees.

Abduction and verified requirements

abduce(&theory, &goal, max_solutions)? returns candidate assumptions. A candidate can fail under full conflict resolution. requires_with_options returns verified solutions. Verification injects each candidate fact-set and reruns reasoning, retaining only candidates that establish the goal.

Each AbductionSolution contains:

• facts: Vec<Literal>: deterministic, deduplicated assumptions preserving typed terms and distinct temporal windows.
• rules_used: the rules associated with that solution's fact-set.
• confidence: currently initialized to 1.0; this value is not a calibrated probability or proof that the candidate establishes the goal.

RequiresResult reports already_provable, solutions, search_status, and verification counters (raw_examined, accepted, rejected). BoundedComplete means the available search finished or the requested solution count was reached; it does not promise exhaustive enumeration. BudgetExhausted means further raw candidates existed beyond the budget. Duplicate fact-sets consume one budget slot. An unproved goal with no accepted solutions is a valid result.

Temporal matching

Bounded goals use exact temporal windows. A query for p@[1,10] does not match p@[20,30], atemporal p, or even a containing window p@[0,20]. Atemporal goals match any member of the same literal family. This applies to query, requires, what_if, and abduce.

query_with_match_mode(&theory, &goal, QueryMatchMode::Family) in spindle_core::query explicitly selects family-wide matching. See Temporal Reasoning.

CLI and WebAssembly

spindle query flies theory.spl --json
spindle why-not flies theory.spl --json
spindle requires flies theory.spl --max 3 --json

requires --json emits spindle.requires.v2; an unsatisfied goal can have an empty solution list. The CLI has no standalone what-if or abduce command. The WASM Spindle object exposes query, whatIf, whyNot, and raw abduce; it does not expose the verified requires API.

const hypothetical = spindle.whatIf(["bird"], "flies");
const blockers = spindle.whyNot("flies");
const candidates = spindle.abduce("flies", 3);

See the CLI reference and WebAssembly guide for output formats.

Explanation API and Output Formats

Spindle’s explanation system exposes the derivation path of defeasible reasoning conclusions. It records rejected alternatives and resolved conflicts alongside proof trees.

Explanation Coverage

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?

These records support decision justification in legal reasoning, medical diagnosis, and access control.

Proof Trees

Structure

An explanation contains a proof tree. This recursive structure traces a literal’s derivation back to its supporting facts and rules.

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 the reasoner considered but rejected
  • conflicts_resolved -- conflict resolutions that occurred at this node

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

  • rule_label -- the applied rule
  • 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. Each node’s proof_step identifies the applied rule. Its body_proofs contain the sub-trees for each premise.

For example, a theory contains the fact penguin, strict rule (always s1 penguin bird), and defeasible rule (normally r1 bird flies). Its proof tree for flies has this structure:

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

Some candidate rules for a literal or its complement face blockers. 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 is unsatisfied
• blocking_rule -- the label of the rule that caused the blocking (if applicable)
• explanation -- a human-readable description

Conflict Resolutions

Rules deriving contradictory conclusions create a conflict. A ConflictResolution records:

• winning_rule -- the rule that prevailed
• losing_rule -- the defeated rule
• 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

The output includes description and source annotations when proof steps contain them.

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

The JSON-LD serializer maps rule metadata provenance annotations 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. Edge labels identify rules.

Annotations and Metadata

The Annotations Type

Annotations is a metadata container with two fields:

• id -- a URI identifier, when present (@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);
}

All output formats preserve annotations. Natural-language output prints description and source inline. JSON-LD maps description, source, and confidence to rdfs:comment, prov:wasAttributedTo, and spindle:confidence, respectively.

CLI Usage

The explain Command

explain returns 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

why-not reports why a literal is not provable:

spindle why-not flies theory.spl

The output lists candidate derivation rules and their blockers. Blockers include missing premises, defeat by a stronger rule, and contradiction 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.

The conclusion debugging guide combines these commands to diagnose unexpected results.

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. New information can override these conclusions.
• 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. Each edge label identifies the applied rule.

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. The why-not CLI command and query module provide negative explanations.
2. Grounded theories: Explanations work on grounded theories. Explanation generation requires bound variables.
3. No incremental updates: A full reasoning pass produces explanations. Changes to the theory require re-running the reasoner.
4. Annotation attachment: Programmatic explanation construction requires manual annotation attachment to proof steps. The explain function does not yet automatically populate annotations from rule metadata.

Process Mining API

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, actor when present, and annotations
• Case -- a complete process trace identified by a unique ID, containing events sorted by timestamp
• EventLog -- the collection of cases with metadata when present

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

Case::new automatically sorts events 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 adjacent activity pairs occur without their reverse? (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. Computes the footprint from the event log's directly-follows pairs
2. Identifies start/end activities (first/last in each trace)
3. Finds maximal pairs (A, B) where all activities in A causally lead to all activities in B, and both sets are internally unrelated
4. Builds the net: creates 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: no trace contains both activities. A choice conflict does not already capture the relationship. 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

The extractor excludes rules below the minimum support or confidence thresholds:

#![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. Builds the footprint matrix from the event log
2. Runs the Alpha miner to discover the Petri net
3. Detects conflicts from the net structure and trace analysis
4. Extracts SPL rules from causal pairs, filtered by support and confidence
5. Packages everything into a MiningResult with metadata

Use Cases

Workflow Analysis

This API example discovers 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

This API example compares mined rules against expected patterns to identify process deviations:

#![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 for an observed review-to-approve relation without its reverse
if fp.is_causal("review", "approve") {
    println!("Observed: review directly precedes approve, with no reverse pair");
} else {
    println!("No unidirectional review-to-approve relation");
}

// Check for unauthorized shortcuts
if fp.is_causal("submit", "approve") {
    println!("Warning: direct submit-to-approve path detected");
}
}

is_causal checks observed adjacent pairs across the log. It does not establish that review precedes every approval. This log contains a skipped review despite its causal review -> approve relation. Checking compliance for every approval requires inspecting each trace.

Process Discovery

Mining produces rule sets for Spindle’s reasoning engine:

#![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: Case::new sorts events lexicographically by timestamp string. ISO-8601 formatting ensures correct ordering.
4. Rust API only: Process mining is not yet available through the CLI or WebAssembly bindings.
5. No incremental mining: The API requires the entire log upfront. It does not support streaming or incremental updates.

How to Tune Reasoning Performance

Measure complete preparation and reasoning on representative theories. Grounding, conflict resolution, and aggregate stages can dominate different workloads.

Start with a baseline

cargo build --release -p spindle-cli
./target/release/spindle stats theory.spl
time ./target/release/spindle reason theory.spl > /dev/null
make bench
make bench-scaling

When comparing revisions, use the same toolchain, machine, and fixture. A short local benchmark is not a portable performance guarantee.

Control grounding

Independent variables multiply candidate combinations. For example, with 100 nodes this rule can produce 10,000 pairs:

(normally pairs (and (node ?x) (node ?y)) (pair ?x ?y))

When selective relations and guards express the intended domain, use them. Bind expression inputs before evaluating them. Configure grounding limits via PrepareOptions in Rust. Splitting a rule or adding priorities can change its defeasible semantics. After a rewrite, check conclusions as well as runtime.

Aggregate workloads

make bench-aggregation
cargo bench -p spindle-core --bench aggregation -- --test
cargo bench -p spindle-core --bench aggregation -- --save-baseline before
# After changing the implementation:
cargo bench -p spindle-core --bench aggregation -- --baseline before

The aggregate suite measures preparation and full reasoning separately. It covers reducer choice, row count, grouping, unrelated facts, and chained stages. Fixture creation and expected-output checks happen outside timed loops; timed loops include allocation and destruction. See the initial baseline and methodology.

Repeated stages can require grounding and reasoning earlier prefixes again. Grounding can instantiate cyclic predicates over source and computed constants. These combinations can grow exponentially. max_instances bounds aggregate grounding work across repeated passes; exhaustion is an error, not a partial answer.

Memory and integration

The engine uses interned names, compact indexes, bitsets, and small-vector rule storage. These reduce overhead but do not eliminate the cost of a large grounded theory. reason() returns a collected result; there is no public reason_iter() streaming API. Unless your application needs cloned theories or full result histories, avoid retaining them.

For heap profiling, use make bench-memory. Criterion output lives under target/criterion/. In browser applications, run expensive synchronous WASM reasoning in a worker to keep the UI responsive.

How to benchmark aggregation

Run these commands from the repository root on an otherwise idle machine.

Check fixtures

Before collecting timings, check every fixture's expected results:

cargo bench -p spindle-core --bench aggregation -- --test

The command checks all fixtures without collecting timings.

Measure the current revision

Run the dedicated Criterion suite:

make bench-aggregation

Criterion writes reports under target/criterion/. The benchmark reference describes coverage, timing boundaries, defaults, and the initial local baseline.

Compare a change

Save a baseline before changing the code:

cargo bench -p spindle-core --bench aggregation -- --save-baseline before

After changing the code, compare against that baseline:

cargo bench -p spindle-core --bench aggregation -- --baseline before

For more precise comparisons, increase the sampling budget. This command measures one family with 30 samples and a 5-second measurement target:

cargo bench -p spindle-core --bench aggregation -- aggregation/groups --sample-size 30 --measurement-time 5

How to inspect a theory

Start with penguin.spl from Getting Started.

1. Show only positive conclusions:

   spindle reason --positive penguin.spl
   

2. Request structured JSON output:

   spindle reason --json penguin.spl
   

3. Check syntax without reasoning:

   spindle validate penguin.spl
   

4. Inspect theory statistics:

   spindle stats penguin.spl
   

The CLI reference describes each command and its output.

How to Debug Unexpected Conclusions

This guide diagnoses missing or unexpected conclusions in an existing SPL theory.

Run these commands against theory.spl:

# 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'

The explanation API reference describes both commands and their output formats.

How to run verification checks

Use the Lean toolchain specified under lean/. Run these checks from the repository root:

make check
make test
scripts/check-lean-verification.sh

The Lean gate builds the oracle executables. After the gate succeeds, run the external-oracle tests explicitly. For example:

cargo test -p spindle-core --test lean_aggregation_oracle_difftest -- --ignored --nocapture
cargo test -p spindle-core --test lean_arith_oracle_difftest -- --ignored

Each test compares Rust results with the corresponding executable Lean model. A passing run reports no mismatches for the tested inputs.

The repository guides record theorem statements, hypotheses, and the full suite list:

• Lean guide
• Proof catalogue
• Aggregate proof guide

Verification explains the scope of these checks.

How to Troubleshoot Spindle

Use this guide to diagnose parse errors, unexpected conclusions, grounding failures, and performance problems.

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 whether the rule exists:

   spindle stats theory.spl
   

2. Check whether the reasoner proves the body:

   ; 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 unexpectedly has status +d.

Debugging steps:

1. Find which rule proves it:

   grep "literal" theory.spl
   

2. Check whether a defeater is missing:

   ; Add a defeater to block
   (except d1 exception (not 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 cannot overturn a definite proof. Strict rules with only defeasible premises still participate in defeasible conflict resolution.
   • Check whether strict-rule premises have definite proofs before treating the resulting conclusion as immune to defeasible attacks.

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: Contradictory facts or strict derivations can prove both sides definitely. Unresolved defeasible conflicts alone block both sides.

Fix:

1. Check whether both literals also have +D proofs.
2. Inspect their facts and strict derivations with spindle explain.
3. When the domain does not justify both sides, correct contradictory premises or strict rules.
4. When the domain establishes a preference between competing defeasible derivations, add a superiority declaration.
5. Re-run reasoning and check the resulting conclusions.

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

Check the theory 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://git.anuna.io/anuna-research/spindle-rust/issues

Changelog

All notable changes to this project will be documented in this file.

The format is based on Keep a Changelog, and this project follows pre-1.0 Semantic Versioning (0.y.z).

[Unreleased]

Added

• Predicate identity: public PredicateKey and predicate_key() accessors on Literal and BodyLogicLiteral expose functor plus arity, with diagnostic functor/arity formatting. Argument values, negation, modality, and temporal bounds are excluded; arithmetic body argument positions are counted. Arity uses usize so construction and extraction are infallible (#33).
• Aggregation in SPL: named agg premises (sum, count, min-of, max-of) and explicit (bind ?result (fold ...)) expressions.
  • Aggregate over completed, positively proved predicates, including derived rows, with grouping and inferred strata. Cycles through aggregates are rejected.
  • Distinct rows contribute separately even when their selected values match; multiple proofs of the same row contribute once.
  • Results bind directly without an enumerated output domain. sum and count return zero on empty input; min-of and max-of fail the premise.
  • Snapshot premises preserve defeasible evidence, source labels, and priorities; internal snapshot predicates are hidden from conclusions.
  • Checked integer arithmetic and bounded grounding report overflow or exhausted budgets as errors. The aggregate bridge currently excludes decimal/float, modal, temporal, and trust-weighted inputs.
  • Syntax, embedding guidance, and a runnable example in Aggregation and extension functions.
• Extension functions: ExtensionFunction, FunctionRegistry, and PrepareOptions::function_registry support host-registered pure functions, integer/symbol value bindings, and custom named aggregators. The builtin prelude includes arithmetic, round (half-to-even), floor, and ceil.
• Trust diminishment: applicable but overruled defeaters reduce defeasible conclusion credibility multiplicatively using their weakest-link degrees. Thresholds use the diminished degree, WeightedConclusion::diminished_by records the challenges, and definite conclusions are exempt.
• Lean verification and differential testing: models and proofs for grounding, arithmetic, temporal intervals, query operators, and trust. Aggregate coverage includes dependency/stratum inference, source semantics, lowering, and completed-prefix equivalence for all four proof tags. Rust/Lean oracle suites compare supported fragments; these do not establish whole-language Rust conformance or verify custom extension implementations.
• Verification gate: builds Lean libraries and oracle executables, rejects admitted proofs and local axioms, checks for vacuous proofs, and audits theorem dependencies.
• Aggregate benchmarks: make bench-aggregation measures preparation and full reasoning across row counts, groups, unrelated facts, and chained stages, with a documented local baseline.
• Predicate model and vocabulary (SPEC-024): a structural predicate identity and derived tooling projections, all additive and non-semantic (reasoning is unchanged).
  • PredicateSymbol (functor + arity) with a HasPredicateSymbol projection for Literal and BodyLogicLiteral (body arity retains arithmetic args).
  • Primitive sorts, checked PredicateSignature, positional ArgumentProfile, and non-semantic Shape validation.
  • GroundLiteral / LiteralPattern phase wrappers and Literal::classify.
  • TheorySignature::derive and Vocabulary::derive (deterministic symbol sets, declaration conflict handling, descriptions, provenance, summary counts).
  • SPL: first-class (predicate name ((arg sort) ...)) declarations and structured (meta (predicate functor arity) ...) metadata targets, stored in Theory with source provenance. Undeclared predicates remain valid. Declarations also accept inline meta properties ((predicate name (...) (description "..."))) as sugar for the separate metadata target.
  • Predicate-indicator recognizer (functor/arity) in spindle-parser.
  • Additive spindle.vocabulary/1 JSON DTOs in spindle-contract.
  • Theory::metadata() retains its label-keyed API; predicate metadata is available separately through Theory::predicate_metadata().
• Arithmetic module (SPEC-017): full arithmetic expression support in SPL.
  • Term enum with Symbol, Integer, Decimal, Float variants.
  • FiniteFloat wrapper: rejects NaN/Inf, normalizes -0.0, safe for Eq/Hash.
  • ArithExpr AST with NaryOp (+, -, *, /, min, max), BinOp (div, rem, **), and UnaryOp (abs).
  • ArithConstraint: bind variable binding and comparison guards (=, !=, <, >, <=, >=).
  • BodyLiteral, BodyLogicLiteral, and BodyArg types for mixed logic/arithmetic rule bodies.
  • Cross-type numeric matching in grounding (REQ-010/CON-005): Integer(2) matches Decimal(2.0) matches Float(2.0).
  • Type promotion chain: Integer -> Decimal -> Float.
  • rust_decimal dependency for fixed-precision decimal arithmetic.
• SPL parser extensions:
  • Arithmetic expression parser for +, -, *, /, div, rem, **, abs, min, max.
  • (bind ?var expr) and comparison guard parsing in rule bodies.
  • Arithmetic expressions in body literal argument positions.
  • Numeric literal detection in predicate arguments.
  • Lexer extended to accept operator characters in atoms.
  • Parse-time guard checks: reserved keyword rejection (REQ-008), arithmetic in head rejection (REQ-009), negated arithmetic rejection (REQ-011).
• v2 JSON output (REQ-012/CON-006):
  • --v2 flag on CLI, reasonV2 method on WASM.
  • Typed Term arguments in JSON schema (spindle.reason.v2).
• Test suites:
  • Unit tests for Term, ArithExpr, and type promotion (TEST-001, TEST-002, TEST-005).
  • Arithmetic parsing and guard enforcement integration tests.
  • Grounding integration tests with arithmetic pipeline.
  • Worked examples, NFR, and proptest suites for arithmetic.
  • v2 JSON typed argument serialization tests (TEST-012).

Changed

• Reasoning semantics: Rust and the standard Lean oracles now follow traditional ambiguity-blocking DL(∂) with four constructive proof tags. Unsupported cycles remain undecided instead of receiving automatic negative conclusions; undecided attackers are not discarded. Contradictory definite facts retain both positive definite and defeasible tags without proving unrelated literals.
• Breaking: arithmetic expressions use registry-dispatched ArithExpr::Call nodes, replacing the operator-specific AST variants, with Value and Fold variants for general bindings and aggregation.
• Projection snapshots and abduction output use deterministic, injective semantic keys, preserving distinct temporal windows and typed terms.
• CI workflows restored for Forgejo compatibility.
• Documentation book uses a forge-neutral repository icon and canonical repository source links in place of edit links (#37, contributed by SamB).
• Refreshed the documentation book with aggregation and verification guides, current DL(∂) semantics, query and WASM APIs, trust diminishment, and aggregate performance guidance. The book includes this changelog directly.
• Breaking: bounded temporal queries now match exact windows (SPEC-020 REQ-006). query, requires, what_if, and abduce goals carrying a bounded temporal window (e.g. p@[1,10]) only match conclusions with the identical window. Previously the window was ignored, so a bounded query matched any conclusion in the same family — including atemporal p or p@[20,30]. A query window strictly contained in a proven window (query p@[1,10] vs proven p@[0,20]) now also returns unknown. This applies to CLI queries (spindle query/requires) and WASM query methods. The JSON envelope schemas (spindle.query.v1, spindle.requires.v2) are unchanged; only the reported status for bounded queries differs. Atemporal queries still match any family member. Call query_with_match_mode(theory, literal, QueryMatchMode::Family) to restore family-wide matching for a bounded literal.
• Breaking: AbductionSolution.facts changed from HashSet<Literal> to Vec<Literal>, deduplicated by injective canonical key so distinct temporal windows and typed terms are no longer collapsed.
• Breaking: AbductionSolution.rules_used now lists only the rules that produce that specific solution's fact-set, not every rule whose head matches the goal.
• Breaking: From<NumericValue> for Term replaced with TryFrom<NumericValue> for Term. Non-finite floats (NaN, Inf) now return an error instead of silently coercing to 0.0.
• Literal::predicate_ids migrated from Vec<SymbolId> to Vec<Term>.
• Substitution::terms migrated from SymbolId values to Term values.
• RuleBody migrated from SmallVec<[Literal; 4]> to SmallVec<[BodyLiteral; 4]>.
• Body literals evaluated in source order with threaded substitutions.
• Temporal variables rejected as arithmetic operands (REQ-006).

Fixed

• Documentation examples now use complementary defeater heads and defeasible defaults correctly. Temporal documentation describes current interval variables, Allen constraints, and family matching instead of the removed bridge stage.
• Explanation witnesses: explanations on original quantified theories now use actual grounded rule instances, preserving consistent variable bindings across the conclusion and every premise. Incomplete derivations return no proof tree instead of a partial justification (#37).
• why_not inspects grounded rules so variable-headed rules report actual blockers. Superiority checks use template labels, and defeated rules are no longer projected as supporting proofs.
• what_if deduplicates new conclusions proven at both positive tags while preserving distinct typed arguments and temporal windows.
• Predicate declarations and metadata survive grounding, wildcard rewriting, and temporal filtering. Vocabulary reports retain conflicting declarations and their provenance; deferred shape checks no longer count as mismatches.
• Vocabulary DTO validation rejects malformed functors and inconsistent diagnostics while accepting coherent v1 signatures that omit declaration origins. SPL rejects malformed metadata properties, and WASM output quotes structured predicate metadata targets correctly.
• Symbol-valued extension returns bind correctly, and float-to-integer boundary checks reject out-of-range values.
• Reasoning tracks repeated body occurrences per slot and discards attackers with disproved premises consistently.
• FiniteFloat serde deserialization now validates through FiniteFloat::new, preventing non-canonical values (-0.0) and non-finite values from bypassing type invariants.
• BinArithOp::Pow Display emits ** (matching the SPL parser) instead of pow.
• BodyLogicLiteral::to_spl() renders BodyArg::Arith directly instead of quoting through render_spl_atom, preserving arithmetic s-expression syntax on round-trip.
• Tilde-negated reserved keywords (~>, ~bind, etc.) rejected in list-form literals in both body and head parsers (REQ-008).
• Negative base with fractional exponent rejected in decimal_pow.
• Bind consistency enforced; constant arithmetic args grounded correctly; numeric parsing unified across paths.
• Temporal bounds preserved in body normalization.
• Non-finite floats rejected in bind evaluation.
• Arithmetic module memory leaks resolved; duplicate fact double-decrement fixed.

[0.2.0]

Added

• Verified requires core API:
  • requires_with_options(theory, goal, options)
  • RequiresOptions, RequiresResult, RequiresSearchStatus, RequiresVerificationStats
• New CLI contract schema: spindle.requires.v2.
• New core test suite: crates/spindle-core/tests/requires_verified_tests.rs.

Changed

• requires is now verified-by-default in core and CLI.
• requires --json emits spindle.requires.v2 only.
• spindle capabilities --json now advertises schemas.requires = spindle.requires.v2.
• Core requires() compatibility wrapper now 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.
• Added defensive collision handling for injected verification fact labels.

Migration

• Clients checking requires JSON need the spindle.requires.v2 schema instead of spindle.requires.v1.
• In v2, satisfied=false with solutions=[] is valid.

Rust Library API

This reference describes Spindle’s Rust library types, preparation pipeline, and reasoning APIs.

Installation

Git dependency declarations in Cargo.toml:

[dependencies]
spindle-core = { git = "https://git.anuna.io/anuna-research/spindle-rust", package = "spindle-core" }
spindle-parser = { git = "https://git.anuna.io/anuna-research/spindle-rust", package = "spindle-parser" }

Local path dependencies, for a consumer whose manifest sits beside crates/:

[dependencies]
spindle-core = { path = "crates/spindle-core" }
spindle-parser = { path = "crates/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 fixed-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). Term::to_numeric_value() performs the conversion:

#![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. PipelineBuilder assembles its composable stages.

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

PipelineBuilder supports custom pipelines assembled 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

All stages share a PipelineContext, which collects 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 configurable temporal filtering and grounding:

#![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

An indexed theory supports multiple queries after a single construction:

#![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(())
}

Predicate Vocabulary

SPEC-024 adds a structural predicate model on top of the reasoning AST. It is entirely additive and non-semantic: constructing signatures, vocabularies, or shapes never changes conclusions. The types live in spindle_core::vocabulary and are re-exported from the prelude.

Predicate Symbols

A PredicateSymbol is the pair (functor, arity) — the structural identity of a predicate, excluding arguments, polarity, mode, and temporal bounds. Any head literal or logical body literal projects to one:

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

let lit = Literal::new("assign-to", false, Mode::empty(), Default::default(),
    vec!["t1".into(), "alice".into()]);
let sym = lit.predicate_symbol().unwrap();   // via HasPredicateSymbol
assert_eq!(sym.arity(), 2);
assert_eq!(sym.indicator().to_string(), "assign-to/2");
}

p(a) and ~p(b) share p/1, but this identity is deliberately not a proof-state key. FamilyId, LitId, and ExactLitId remain authoritative for reasoning.

Declaring Predicates Programmatically

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

let mut theory = Theory::new();
let sig = PredicateSignature::try_new(
    PredicateSymbol::try_new("assign-to".into(), 2).unwrap(),
    vec![
        ArgumentDecl::new("task", PrimitiveSort::Symbol),
        ArgumentDecl::new("agent", PrimitiveSort::Symbol),
    ],
).unwrap();
theory.add_predicate_declaration(
    PredicateDeclaration::new(sig, DeclarationOrigin::Programmatic));

// Predicate-targeted metadata (distinct from rule-label metadata):
theory.add_meta_target(
    MetaTarget::Predicate(PredicateSymbol::try_new("assign-to".into(), 2).unwrap()),
    "description",
    MetaValue::String("Assign a task to an agent.".into()),
);
}

PredicateSignature::try_new enforces that the argument count equals the arity and that names are non-empty and unique.

Deriving the Theory Signature and Vocabulary

TheorySignature::derive returns every predicate symbol the theory uses or declares, plus each symbol's declaration state (Declared or Conflict). Vocabulary::derive builds the fuller catalogue and its diagnostics:

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

let report = Vocabulary::derive(&theory);
for entry in &report.vocabulary.entries {
    println!("{}", entry.symbol.indicator());
    if let Some(desc) = &entry.description {
        println!("  {desc}");
    }
    // entry.profile — observed argument kinds per position
    // entry.origins — rule occurrences, sorted by (label, head-before-body, index)
}

// Deterministic summary counts (OBS-001):
println!("{} symbols, {} occurrences, {} conflicts",
    report.summary.distinct_symbols,
    report.summary.observed_occurrences,
    report.summary.declaration_conflicts);
}

Entries follow (functor, arity) order, independently of HashMap iteration order.

Literal Phases

GroundLiteral and LiteralPattern are checked wrappers that make illegal phase transitions unrepresentable. Literal::classify places every literal in exactly one:

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

match Literal::simple("bird").classify() {
    ClassifiedLiteral::Ground(g) => { /* g.as_literal() has no variables */ }
    ClassifiedLiteral::Pattern(p) => { /* p.ground(&bindings) -> GroundLiteral */ }
}
}

Shape Validation

A Shape compiled from a signature validates argument sorts at a boundary (e.g. before an effectful action). The reasoner never consults it:

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

let shape = Shape::from(&sig);
let report = shape.validate(&lit).unwrap();
// report.diagnostics: SortMismatch / PredicateMismatch / Deferred (for variables)
}

Parsing Predicate Indicators

The spindle-parser crate exposes a fully-consuming recognizer for the functor/arity notation (slash-bearing functors require quotes):

#![allow(unused)]
fn main() {
use spindle_parser::parse_predicate_indicator;

let sym = parse_predicate_indicator("assign-to/2").unwrap();
assert!(parse_predicate_indicator("rate/limit/2").is_err());        // ambiguous
let quoted = parse_predicate_indicator("\"rate/limit\"/2").unwrap(); // ok
}

Extension registry and aggregate preparation

prepare() supplies FunctionRegistry::with_prelude() and merges a host registry from PrepareOptions::function_registry. An ExtensionFunction implementation supplies a FunctionSignature and eval(&[Term]) -> Result<Term, EvalError>. registry.register(Box::new(function)) registers the implementation. Functions MUST be pure, deterministic, and Send + Sync. They receive values, not theory access.

ArithExpr::Call { name, args } represents both builtin and extension calls; Value supports general terms and Fold represents snapshot-aware aggregation. The former operator-specific AST variants are no longer the dispatch interface.

Named aggregators live in a separate registry namespace. register_aggregator(name, AggregatorDefinition { reducer, identity, count }) registers custom definitions. The aggregation guide describes reducer laws, preparation limits, and the Lean proof boundary.

Theory::metadata() remains label-keyed. predicate_metadata() accesses the separate predicate store. Vocabulary DTOs preserve conflicting declarations and provenance; declaration origins enrich coherent signatures when present.

WebAssembly

The spindle-wasm crate exposes a Spindle class to JavaScript. It uses the same preparation and reasoning pipeline as the Rust library.

The browser how-to covers initialization, object lifetime, error handling, and UI responsiveness.

Build targets

Builds require wasm-pack. Each target writes generated JavaScript and WASM files under crates/spindle-wasm/pkg.

Initialization is asynchronous. Instance methods run synchronously and throw JavaScript errors on parsing or reasoning failure.

Reasoning output

reason() returns a structured spindle.reason.v1 object, not a bare array. reasonV2() returns the corresponding spindle.reason.v2 object with typed term arguments. Both include:

• schema_version, evaluated_at, and grounding statistics.
• conclusions, whose entries include conclusion_type, literal_spl, literal_struct, and positive.
• diagnostics and theory stats.

result.conclusions contains the result entries. getPositiveConclusions() returns an array of positive literal strings. The shared DTO definitions live in spindle-contract; WASM returns the result as a JavaScript object rather than serialized JSON text.

Theory operations

SPL input supports structured predicates, arithmetic, metadata, and aggregates. The builtin prelude is available; the current JavaScript API does not expose host extension registration. See Aggregation for supported values and preparation restrictions.

Query methods

const status = spindle.query('flies');
// status.status: "provable", "refuted", or "unknown"
const hypothetical = spindle.whatIf(['bird'], 'flies');
// hypothetical.provable: boolean; new_conclusions: string[]
const why = spindle.whyNot('flies');
// why.is_provable, why.would_derive, why.blockers
const candidates = spindle.abduce('flies', 3);
// candidates.solutions: { facts: string[], rules_used: string[], confidence }[]

whatIf does not mutate the original theory and deduplicates newly positive literals. whyNot uses grounded rules for variable-headed diagnostics. Bounded temporal goals use exact windows; atemporal goals use family matching.

abduce returns raw candidates, not verified requirements. The WASM class has no requires method. The Rust requires_with_options API and CLI requires command verify candidates by full reasoning. See Query Operators.

How to run a theory in the browser

This guide uses the web target of spindle-wasm.

1. Install wasm-pack.

2. From the repository root, build the web target:

   make wasm
   

3. Copy the generated files from crates/spindle-wasm/pkg into your application's pkg directory.

4. Serve your application over HTTP with a server that serves WASM correctly.

5. Run this code from a JavaScript module beside pkg:

import init, { Spindle } from './pkg/spindle_wasm.js';

await init();
const spindle = new Spindle();
try {
    spindle.parseSpl(`
        (given (payment alice first 10))
        (given (payment alice second 10))
        (normally total
          (agg ?total sum ?amount (payment ?person ?id ?amount))
          (total-payment ?total))
    `);
    const result = spindle.reasonV2();
    console.log(result.schema_version); // spindle.reason.v2
    for (const conclusion of result.conclusions) {
        if (conclusion.positive) {
            console.log(conclusion.conclusion_type, conclusion.literal_spl);
        }
    }
} finally {
    spindle.free();
}

The console shows spindle.reason.v2 and positive conclusions, including (total-payment 20).

Repeated runs

Initialize the module once with await init(). Reuse a Spindle object while its owner remains active. Before rebuilding a theory programmatically, call clear(). When its owner is disposed, call free(). The example's finally block releases its single-use instance even after an error.

User interfaces

Store reasonV2().conclusions in application state. Render each conclusion's literal_spl value. Display initialization progress while init() runs. Catch parsing and reasoning errors at the application boundary. Display those errors to the user.

Calls on an initialized instance run synchronously. During representative grounding and aggregation jobs, measure input responsiveness and rendering delays. If these calls interrupt interaction or animation, run them in a worker. Measure the generated bundle size for your build; historical size estimates do not describe every application.

The WebAssembly reference describes methods, return values, and build targets.

Architecture

Workspace

Preparation and reasoning

Preparation turns source theories into inputs for ordinary reasoning. Aggregate preparation also reasons about earlier evidence before computing aggregate values.

A stratum is a dependency layer. Aggregate consumers read predicates from earlier layers, whose reasoning finishes first. A completed prefix contains the earlier rule layers together with their priorities and attackers. Reasoning completes that prefix before an aggregate reads its rows.

Snapshot lowering replaces aggregate calculations with results and fresh defeasible premises that record their evidence. These premises preserve the boundary between defeasible aggregate evidence and definite proof. Even a strict aggregate rule cannot promote this evidence to +D.

SPL → parser → Theory → prepare → prepared Theory → indexed reasoner → conclusions
                          │
                          ├─ ordinary: validate, rewrite wildcards, ground,
                          │            validate temporal variables, optional as-of filtering
                          │
                          └─ aggregates: infer strata, ground predicates,
                                         reason completed prefixes, lower snapshots

prepare(&theory, PrepareOptions) supplies the builtin function prelude and merges a host registry. Ordinary preparation uses composable PipelineStage implementations. Aggregate theories take a snapshot-aware preparation path; assembling only the ordinary pipeline stages does not implement aggregate semantics.

PrepareOptions controls grounding limits and configurable temporal/trust behavior. The aggregate path requires grounding and currently rejects temporal/trust options. Its max_instances budget includes repeated grounding passes; exhaustion returns an error rather than partial aggregate results.

Expressions and extensions

BodyLiteral represents logical premises or arithmetic constraints. ArithExpr contains numeric literals, variables, general values, registry-dispatched Call nodes, and Fold nodes. ExtensionFunction implementations receive evaluated Term arguments and return a value or error; they do not receive theory access.

Named aggregators have a separate namespace in FunctionRegistry. Their reducer, integer identity when supplied, and row-counting flag determine fold behavior. The host contract requires pure, associative, and commutative custom reducers. See Aggregation and Extension Functions.

Literal identity and vocabulary

Term distinguishes symbols, integers, decimals, and finite floats. Reasoning indexes use literal identity including the relevant temporal information; PredicateSymbol is only the structural (functor, arity) identity used by vocabulary tooling. It is not a proof-state key.

Predicate declarations, metadata, and provenance survive theory reconstruction. Theory::metadata() is label-keyed; predicate_metadata() is a separate store. Vocabulary derivation reports declarations, conflicts, argument profiles, and shape diagnostics without changing reasoning.

Constructive proof state

StandardReasoner implements traditional ambiguity-blocking DL(∂). State and propagation live under reason/, with definite and defeasible phases maintaining positive and negative evidence. Negative conclusions require constructive proof; there is no final sweep that labels every unproved literal negative.

Indexes and per-slot body counters support propagation. An unresolved cyclic premise remains undecided. It does not justify discarding an attacker. Definite proof implies defeasible proof even for contradictory facts; inconsistency does not cause unrelated conclusions. See Algorithms.

Aggregate evidence

Aggregate consumers read completed earlier strata, retaining priorities and attackers in the earlier rule prefix. The aggregate path deduplicates matching rows as whole rows, then reduces them. Snapshot lowering preserves the evidence boundary described above. User conclusions omit internal snapshot predicates. Prepared theories retain them for audit, and lowered rules retain source template labels.

Queries and trust

Queries reason over prepared theories and use exact matching for bounded temporal goals. requires_with_options verifies raw abduction candidates by rerunning reasoning. Explanation and blocker diagnostics connect grounded instances to source templates.

The trust pass computes weakest-link credibility, applies diminishment from applicable overruled defeaters to positive defeasible conclusions, and then checks thresholds. Definite conclusions are exempt from diminishment.

See Verification for the boundary between Lean proofs, Rust regression tests, and differential oracle checks.

Verification

The repository contains Lean models, proofs, and executable oracles alongside Rust tests. The current standard, family, and aggregate oracles use traditional ambiguity-blocking DL(∂) with four constructive tags.

What is checked

Lean modules cover arithmetic and grounding, temporal intervals and Allen relations, query models, trust operations, and aggregation. Aggregate proofs cover dependency checks, inferred strata, unordered row semantics, lowering, fixed-point completion, and equivalence of completed prefixes for all four tags.

Rust differential tests compare supported inputs with executable Lean models. The aggregate suite includes typed schemas, parsed SPL, grouping, empty input, duplicate contributions, conflicts, priorities, and cycles.

These are proofs of the stated models and differential checks of the Rust implementation, not a proof of whole-language Rust conformance. In particular:

• Rust aggregate arithmetic uses checked i64; Lean uses exact integers. Intermediate overflow is outside an unqualified refinement claim.
• Custom extension implementations and their reducer laws are host contracts.
• SPL parsing and extension registration are tested integrations.
• Historical lambda-only and strengthened two-sided models retain their own proofs; those results do not establish properties of the current standard backend.

Verification gate

The Lean gate builds libraries and oracle executables with warnings as errors. It rejects admitted proofs and local axioms, checks vacuity, and audits theorem axioms. The gate uses the Lean toolchain specified under lean/. Ordinary Cargo tests do not perform these checks.

Running verification checks gives the commands and external-oracle test examples.

See the repository's Lean guide, proof catalogue, and aggregate proof guide for theorem statements, hypotheses, and the full suite list.

Lattice Memoization Experiments

This document records February 2026 optimization experiments and findings. The implementations and untested proposals below describe that historical investigation.

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 were expected to check the same attackers
2. Caching attacker status promised to avoid repeated O(body_size) checks
3. A lattice-based approach (inspired by Ascent) offered a formal model for memoization

Approaches Tried

1. ProofStatus Lattice with Memoization

The first experiment 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

The second experiment cached active attackers per complement literal. It cleared the cache when the proven set grew.

Result: The experiment cleared the cache too often, providing no benefit.

3. Incremental Invalidation

The third experiment tracked pending_body_literals for each cache entry. It invalidated entries only when the reasoner proved relevant literals.

Result: Reduced unnecessary invalidation, but overhead still exceeded savings. Cloning the proven HashSet for snapshot tracking was expensive.

4. Lazy Attacker Tracking

The fourth experiment 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 investigation found the original is_blocked_by_superior 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

Proposed Memoization Applications

Effective Optimizations at the Time

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)

The investigation proposed these alternatives if later profiling identified is_blocked_by_superior as a bottleneck:

1. Bit vectors - Replacing HashSet with a bit vector for proven literals
2. Arena allocation - Pre-allocation of rules in contiguous memory
3. Rule ordering - Processing rules in topological order
4. SIMD body checks - Vectorization of body satisfaction for large bodies

Lessons Learned

1. Profiling matters - 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 investigation stored its experimental code 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 investigation retained the lattice module (lattice.rs) and memoized/lazy functions for reference. It did not adopt them for production.