Spindle-Rust

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

This project is part of the SPINdle family:

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

What is Defeasible Logic?

Defeasible logic is a non-monotonic reasoning system that allows conclusions to be defeated by stronger evidence. Unlike classical logic where adding new information only adds new conclusions, defeasible logic can revise existing conclusions when conflicting evidence appears.

# The classic "Tweety" example
f1: >> bird
f2: >> penguin

r1: bird => flies        # Birds typically fly
r2: penguin => -flies    # Penguins don't fly

r2 > r1                  # Penguin rule beats bird rule

Result: -flies is provable (Tweety doesn’t fly).

Features

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

Quick Example

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

let mut theory = Theory::new();

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

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

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

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

Installation

CLI

cargo install --path crates/spindle-cli

Library

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

Crate Structure

Crate	Description
`spindle-core`	Core reasoning engine
`spindle-parser`	DFL and SPL format parsers
`spindle-cli`	Command-line interface
`spindle-wasm`	WebAssembly bindings

References

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

License

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

Getting Started

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

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

Installation

Building from Source

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

Installing the CLI

cargo install --path crates/spindle-cli

This installs the spindle command to your Cargo bin directory.

Your First Theory

Create a file called hello.dfl:

# Facts
f1: >> bird

# Rules
r1: bird => flies
r2: bird => has_feathers

Run it:

spindle hello.dfl

Output:

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

Understanding the Output

Conclusion	Meaning
`+D bird`	`bird` is definitely provable (it’s a fact)
`+d bird`	`bird` is defeasibly provable
`+d flies`	`flies` is defeasibly provable via r1
`-D flies`	`flies` is not definitely provable (no strict rule)

The Penguin Example

Create penguin.dfl:

# Tweety is a bird and a penguin
f1: >> bird
f2: >> penguin

# Birds typically fly
r1: bird => flies

# Penguins typically don't fly
r2: penguin => -flies

# Penguin rule is more specific
r2 > r1

Run it:

spindle penguin.dfl

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

Using SPL Format

The same theory in SPL (Spindle Lisp) format, penguin.spl:

; Facts
(given bird)
(given penguin)

; Rules
(normally r1 bird flies)
(normally r2 penguin (not flies))

; Superiority
(prefer r2 r1)

Run it:

spindle penguin.spl

CLI Options

# Show only positive conclusions
spindle --positive penguin.dfl

# Use scalable algorithm (for large theories)
spindle --scalable penguin.dfl

# Output as JSON
spindle --json penguin.dfl

# Validate syntax without reasoning
spindle validate penguin.dfl

# Show theory statistics
spindle stats penguin.dfl

Using as a Library

Add to your Cargo.toml:

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

Basic usage:

use spindle_core::prelude::*;

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

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

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

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

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

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

Next Steps

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

Concepts

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

Classical vs. Defeasible Logic

Classical (Monotonic) Logic:

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

Defeasible (Non-Monotonic) Logic:

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

The Tweety Problem

The motivating example for defeasible logic:

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

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

f1: >> bird
f2: >> penguin
r1: bird => flies
r2: penguin => -flies
r2 > r1

Result: Tweety doesn’t fly.

Key Terminology

Term	Definition
Literal	An atomic proposition, possibly negated (e.g., `flies`, `-flies`)
Rule	A conditional statement with body and head
Theory	A collection of rules and superiority relations
Conclusion	A proven literal with a provability level
Defeat	When one rule blocks another’s conclusion
Superiority	A preference relation between rules

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

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

DFL:

f1: >> bird
f2: >> penguin
f3: >> -guilty    # Negated fact

SPL:

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

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

Strict Rules (`->`)

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

DFL:

r1: penguin -> bird        # All penguins are birds
r2: human, mortal -> dies  # All mortal humans die

SPL:

(always r1 penguin bird)
(always r2 (and human mortal) dies)

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

When to Use Strict Rules

Use strict rules for:

Definitional relationships (penguin -> bird)
Logical necessities (p, p->q -> q)
Constraints that have no exceptions

Defeasible Rules (`=>`)

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

DFL:

r1: bird => flies           # Birds typically fly
r2: student => has_loans    # Students typically have loans

SPL:

(normally r1 bird flies)
(normally r2 student has_loans)

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

Strict rules proving the opposite
Superior defeasible rules
Defeaters

When to Use Defeasible Rules

Use defeasible rules for:

Default behaviors with exceptions
Typical properties
Rules of thumb

Defeaters (`~>`)

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

DFL:

d1: broken_wing ~> flies    # A broken wing blocks "flies"

SPL:

(except d1 broken_wing flies)

Defeater vs. Defeasible Rule

# Defeasible rule: proves -flies
r1: penguin => -flies

# Defeater: only blocks flies, doesn't prove -flies
d1: sick ~> flies

The difference:

r1 can prove -flies if its body is satisfied
d1 can only block flies, it never proves -flies

When to Use Defeaters

Use defeaters when:

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

Rule Bodies (Antecedents)

Rule bodies can contain:

Single Literal

r1: bird => flies

Multiple Literals (Conjunction)

r1: bird, healthy => flies
r2: student, employed => busy

SPL:

(normally r1 (and bird healthy) flies)

Negated Literals

r1: bird, -penguin => flies   # Non-penguin birds fly

Rule Heads (Consequents)

Rule heads are single literals that can be:

Positive

r1: bird => flies

Negated

r1: penguin => -flies

Rule Labels

Every rule has a label (identifier) used for:

Superiority relations (r2 > r1)
Explanations
Debugging

DFL: Labels are required and appear before the colon:

my_rule: bird => flies

SPL: Labels are optional (auto-generated if omitted):

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

Summary

Rule Type	Symbol	Conclusion	Can be Defeated?
Fact	`>>`	+D	No
Strict	`->`	+D	No
Defeasible	`=>`	+d	Yes
Defeater	`~>`	None (blocks only)	N/A

Conclusions

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

The Four Conclusion Types

Symbol	Name	Meaning
`+D`	Definitely Provable	Proven via facts and strict rules only
`-D`	Definitely Not Provable	Cannot be proven via strict rules
`+d`	Defeasibly Provable	Proven via defeasible rules (may be defeated)
`-d`	Defeasibly Not Provable	Cannot be proven even defeasibly

Definite Conclusions (+D / -D)

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

f1: >> bird
r1: bird -> animal    # Strict rule
r2: bird => flies     # Defeasible rule

Conclusions:

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

When is +D Useful?

Use definite provability when you need certainty:

Legal requirements that must be met
Safety constraints
Logical necessities

Defeasible Conclusions (+d / -d)

Defeasible provability extends definite provability with defeasible rules.

f1: >> bird
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:

f1: >> trigger
r1: trigger => outcome
r2: trigger => -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:

f1: >> trigger
r1: trigger => outcome
r2: trigger => -outcome
r1 > r2

Conclusions:

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

Example: Multi-Level

f1: >> a
r1: a -> b           # Strict: a implies b
r2: b => c           # Defeasible: b typically implies c
r3: b => -c          # Defeasible: b typically implies -c
r2 > r3              # r2 wins

Conclusions:

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

Negative Conclusions

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

-D (Definitely Not Provable)

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

-d (Defeasibly Not Provable)

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

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

Reading Spindle Output

$ spindle penguin.dfl
+D bird
+D penguin
+d bird
+d penguin
+d -flies
-D flies
-D -flies
-d flies

Interpretation:

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

Filtering Output

Show only positive conclusions:

spindle --positive penguin.dfl

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:

f1: >> bird
f2: >> penguin
r1: bird => flies
r2: penguin => -flies

Both r1 and r2 fire. Without superiority, we get ambiguity - neither flies nor -flies is provable.

Declaring Superiority

The > operator declares that one rule is superior to another:

r2 > r1    # r2 beats r1

Now when both rules fire, r2 wins and -flies is provable.

SPL:

(prefer r2 r1)

Superiority Chains

You can declare chains of superiority:

DFL:

r3 > r2
r2 > r1

SPL (shorthand):

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

Transitivity

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

r3 > r2
r2 > r1
r3 > r1    # Must be explicit

Conflict Resolution Algorithm

When evaluating a defeasible conclusion:

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

Example: Three-Way Conflict

f1: >> a
f2: >> b
f3: >> c

r1: a => result
r2: b => -result
r3: c => result

r1 > r2    # r1 beats r2
r3 > r2    # r3 beats r2

Analysis:

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

Symmetric Conflicts

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

f1: >> trigger
r1: trigger => a
r2: trigger => -a
# No superiority

Result: Neither a nor -a is provable.

Defeating Defeaters

Defeaters can be overridden by superiority:

f1: >> bird
f2: >> healthy

r1: bird => flies
d1: bird ~> flies      # Defeater blocks flies
r2: healthy => flies

r2 > d1                # Healthy birds overcome the defeater

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

Strict Rules and Superiority

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

f1: >> p
r1: p -> q           # Strict
r2: p => -q          # Defeasible
r2 > r1              # This has no effect!

Result: +D q (strict rule wins)

Superiority only affects conflicts between:

Defeasible rules
Defeasible rules and defeaters
Defeaters

Best Practices

Use Specificity

More specific rules should be superior:

r2: penguin => -flies
r1: bird => flies
r2 > r1    # Penguin is more specific than bird

Document Reasoning

Use comments to explain why one rule beats another:

# Medical override: confirmed diagnosis beats symptoms
r_diagnosis > r_symptoms

Avoid Cycles

Don’t create circular superiority:

# BAD - creates a cycle
r1 > r2
r2 > r1

This leads to undefined behavior.

Negation

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

Strong Negation vs. Negation-as-Failure

Negation-as-Failure (NAF)

Used in Prolog and many logic programming systems:

“not P” means “P cannot be proven”
Absence of evidence is evidence of absence

Strong Negation

Used in Spindle:

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

Syntax

Both - and ~ denote negation:

DFL:

f1: >> -guilty       # Explicitly not guilty
r1: penguin => ~flies

SPL:

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

Three-Valued Outcomes

For any literal P, the outcome can be:

State	Meaning	Conclusions
True	P is provable	`+d P`
False	-P is provable	`+d -P`
Unknown	Neither provable	`-d P` and `-d -P`

Example: Unknown State

f1: >> bird
r1: bird => flies
# No information about grounded

Conclusions:

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

The grounded literal is in an unknown state.

Complementary Literals

P and -P are complements. They interact in specific ways:

Conflict

If rules prove both P and -P:

f1: >> a
r1: a => p
r2: a => -p

Without superiority, neither is provable (ambiguity).

Definite Blocking

If -P is definitely provable, P cannot be defeasibly provable:

f1: >> -p        # Definite fact: -p
r1: a => p       # Tries to prove p

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

Negation in Rule Bodies

Negated literals can appear in rule bodies:

r1: bird, -penguin => flies    # Non-penguin birds fly
r2: student, -employed => needs_loan

SPL:

(normally r1 (and bird (not penguin)) flies)

Double Negation

--P is equivalent to P:

r1: a => --flies    # Same as: a => flies

Consistency

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

f1: >> p
f2: >> -p

Result:

+D p
+D -p

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

Detecting Inconsistency

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

Closed World Assumption

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

# CWA for 'guilty': if not proven guilty, then not guilty
d1: >> -guilty           # Default: not guilty
r1: evidence => guilty   # Can be overridden by evidence
r1 > d1

This pattern uses a defeatable default.

DFL Format Reference

DFL (Defeasible Logic Format) is a textual syntax for writing defeasible logic theories.

File Extension

.dfl

Comments

Lines starting with # are comments:

# This is a comment
f1: >> bird   # Inline comment

Grammar

theory      = (rule | superiority | comment | blank)*
rule        = label ":" body? arrow head
superiority = label ">" label
label       = identifier
body        = literal ("," literal)*
head        = literal
literal     = negation? identifier
negation    = "-" | "~" | "¬"
arrow       = ">>" | "->" | "=>" | "~>"
identifier  = [a-zA-Z_][a-zA-Z0-9_-]*
comment     = "#" .*
blank       = whitespace

Rules

Facts (`>>`)

No body, unconditional truth.

f1: >> bird
f2: >> penguin
f3: >> -guilty

Strict Rules (`->`)

Body implies head necessarily.

r1: penguin -> bird
r2: human, mortal -> dies
r3: a, b, c -> result

Defeasible Rules (`=>`)

Body typically implies head.

r1: bird => flies
r2: penguin => -flies
r3: student, employed => busy

Defeaters (`~>`)

Body blocks head (doesn’t prove it).

d1: broken_wing ~> flies
d2: exception ~> normal_behavior

Literals

Simple Literals

bird
flies
has_feathers

Negated Literals

All three forms are equivalent:

-flies
~flies
¬flies

Identifiers

Valid identifiers:

Start with letter or underscore
Contain letters, digits, underscores, hyphens

bird
_private
has-feathers
rule_1

Rule Bodies

Single Literal

r1: bird => flies

Multiple Literals (Conjunction)

Comma-separated:

r1: bird, healthy => flies
r2: a, b, c, d => result

Mixed Negation

r1: bird, -penguin => flies
r2: student, -rich, -employed => needs_loan

Superiority Relations

Declare that one rule beats another:

r2 > r1
more_specific > general
exception > default

Multiple declarations:

r3 > r2
r2 > r1

Complete Example

# The Penguin Example
# Demonstrates defeasible reasoning with exceptions

# Facts
f1: >> bird
f2: >> penguin

# Strict rule: all penguins are birds
s1: penguin -> bird

# Defeasible rules
r1: bird => flies
r2: bird => has_feathers
r3: penguin => -flies
r4: penguin => swims

# Superiority: penguin rules beat bird rules
r3 > r1

# Defeater: broken wings block flying
d1: broken_wing ~> flies

Whitespace

Leading/trailing whitespace is ignored
Whitespace around operators is optional
Blank lines are ignored

These are equivalent:

r1: bird => flies
r1:bird=>flies
r1 : bird => flies

Error Handling

Common errors:

Error	Example	Problem
Missing label	`>> bird`	Rules need labels
Missing colon	`r1 >> bird`	Colon required after label
Invalid arrow	`r1: bird -> flies`	Wrong arrow for defeasible
Undefined rule	`r3 > r1`	r3 not defined

Best Practices

Use meaningful labels

# Good
bird_flies: bird => flies

# Avoid
r1: bird => flies

Group related rules

# Bird rules
r1: bird => flies
r2: bird => has_feathers

# Penguin rules
r3: penguin => -flies

Document superiority

# Penguin is more specific than bird
r3 > r1

SPL Format Reference

SPL (Spindle Lisp) is a LISP-based DSL for defeasible logic with support for advanced features like variables, temporal reasoning, and metadata.

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
fact        = "(given" literal ")"
rule        = "(" keyword label? body head ")"
keyword     = "always" | "normally" | "except"
prefer      = "(prefer" label+ ")"
meta        = "(meta" label property* ")"
literal     = atom | "(" atom arg* ")" | "(not" literal ")"
body        = literal | "(and" literal+ ")"
atom        = identifier | variable
variable    = "?" identifier

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 r1 penguin bird)
(always r2 (and human mortal) dies)

Defeasible Rules (`normally`)

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

Defeaters (`except`)

(except d1 broken-wing flies)

Unlabeled Rules

Labels are optional (auto-generated):

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

Literals

Simple

bird
flies
has-feathers

Negated

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

Or with prefix:

~flies

Predicates with Arguments

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

Conjunction

Use and for multiple conditions:

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

Variables

Variables start with ?:

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

; Transitive closure
(normally r1 (parent ?x ?y) (ancestor ?x ?y))
(normally r2 (and (parent ?x ?y) (ancestor ?y ?z)) (ancestor ?x ?z))

Wildcard

Use _ to match anything:

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

Superiority

Two Rules

(prefer r2 r1)    ; r2 > r1

Chain

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

Expands to:

(prefer r3 r2)
(prefer r2 r1)

Metadata

Attach metadata to rules:

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

Properties

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

Obligation (`must`)

(normally signed-contract (must pay))

Permission (`may`)

(normally member (may access))

Forbidden (`forbidden`)

(normally unauthorized (forbidden enter))

Temporal Reasoning

Time Points

(moment 2024)                    ; Year
(moment 2024 6 15)               ; Year, month, day
(moment 2024 6 15 14 30 0 "UTC") ; Full timestamp
(moment "2024-06-15T14:30:00Z")  ; ISO 8601
inf                              ; Positive infinity
-inf                             ; Negative infinity

During

(given (during bird 1 10))
(given (during (employed alice acme) (moment 2020) (moment 2023)))

Allen Relations

All 13 Allen interval relations:

(before ?t1 ?t2)       ; t1 ends before t2 starts
(after ?t1 ?t2)        ; t1 starts after t2 ends
(meets ?t1 ?t2)        ; t1 ends exactly when t2 starts
(met-by ?t1 ?t2)       ; t1 starts exactly when t2 ends
(overlaps ?t1 ?t2)     ; t1 starts before t2, ends during t2
(overlapped-by ?t1 ?t2)
(contains ?t1 ?t2)     ; t1 strictly contains t2
(within ?t1 ?t2)       ; t1 is strictly within t2
(starts ?t1 ?t2)       ; Same start, t1 ends first
(started-by ?t1 ?t2)
(finishes ?t1 ?t2)     ; t1 starts after t2, same end
(finished-by ?t1 ?t2)
(equals ?t1 ?t2)       ; Same start and end

Complete Example

; The Penguin Example

; Facts
(given bird)
(given penguin)

; Strict rule
(always s1 penguin bird)

; Defeasible rules
(normally r1 bird flies)
(normally r2 bird has-feathers)
(normally r3 penguin (not flies))
(normally r4 penguin swims)

; Superiority
(prefer r3 r1)

; Defeater
(except d1 broken-wing flies)

; Metadata
(meta r1 (description "Birds typically fly"))
(meta r3 (description "Penguins are an exception"))

DFL vs SPL Comparison

Concept	DFL	SPL
Fact	`f1: >> bird`	`(given bird)`
Strict	`r1: a -> b`	`(always r1 a b)`
Defeasible	`r1: a => b`	`(normally r1 a b)`
Defeater	`d1: a ~> b`	`(except d1 a b)`
Superiority	`r2 > r1`	`(prefer r2 r1)`
Negation	`-flies`	`(not flies)`
Conjunction	`a, b => c`	`(normally (and a b) c)`
Variables	Not supported	`?x`, `?y`
Predicates	Not supported	`(parent ?x ?y)`

CLI Reference

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

Installation

cargo install --path crates/spindle-cli

Synopsis

spindle [OPTIONS] <FILE>
spindle <COMMAND> [OPTIONS] <FILE>

Commands

reason (default)

Perform defeasible reasoning on a theory.

spindle examples/penguin.dfl
spindle reason examples/penguin.dfl

validate

Check syntax without reasoning.

spindle validate examples/penguin.dfl

Output on success:

Valid DFL theory.

Output on error:

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

stats

Show theory statistics.

spindle stats examples/penguin.dfl

Output:

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

Options

`--scalable`

Use the scalable DL(d||) algorithm instead of standard DL(d).

spindle --scalable large-theory.dfl

Recommended for theories with:

More than 1000 rules
Complex conflict resolution
Long inference chains

`--positive`

Show only positive conclusions (+D, +d).

spindle --positive examples/penguin.dfl

Output:

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

File Format Detection

The CLI auto-detects format by extension:

Extension	Format
`.dfl`	DFL (Defeasible Logic Format)
`.spl`	SPL (Spindle Lisp)

Exit Codes

Code	Meaning
0	Success
1	Error (parse error, file not found, etc.)

Examples

Basic Reasoning

# Reason about a theory
spindle penguin.dfl

# Same with explicit command
spindle reason penguin.dfl

Validate Before Reasoning

spindle validate theory.dfl && spindle theory.dfl

Compare Algorithms

# Standard algorithm
spindle theory.dfl > standard.txt

# Scalable algorithm
spindle --scalable theory.dfl > scalable.txt

# Compare (should be identical for correct theories)
diff standard.txt scalable.txt

Scripting

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

Environment Variables

Variable	Description
`SPINDLE_LOG`	Set log level (error, warn, info, debug, trace)

SPINDLE_LOG=debug spindle theory.dfl

Algorithms

Spindle implements two reasoning algorithms: standard DL(d) and scalable DL(d||).

Standard DL(d)

The default algorithm uses forward chaining to compute conclusions.

How It Works

Initialize: Add all facts to the proven set
Propagate: Find rules whose bodies are satisfied
Fire: Add conclusions, checking for conflicts
Repeat: Until no new conclusions

Pseudocode

function reason(theory):
    proven = {}

    # Phase 1: Facts
    for fact in theory.facts:
        add_conclusion(+D, fact.head)
        add_conclusion(+d, fact.head)
        worklist.add(fact.head)

    # Phase 2: Forward chaining
    while worklist not empty:
        literal = worklist.pop()

        for rule in rules_with_body_containing(literal):
            if body_satisfied(rule, proven):
                if rule.type == Strict:
                    add_conclusion(+D, rule.head)
                    add_conclusion(+d, rule.head)
                elif rule.type == Defeasible:
                    if not blocked_by_superior(rule):
                        add_conclusion(+d, rule.head)
                # Defeaters don't add conclusions

    # Phase 3: Negative conclusions
    for literal in all_literals:
        if literal not in proven[+D]:
            add_conclusion(-D, literal)
        if literal not in proven[+d]:
            add_conclusion(-d, literal)

Conflict Resolution

When a defeasible rule fires, we check for blocking:

function blocked_by_superior(rule):
    complement = negate(rule.head)

    for attacker in rules_for(complement):
        if body_satisfied(attacker):
            if attacker.type == Defeater:
                if not is_superior(rule, attacker):
                    return true  # Blocked by defeater
            elif attacker.type == Defeasible:
                if is_superior(attacker, rule):
                    return true  # Blocked by superior rule

    return false

Complexity

Time: O(n * m) where n = rules, m = average body size
Space: O(n) for proven literals

Scalable DL(d||)

For large theories, the three-phase algorithm is more efficient.

Overview

Theory → [Delta] → [Lambda] → [Partial] → Conclusions
            ↓          ↓           ↓
       Definite   Potential   Defeasible
       (+D)       (approx)    (+d)

Phase 1: Delta Closure (P_Δ)

Computes definite conclusions using only facts and strict rules.

function compute_delta(theory):
    delta = {}
    worklist = theory.facts

    while worklist not empty:
        literal = worklist.pop()
        delta.add(literal)

        for rule in strict_rules_with_body(literal):
            if body_satisfied(rule, delta):
                if rule.head not in delta:
                    worklist.add(rule.head)

    return delta

Result: All +D conclusions.

Phase 2: Lambda Closure (P_λ)

Computes an over-approximation of defeasible conclusions.

A literal is in lambda if:

It’s in delta, OR
Some strict/defeasible rule has:
- Body fully in lambda
- Complement NOT in delta

function compute_lambda(theory, delta):
    lambda = delta.copy()
    worklist = delta.copy()

    while worklist not empty:
        literal = worklist.pop()

        for rule in rules_with_body(literal):
            if rule.type in [Strict, Defeasible]:
                if body_satisfied(rule, lambda):
                    if complement(rule.head) not in delta:
                        if rule.head not in lambda:
                            lambda.add(rule.head)
                            worklist.add(rule.head)

    return lambda

Key insight: If something is NOT in lambda, it’s definitely not defeasibly provable. This allows efficient pruning.

Phase 3: Partial Closure (P_∂||)

Computes actual defeasible conclusions with conflict resolution.

function compute_partial(theory, delta, lambda):
    partial = delta.copy()

    candidates = lambda - delta  # Only check these
    changed = true

    while changed:
        changed = false
        for literal in candidates:
            if literal not in partial:
                if can_prove_defeasibly(literal, partial, lambda):
                    partial.add(literal)
                    changed = true

    return partial

The can_prove_defeasibly function:

function can_prove_defeasibly(literal, partial, lambda):
    # Need a supporting rule with satisfied body
    has_support = false
    for rule in rules_for(literal):
        if rule.type in [Strict, Defeasible]:
            if body_satisfied(rule, partial):
                has_support = true
                break

    if not has_support:
        return false

    # All attacks must be defeated
    for attacker in rules_for(complement(literal)):
        # Attack fails if body not satisfiable
        if not body_satisfiable(attacker, lambda):
            continue

        # Attack fails if we have a superior defender
        if team_defeats(literal, attacker, partial):
            continue

        # This attack succeeds
        return false

    return true

Performance Comparison

Aspect	Standard	Scalable
Small theories (<100 rules)	Faster	Overhead
Large theories (>1000 rules)	Slower	Faster
Memory	Lower	Higher (3 sets)
Conflicts	Per-rule check	Batch processing

When to Use Scalable

Use --scalable when:

Theory has >1000 rules
Many potential conflicts
Long inference chains
Lambda pruning will help

Semi-Naive Evaluation

Phase 3 uses semi-naive evaluation for efficiency:

Instead of checking all candidates each iteration, only check literals whose dependencies changed:

function compute_partial_seminaive(theory, delta, lambda):
    partial = delta.copy()
    worklist = rules_with_empty_body()

    while worklist not empty:
        literal = worklist.pop()

        if can_prove_defeasibly(literal, partial, lambda):
            partial.add(literal)

            # Only add rules triggered by this literal
            for rule in rules_with_body(literal):
                if body_satisfied(rule, partial):
                    worklist.add(rule.head)

    return partial

This avoids redundant checks and provides significant speedup for large theories.

Semantic Equivalence

Both algorithms produce identical results for well-formed theories:

∀ theory: reason(theory) ≡ reason_scalable(theory)

The test suite verifies this property across many test cases.

Variables and Grounding

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

Variable Syntax

Variables are prefixed with ?:

?x
?person
?any_value

Basic Example

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

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

The rule r1 matches against facts:

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

Transitive Closure

A classic example - computing ancestors:

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

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

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

Results:

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

How Grounding Works

Step 1: Collect Ground Facts

Extract all predicate instances from facts:

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

Step 2: Match Rule Bodies

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

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

Substitutions:

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

Step 3: Generate Ground Rules

Apply substitutions to create ground instances:

; Ground instances of r1
r1_1: parent(alice, bob) => ancestor(alice, bob)
r1_2: parent(bob, charlie) => ancestor(bob, charlie)

Step 4: Forward Chaining

Reason over the ground theory using standard algorithms.

Multiple Variables

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

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

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

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

Wildcard Variable

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

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

This matches any parent relationship.

Variable Scope

Variables are scoped to their rule:

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

Safety Requirement

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

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

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

Unsafe rules would generate infinite ground instances.

Negation with Variables

Negated predicates in the body:

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

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

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

Grounding with Superiority

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

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

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

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

Performance Considerations

Grounding can produce many rules:

Facts	Rule Body Size	Ground Rules
100	1	100
100	2 (join)	up to 10,000
100	3 (join)	up to 1,000,000

Tips:

Keep rule bodies small
Use specific predicates to reduce matching
Consider the --scalable flag for large ground theories

DFL Limitations

The DFL format does not support variables. Use SPL for first-order rules:

# DFL - no variables, must enumerate manually
r1: parent_alice_bob => ancestor_alice_bob
r2: parent_bob_charlie => ancestor_bob_charlie

; SPL - single rule with variables
(normally r1 (parent ?x ?y) (ancestor ?x ?y))

Temporal Reasoning

Spindle supports temporal reasoning using Allen’s interval algebra.

Time Points

Basic Moments

(moment 2024)                      ; Year only
(moment 2024 6 15)                 ; Year, month, day
(moment 2024 6 15 14 30 0 "UTC")   ; Full timestamp
(moment "2024-06-15T14:30:00Z")    ; ISO 8601 string

Special Values

inf    ; Positive infinity (never ends)
-inf   ; Negative infinity (always existed)

During Operator

The during operator associates a literal with a time interval:

(given (during bird 1 10))
(given (during (employed alice acme) (moment 2020) (moment 2023)))

Syntax: (during literal start end)

Example: Employment History

; Alice worked at Acme from 2020 to 2022
(given (during (employed alice acme) (moment 2020) (moment 2022)))

; Alice works at Beta from 2022 onwards
(given (during (employed alice beta) (moment 2022) inf))

; Employees can access company resources
(normally r1 (during (employed ?x ?company) ?t) (during (can-access ?x ?company) ?t))

Allen’s Interval Relations

Spindle supports all 13 Allen interval relations for comparing time intervals.

Basic Relations

(before ?t1 ?t2)    ; t1 ends before t2 starts
                    ; |--t1--|
                    ;           |--t2--|

(after ?t1 ?t2)     ; t1 starts after t2 ends
                    ;           |--t1--|
                    ; |--t2--|

(meets ?t1 ?t2)     ; t1 ends exactly when t2 starts
                    ; |--t1--|
                    ;        |--t2--|

(met-by ?t1 ?t2)    ; t1 starts exactly when t2 ends
                    ;        |--t1--|
                    ; |--t2--|

Overlap Relations

(overlaps ?t1 ?t2)      ; t1 starts before t2, ends during t2
                        ; |----t1----|
                        ;       |----t2----|

(overlapped-by ?t1 ?t2) ; t2 starts before t1, ends during t1
                        ;       |----t1----|
                        ; |----t2----|

Containment Relations

(contains ?t1 ?t2)  ; t1 strictly contains t2
                    ; |--------t1--------|
                    ;     |--t2--|

(within ?t1 ?t2)    ; t1 is strictly within t2
                    ;     |--t1--|
                    ; |--------t2--------|

(starts ?t1 ?t2)      ; Same start, t1 ends first
                      ; |--t1--|
                      ; |------t2------|

(started-by ?t1 ?t2)  ; Same start, t2 ends first
                      ; |------t1------|
                      ; |--t2--|

(finishes ?t1 ?t2)    ; t1 starts after t2, same end
                      ;       |--t1--|
                      ; |------t2----|

(finished-by ?t1 ?t2) ; t2 starts after t1, same end
                      ; |------t1----|
                      ;       |--t2--|

(equals ?t1 ?t2)      ; Same start and end
                      ; |----t1----|
                      ; |----t2----|

Temporal Rules

Propagating Temporal Properties

; If something is a bird during interval t, it has feathers during t
(normally r1 (during bird ?t) (during has-feathers ?t))

Temporal Constraints

; Events that precede others
(normally r1
  (and (during event1 ?t1)
       (during event2 ?t2)
       (before ?t1 ?t2))
  event1-precedes-event2)

Overlapping Intervals

; If two meetings overlap, there's a conflict
(normally conflict
  (and (during (meeting ?room ?m1) ?t1)
       (during (meeting ?room ?m2) ?t2)
       (overlaps ?t1 ?t2))
  (scheduling-conflict ?room))

Example: Project Timeline

; Project phases
(given (during (phase design) (moment 2024 1 1) (moment 2024 3 31)))
(given (during (phase implementation) (moment 2024 3 1) (moment 2024 8 31)))
(given (during (phase testing) (moment 2024 7 1) (moment 2024 9 30)))

; Phases that overlap
(normally r1
  (and (during (phase ?p1) ?t1)
       (during (phase ?p2) ?t2)
       (overlaps ?t1 ?t2))
  (parallel-work ?p1 ?p2))

; Resource needed during phase
(normally r2 (during (phase implementation) ?t) (during needs-developers ?t))

Querying at Specific Times

To query conclusions at a specific time, filter the results by temporal bounds.

; Is alice employed at acme in 2021?
; Check: (during (employed alice acme) ?t) where 2021 is within ?t

Limitations

Discrete time: Moments are discrete, not continuous
No duration arithmetic: Cannot compute t1 + 5 days
No fuzzy boundaries: Intervals have precise start/end
Grounding required: Temporal variables must be bound by facts

Best Practices

Use meaningful intervals

; Good: named intervals
(given (during project-alpha (moment 2024 1 1) (moment 2024 12 31)))

; Avoid: magic numbers
(given (during x 1 365))

Document temporal semantics

; Employment is during working hours only
(meta r1 (note "Applies during business hours"))

Consider open intervals

; Ongoing employment (no end date)
(given (during (employed alice acme) (moment 2024) inf))

Query Operators

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

What-If Queries

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

API

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

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

How It Works

Create a copy of the theory
Add hypothetical facts
Reason over the modified theory
Return new conclusions

Example

Original theory:

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

Query: What if wounded is true?

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

Use Cases

Exploring consequences of decisions
Scenario analysis
Testing rule interactions

Why-Not Queries

Why-not explains why a literal is NOT provable.

API

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

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

How It Works

Check if the literal is actually unprovable
Find rules that could prove it
For each rule, identify what’s blocking it:
- Missing body literals
- Defeated by superior rules
- Blocked by defeaters

Example

Theory:

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

Query: Why is flies not provable?

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

Result Structure

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

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

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

Use Cases

Debugging unexpected results
Understanding rule interactions
Explaining decisions to users

Abduction

Abduction finds hypotheses that would make a goal provable.

API

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

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

How It Works

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

Example

Theory:

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

Query: What facts would make flies provable?

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

Solution Structure

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

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

Handling Conflicts

Abduction considers superiority:

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

Abducing flies might return:

["bird", "healthy"] with a rule r3: bird, healthy => flies where r3 > r2
Or indicate that flies cannot be achieved given penguin

Use Cases

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

Combined Queries

Debugging Workflow

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

Example Session

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

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

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

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

WebAssembly API

The WASM bindings expose these operators:

import { Spindle } from 'spindle-wasm';

const spindle = new Spindle();
spindle.parseDfl(`
  f1: >> bird
  f2: >> penguin
  r1: bird => flies
  r2: penguin => ~flies
  r2 > r1
`);

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

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

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

Limitations

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

Performance Tuning

This guide covers performance optimization for Spindle.

Choosing an Algorithm

Standard DL(d)

Best for:

Small to medium theories (<1000 rules)
Simple conflict patterns
Low memory environments

spindle theory.dfl

Scalable DL(d||)

Best for:

Large theories (>1000 rules)
Complex conflict resolution
Long inference chains

spindle --scalable theory.dfl

Benchmark Your Theory

# Time both algorithms
time spindle theory.dfl > /dev/null
time spindle --scalable theory.dfl > /dev/null

Theory Design

Minimize Rule Bodies

Larger bodies = more matching work:

; Slower: 5-way join
(normally r1 (and a b c d e) result)

; Faster: chain of 2-way joins
(normally r1 (and a b) ab)
(normally r2 (and ab c) abc)
(normally r3 (and abc d) abcd)
(normally r4 (and abcd e) result)

Use Specific Predicates

; Slower: matches all 'thing' facts
(normally r1 (thing ?x) (processed ?x))

; Faster: matches only relevant facts
(normally r1 (unprocessed-item ?x) (processed ?x))

Reduce Grounding Explosion

Variables can cause combinatorial explosion:

; If there are 100 'node' facts, this creates 10,000 ground rules
(normally r1 (and (node ?x) (node ?y)) (pair ?x ?y))

; Add constraints to reduce matching
(normally r1 (and (node ?x) (node ?y) (edge ?x ?y)) (connected ?x ?y))

Memory Optimization

String Interning

Spindle uses string interning internally. You can benefit by:

#![allow(unused)]
fn main() {
// Reuse literal names
let bird = "bird";
theory.add_fact(bird);
theory.add_defeasible_rule(&[bird], "flies");
}

Stream Large Results

For large result sets:

#![allow(unused)]
fn main() {
// Instead of collecting all conclusions
let conclusions: Vec<Conclusion> = theory.reason();

// Process incrementally (future API)
for conclusion in theory.reason_iter() {
    process(conclusion);
}
}

Theory Cloning

Avoid unnecessary cloning:

#![allow(unused)]
fn main() {
// Expensive: clones the whole theory
let copy = theory.clone();

// Better: reuse the indexed theory
let indexed = IndexedTheory::build(theory);
// Use indexed for multiple queries
}

Conflict Optimization

Minimize Conflicts

Fewer conflicts = faster resolution:

; Many potential conflicts
(normally r1 a result)
(normally r2 b ~result)
(normally r3 c result)
(normally r4 d ~result)

; Better: restructure to reduce conflicts
(normally supports a supports-result)
(normally supports c supports-result)
(normally opposes b opposes-result)
(normally opposes d opposes-result)
(normally conclusion supports-result result)
(normally conclusion opposes-result ~result)
(prefer conclusion ...)

Explicit Superiority

Unresolved conflicts cause ambiguity propagation:

; Bad: no superiority, causes ambiguity checks
(normally r1 a q)
(normally r2 b ~q)

; Good: explicit resolution
(normally r1 a q)
(normally r2 b ~q)
(prefer r1 r2)  ; or (prefer r2 r1)

Indexing Benefits

Spindle indexes rules by:

Head literal → O(1) lookup
Body literal → O(1) lookup
Superiority → O(1) lookup

The indexed theory is built once and reused:

#![allow(unused)]
fn main() {
let indexed = IndexedTheory::build(theory);

// Fast: O(1) lookups
for rule in indexed.rules_with_head(&literal) { ... }
for rule in indexed.rules_with_body(&literal) { ... }
}

Profiling

Theory Statistics

spindle stats theory.dfl

Look for:

High rule count → consider --scalable
Many defeaters → potential blocking overhead
Complex bodies → grounding overhead

Rust Profiling

# Build with profiling
cargo build --release

# Profile with flamegraph
cargo flamegraph -- spindle theory.dfl

Memory Profiling

# Use heaptrack
heaptrack spindle large-theory.dfl
heaptrack_print heaptrack.spindle.*.gz

Benchmarks

Run the built-in benchmarks:

cd crates/spindle-core
cargo bench

Key benchmarks:

reason_penguin - basic conflict resolution
reason_long_chain - forward chaining depth
reason_wide - parallel independent rules
scalable_vs_standard - algorithm comparison

Performance Checklist

Choose the right algorithm
- Small theory → standard
- Large theory → --scalable
Optimize theory design
- Keep rule bodies small
- Use specific predicates
- Control grounding size
Resolve conflicts
- Add superiority relations
- Avoid unnecessary ambiguity
Monitor resources
- Check spindle stats output
- Profile if needed
- Benchmark algorithm choice

Troubleshooting

Common issues and how to resolve them.

Parse Errors

“Could not parse” Error

Error at line 5: could not parse: bird flies

Cause: Missing arrow operator.

Fix: Add the correct arrow:

r1: bird => flies

“Unknown keyword” Error (SPL)

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)

Missing Label (DFL)

Error at line 3: could not parse: >> bird

Cause: DFL rules require labels.

Fix: Add a label:

f1: >> bird

Unexpected Conclusions

Expected Conclusion Missing

Symptom: A literal you expected to be +d is -d.

Debugging steps:

Check if the rule exists:
```
spindle stats theory.dfl
```

Check if the body is satisfied:

# Is 'bird' actually proven?
r1: bird => flies

Check for conflicts:

# Look for rules proving the complement
grep "~flies\|-flies" theory.dfl

Check superiority:

# Is there a superior rule blocking?
grep ">" theory.dfl

Unexpected Conclusion Present

Symptom: A literal is +d when it shouldn’t be.

Debugging steps:

Find which rule proves it:

grep "=> literal\|-> literal" theory.dfl

Check if a defeater is missing:

# Add a defeater to block
d1: exception ~> unexpected_literal

Both Literals Unprovable (Ambiguity)

Symptom: Neither q nor ~q is +d.

Cause: Conflicting rules without superiority.

Fix: Add superiority:

r1: a => q
r2: b => ~q
r1 > r2    # or r2 > r1

Superiority Issues

Superiority Not Working

Symptom: Declared r1 > r2 but r2 still wins.

Check:

Rule labels match exactly:

r1: bird => flies      # Label is "r1"
r2: penguin => ~flies  # Label is "r2"
r1 > r2                # Must match exactly

Rule type compatibility:
- Superiority only affects defeasible rules and defeaters
- Strict rules always win regardless of superiority

Both rules actually fire:

# Both bodies must be satisfied
spindle --positive theory.dfl | grep "bird\|penguin"

Circular Superiority

# BAD: creates undefined behavior
r1 > r2
r2 > r1

Fix: Remove one declaration or restructure rules.

Grounding Issues

Variables Not Matching

Symptom: Rules with variables don’t produce expected results.

Check:

Facts use predicates:

; Wrong: not a predicate
(given parent-alice-bob)

; Right: predicate with arguments
(given (parent alice bob))

Variable positions match:

; Fact: (parent alice bob)
;              ?x    ?y

; Rule must match positions
(normally r1 (parent ?x ?y) (ancestor ?x ?y))

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
Use the --scalable flag

File Format Issues

Wrong Format Detection

Symptom: File parses incorrectly.

Fix: Use correct extension:

.dfl for DFL format
.spl for SPL format

Encoding Issues

Symptom: Special characters cause errors.

Fix: Use UTF-8 encoding. The negation symbol ¬ is supported.

Algorithm Differences

Different Results: Standard vs Scalable

Symptom: --scalable gives different results.

This should not happen. Both algorithms are semantically equivalent.

Debug:

spindle theory.dfl > standard.txt
spindle --scalable theory.dfl > scalable.txt
diff standard.txt scalable.txt

If different, please report a bug.

Performance Issues

Slow Reasoning

Check:

Theory size: spindle stats theory.dfl
Algorithm: try --scalable for large theories
Grounding: check for variable explosion
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
Use --scalable algorithm
Restructure theory

Debugging Tips

Validate First

Always validate before reasoning:

spindle validate theory.dfl && spindle theory.dfl

Minimal Reproduction

Create a minimal theory that reproduces the issue:

# Start with just the failing rules
f1: >> bird
r1: bird => flies
# Add rules until issue appears

Use Positive Output

Focus on what IS proven:

spindle --positive theory.dfl

Check Statistics

spindle stats theory.dfl

Look for unexpected counts.

Enable Logging

SPINDLE_LOG=debug spindle theory.dfl 2>&1 | less

Getting Help

If you can’t resolve an issue:

Create a minimal reproduction
Include the theory file
Show expected vs actual output
Report at: https://codeberg.org/anuna/spindle-rust/issues

Rust Library Guide

This guide covers using Spindle as a Rust library.

Installation

Add to your Cargo.toml:

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

Basic Usage

use spindle_core::prelude::*;

fn main() {
    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);
        }
    }
}

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 DFL

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

let dfl = r#"
    f1: >> bird
    f2: >> penguin
    r1: bird => flies
    r2: penguin => ~flies
    r2 > r1
"#;

let theory = parse_dfl(dfl)?;
}

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

Standard Algorithm

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

let conclusions = reason(&theory);
}

Scalable Algorithm

#![allow(unused)]
fn main() {
use spindle_core::scalable::reason_scalable;

let result = reason_scalable(&theory);
let conclusions = result.to_conclusions(&indexed_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!");
}
}

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

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

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::ParseError;

fn load_theory(path: &str) -> Result<Theory> {
    let content = std::fs::read_to_string(path)?;

    if path.ends_with(".dfl") {
        parse_dfl(&content).map_err(|e| SpindleError::Parse(e.to_string()))
    } else if path.ends_with(".spl") {
        parse_spl(&content).map_err(|e| SpindleError::Parse(e.to_string()))
    } else {
        Err(SpindleError::Parse("Unknown format".to_string()))
    }
}
}

Advanced: Indexed Theory

For multiple queries, build an indexed theory once:

#![allow(unused)]
fn main() {
use spindle_core::index::IndexedTheory;

let indexed = IndexedTheory::build(theory.clone());

// O(1) lookups
for rule in indexed.rules_with_head(&literal) {
    // Process rules that conclude this literal
}

for rule in indexed.rules_with_body(&literal) {
    // Process rules that have this literal in body
}
}

Thread Safety

Theory and Conclusion are Send + Sync. You can:

#![allow(unused)]
fn main() {
use std::sync::Arc;
use rayon::prelude::*;

let theory = Arc::new(theory);

let results: Vec<_> = queries
    .par_iter()
    .map(|query| {
        let t = theory.clone();
        process_query(&t, query)
    })
    .collect();
}

Example: Complete Application

use spindle_core::prelude::*;
use spindle_parser::parse_dfl;
use std::fs;

fn main() -> Result<()> {
    // Load theory
    let content = fs::read_to_string("rules.dfl")?;
    let mut theory = parse_dfl(&content)?;

    // Add runtime facts
    theory.add_fact("current_user_admin");

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

    // Check permissions
    let can_delete = conclusions.iter().any(|c| {
        c.conclusion_type == ConclusionType::DefeasiblyProvable
            && c.literal.name() == "can_delete"
    });

    if can_delete {
        println!("User can delete");
    } else {
        println!("Permission denied");
    }

    Ok(())
}

WebAssembly Integration

Spindle compiles to WebAssembly for use in browsers and Node.js.

Building

Prerequisites

cargo install wasm-pack

Build for Web

cd crates/spindle-wasm
wasm-pack build --target web --release

Build for Node.js

wasm-pack build --target nodejs --release

Build for Bundlers (webpack, etc.)

wasm-pack build --target bundler --release

Installation

npm/yarn

npm install spindle-wasm
# or
yarn add spindle-wasm

From Local Build

// Point to your build output
import init, { Spindle } from './pkg/spindle_wasm.js';

Browser Usage

ES Modules

<script type="module">
import init, { Spindle } from './pkg/spindle_wasm.js';

async function main() {
    await init();

    const spindle = new Spindle();
    spindle.addFact("bird");
    spindle.addFact("penguin");
    spindle.addDefeasibleRule(["bird"], "flies");
    spindle.addDefeasibleRule(["penguin"], "~flies");
    spindle.addSuperiority("r2", "r1");

    const conclusions = spindle.reason();
    console.log(conclusions);
}

main();
</script>

With Bundler (Vite, webpack)

import init, { Spindle } from 'spindle-wasm';

async function setup() {
    await init();
    return new Spindle();
}

const spindle = await setup();

Node.js Usage

const { Spindle } = require('spindle-wasm');

const spindle = new Spindle();

spindle.parseDfl(`
    f1: >> bird
    f2: >> penguin
    r1: bird => flies
    r2: penguin => ~flies
    r2 > r1
`);

const conclusions = spindle.reason();
console.log(conclusions);

API Reference

Constructor

const spindle = new Spindle();

Creates a new empty theory.

Adding Facts

spindle.addFact("bird");
spindle.addFact("~guilty");  // Negated fact

Adding Rules

// Defeasible rules
spindle.addDefeasibleRule(["bird"], "flies");
spindle.addDefeasibleRule(["bird", "healthy"], "strong_flyer");

// Strict rules
spindle.addStrictRule(["penguin"], "bird");

// Defeaters
spindle.addDefeater(["broken_wing"], "flies");

Superiority

spindle.addSuperiority("r2", "r1");  // r2 > r1

Parsing

// Parse DFL
spindle.parseDfl(`
    f1: >> bird
    r1: bird => flies
`);

// Parse SPL
spindle.parseSpl(`
    (given bird)
    (normally r1 bird flies)
`);

Reasoning

const conclusions = spindle.reason();
// Returns: Array of conclusion objects

// Each conclusion:
{
    conclusion_type: "+D" | "-D" | "+d" | "-d",
    literal: string,
    positive: boolean
}

Scalable Reasoning

const conclusions = spindle.reasonScalable();

Query

// Check if a literal is provable
const result = spindle.query("flies");
// Returns: { status: "provable" | "not_provable", literal, conclusion_type }

What-If

const result = spindle.whatIf(["wounded"], "~flies");
// Returns: { provable: boolean, new_conclusions: Array }

Why-Not

const explanation = spindle.whyNot("flies");
// Returns: { literal, would_derive, blockers: Array }

Abduction

const solutions = spindle.abduce("goal", 3);
// Returns: { goal, solutions: Array<Array<string>> }

Reset

spindle.clear();  // Clear all rules and facts

TypeScript Types

interface Conclusion {
    conclusion_type: "+D" | "-D" | "+d" | "-d";
    literal: string;
    positive: boolean;
}

interface QueryResult {
    status: "provable" | "not_provable";
    literal: string;
    conclusion_type?: string;
}

interface WhatIfResult {
    provable: boolean;
    new_conclusions: Conclusion[];
}

interface WhyNotExplanation {
    literal: string;
    would_derive: string | null;
    blockers: Blocker[];
}

interface Blocker {
    rule: string;
    reason: string;
}

interface AbductionResult {
    goal: string;
    solutions: string[][];
}

Complete Example

import init, { Spindle } from 'spindle-wasm';

async function reasonAboutPenguins() {
    await init();

    const spindle = new Spindle();

    // Build theory
    spindle.parseDfl(`
        f1: >> bird
        f2: >> penguin

        r1: bird => flies
        r2: bird => has_feathers
        r3: penguin => ~flies
        r4: penguin => swims

        r3 > r1
    `);

    // Reason
    const conclusions = spindle.reason();

    // Filter positive conclusions
    const positive = conclusions.filter(c =>
        c.conclusion_type === "+D" || c.conclusion_type === "+d"
    );

    console.log("Provable:", positive.map(c => c.literal));

    // Query specific literal
    const fliesResult = spindle.query("flies");
    console.log("Does it fly?", fliesResult.status);

    // What-if analysis
    const whatIf = spindle.whatIf(["super_bird"], "flies");
    console.log("With super_bird:", whatIf.provable);

    // Explain why not
    if (fliesResult.status === "not_provable") {
        const explanation = spindle.whyNot("flies");
        console.log("Why not flies:", explanation.blockers);
    }
}

reasonAboutPenguins();

React Integration

import { useState, useEffect } from 'react';
import init, { Spindle } from 'spindle-wasm';

function useSpindle() {
    const [spindle, setSpindle] = useState<Spindle | null>(null);
    const [loading, setLoading] = useState(true);

    useEffect(() => {
        init().then(() => {
            setSpindle(new Spindle());
            setLoading(false);
        });
    }, []);

    return { spindle, loading };
}

function ReasoningComponent() {
    const { spindle, loading } = useSpindle();
    const [conclusions, setConclusions] = useState([]);

    const reason = () => {
        if (!spindle) return;

        spindle.reset();
        spindle.addFact("bird");
        spindle.addDefeasibleRule(["bird"], "flies");

        const result = spindle.reason();
        setConclusions(result);
    };

    if (loading) return <div>Loading WASM...</div>;

    return (
        <div>
            <button onClick={reason}>Reason</button>
            <ul>
                {conclusions.map((c, i) => (
                    <li key={i}>{c.conclusion_type} {c.literal}</li>
                ))}
            </ul>
        </div>
    );
}

Performance Notes

Initialize once: Call init() once at startup
Reuse Spindle instances: Create once, reset between uses
Batch operations: Add all rules before reasoning
Use scalable for large theories: reasonScalable() for >1000 rules

Bundle Size

Approximate sizes (gzipped):

Core WASM: ~150KB
JavaScript bindings: ~10KB

Browser Compatibility

Requires WebAssembly support:

Chrome 57+
Firefox 52+
Safari 11+
Edge 16+
Node.js 8+

Architecture

This document describes the internal architecture of Spindle-Rust.

Crate Structure

spindle-rust/
├── crates/
│   ├── spindle-core/     # Core reasoning engine
│   ├── spindle-parser/   # DFL and SPL parsers
│   ├── spindle-cli/      # Command-line interface
│   └── spindle-wasm/     # WebAssembly bindings

spindle-core

The core reasoning engine with these modules:

spindle-core/src/
├── lib.rs              # Crate root, prelude
├── intern.rs           # String interning
├── literal.rs          # Literal representation
├── mode.rs             # Modal operators
├── temporal.rs         # Temporal reasoning
├── rule.rs             # Rule types
├── superiority.rs      # Superiority relations
├── theory.rs           # Theory container
├── conclusion.rs       # Conclusion types
├── index.rs            # Theory indexing
├── reason.rs           # Standard DL(d) algorithm
├── scalable.rs         # Scalable DL(d||) algorithm
├── grounding.rs        # Variable grounding
├── worklist.rs         # Worklist data structures
├── explanation.rs      # Proof trees
├── trust.rs            # Trust-weighted reasoning
├── query.rs            # Query operators
└── error.rs            # Error types

Data Flow

Input (DFL/SPL)
      │
      ▼
┌─────────────┐
│   Parser    │  spindle-parser
└─────────────┘
      │
      ▼
┌─────────────┐
│   Theory    │  Rules, facts, superiority
└─────────────┘
      │
      ▼
┌─────────────┐
│  Grounding  │  Instantiate variables
└─────────────┘
      │
      ▼
┌─────────────┐
│   Index     │  Build lookup tables
└─────────────┘
      │
      ▼
┌─────────────┐
│  Reasoning  │  DL(d) or DL(d||)
└─────────────┘
      │
      ▼
┌─────────────┐
│ Conclusions │  +D, -D, +d, -d
└─────────────┘

Key Design Decisions

String Interning

All literal names are interned to reduce memory and enable O(1) comparisons.

#![allow(unused)]
fn main() {
// intern.rs
pub struct SymbolId(u32);   // Interned string ID
pub struct LiteralId(u32);  // Interned literal (name + negation)

// Convert string to ID (only allocates once per unique string)
let id = intern("bird");

// Compare IDs (O(1), no string comparison)
if id1 == id2 { ... }

// Resolve back to string when needed
let name = resolve(id);
}

Benefits:

HashSetLiteralId uses 4 bytes per entry vs ~24+ for String
No heap allocation in hot reasoning loops
O(1) equality checks

Indexed Theory

Rules are indexed by head and body literals for O(1) lookup.

#![allow(unused)]
fn main() {
// index.rs
pub struct IndexedTheory {
    theory: Theory,
    by_head: HashMap<LiteralId, Vec<&Rule>>,
    by_body: HashMap<LiteralId, Vec<&Rule>>,
}

// O(1) lookup instead of O(n) scan
indexed.rules_with_head(&literal)
indexed.rules_with_body(&literal)
}

LiteralId Design

A LiteralId packs symbol ID and negation into a single u32:

#![allow(unused)]
fn main() {
pub struct LiteralId(u32);

impl LiteralId {
    // High bit = negation flag
    // Lower 31 bits = symbol ID

    pub fn is_negated(&self) -> bool {
        (self.0 & 0x8000_0000) != 0
    }

    pub fn symbol(&self) -> SymbolId {
        SymbolId(self.0 & 0x7FFF_FFFF)
    }

    pub fn complement(&self) -> LiteralId {
        LiteralId(self.0 ^ 0x8000_0000)
    }
}
}

This allows:

O(1) negation check
O(1) complement computation
Efficient hash set storage

Superiority Index

Superiority relations are indexed for O(1) lookup:

#![allow(unused)]
fn main() {
pub struct SuperiorityIndex {
    // superior -> set of inferior rules
    superiors: HashMap<RuleLabel, HashSet<RuleLabel>>,
}

// O(1) check
theory.is_superior("r1", "r2")
}

Algorithm Implementation

Standard DL(d) (reason.rs)

Phase 1: Initialize with facts
  ├── Add to definite_proven
  ├── Add to defeasible_proven
  └── Add to worklist

Phase 2: Forward chaining
  while worklist not empty:
    ├── Pop literal
    ├── Find rules with literal in body
    ├── Decrement body counters
    └── If counter = 0:
        ├── Strict → add +D, +d
        ├── Defeasible → check blocking, add +d
        └── Defeater → (no conclusion)

Phase 3: Negative conclusions
  for each literal:
    ├── If not in definite_proven → -D
    └── If not in defeasible_proven → -d

Scalable DL(d||) (scalable.rs)

Phase 1: Delta Closure
  ├── Initialize with facts
  └── Forward chain strict rules only
  Result: +D conclusions

Phase 2: Lambda Closure
  ├── Start with delta
  ├── Add defeasible if:
  │   ├── Body in lambda
  │   └── Complement not in delta
  Result: Over-approximation of +d

Phase 3: Partial Closure (semi-naive)
  ├── Start with delta
  ├── Worklist of candidates from lambda
  └── For each candidate:
      ├── Check supporting rules
      ├── Check attacking rules
      ├── Check superiority
      └── Add if all attacks defeated
  Result: Actual +d conclusions

Memory Layout

Theory

#![allow(unused)]
fn main() {
pub struct Theory {
    rules: Vec<Rule>,
    superiorities: Vec<Superiority>,
    meta: HashMap<String, Meta>,
}

pub struct Rule {
    label: String,
    rule_type: RuleType,     // 1 byte + padding
    body: Vec<Literal>,
    head: Vec<Literal>,
}

pub struct Literal {
    name: String,            // 24 bytes (String)
    negation: bool,          // 1 byte + padding
    mode: Option<Mode>,      // 1-2 bytes + padding
    temporal: Option<...>,   // Variable
    predicates: Vec<String>, // 24 bytes (Vec)
}
}

Optimized Representation (reasoning)

#![allow(unused)]
fn main() {
// During reasoning, we use IDs instead of strings
proven: HashSet`LiteralId`  // 4 bytes per entry
worklist: VecDeque`LiteralId`
}

Extension Points

Adding a New Rule Type

Add variant to RuleType enum
Update parsers (dfl.rs, spl.rs)
Update reasoning logic (reason.rs, scalable.rs)
Add tests

Adding a New Query Operator

Add function to query.rs
Implement the algorithm
Add to WASM bindings if needed
Document in guides/queries.md

Adding Temporal Features

Extend temporal.rs
Update literal matching in grounding.rs
Update parsers for new syntax

Testing Strategy

tests/
├── Unit tests (per module)
│   ├── reason.rs - 40+ tests
│   ├── scalable.rs - 30+ tests
│   └── ...
├── Integration tests
│   └── Semantic equivalence (standard vs scalable)
├── Parser tests
│   ├── dfl.rs
│   └── spl.rs
└── WASM tests
    └── Basic functionality

Key Test Categories

Basic reasoning: facts, rules, chains
Conflict resolution: superiority, defeaters
Edge cases: cycles, empty, self-reference
Stress tests: long chains, wide theories
Semantic equivalence: standard ≡ scalable

Performance Characteristics

Operation	Complexity
Add fact	O(1) amortized
Add rule	O(1) amortized
Build index	O(n) where n = rules
Lookup by head	O(1)
Lookup by body	O(1)
Superiority check	O(1)
Standard reasoning	O(n * m)
Scalable reasoning	O(n * m) with better constants

Where:

n = number of rules
m = average body size

Dependencies

Core dependencies:

rustc-hash - Fast hash function for internal HashMaps

Parser dependencies:

nom - Parser combinator library

WASM dependencies:

wasm-bindgen - Rust/JavaScript interop
serde - JSON serialization

Optimization Notes

This document records optimization attempts and findings for future reference.

Lattice-Based Memoization (February 2026)

Motivation

The is_blocked_by_superior function in reason.rs checks if a defeasible rule is blocked by attacking rules. The hypothesis was that:

Multiple rules deriving the same head would check the same attackers
Caching attacker status could avoid repeated O(body_size) checks
A lattice-based approach (inspired by Ascent) could formalize memoization

Approaches Tried

1. ProofStatus Lattice with Memoization

Created a ProofStatus enum representing lattice positions:

#![allow(unused)]
fn main() {
enum ProofStatus {
    Unknown,           // ⊥
    BlockedByDelta,    // Terminal false
    NotInLambda,       // Terminal false
    NoSupport,         // Pending
    HasSupport,        // Pending
    AllAttacksDefeated,// Ready to prove
    ProvedInPartial,   // ⊤
}
}

Result: Correct semantically, but added 5-15% overhead due to HashMap operations.

#![allow(unused)]
fn main() {
struct LazyAttackerTracker {
    attacker_remaining: FxHashMap<String, usize>,
    active_attackers: FxHashMap<LiteralId, Vec<String>>,
    attacker_heads: FxHashMap<String, LiteralId>,
}
}

Result: 10-80% slower due to HashMap operations and string allocations.

Benchmark Results

multi_target_blocked (M targets × N defenders):
  5x10:   standard ~44µs,  lazy ~53µs (+20%),  memoized ~51µs (+16%)
  10x10:  standard ~88µs,  lazy ~100µs (+14%), memoized ~106µs (+20%)
  20x10:  standard ~164µs, lazy ~299µs (+82%), memoized ~228µs (+39%)
  10x20:  standard ~180µs, lazy ~215µs (+19%), memoized ~230µs (+28%)

Why All Approaches Failed

The original is_blocked_by_superior is already well-optimized:

#![allow(unused)]
fn main() {
for attacker in attacking_rules {           // O(1) lookup via IndexedTheory
    let satisfied = attacker.body.iter()    // Small vector (~1-3 elements)
        .all(|b| proven.contains(&b));      // O(1) HashSet lookup
    // Superiority check is O(1) via SuperiorityIndex
}
}

Key factors:

Operation is already cheap - Small vectors, O(1) lookups
Single-pass algorithm - Each literal checked once, no reuse opportunity
Cache overhead exceeds savings - HashMap ops, allocations, tracking state

When Memoization Would Help

Scenario	Single-Pass	Would Benefit
Batch reasoning	❌ No reuse	N/A
Interactive queries	N/A	✅ Repeated queries
Incremental reasoning	❌ Rebuild	✅ Cache across runs
Explanation generation	N/A	✅ Re-queries same literals
What-if analysis	❌ Fresh run	✅ Partial cache hits

Existing Optimizations (Already Effective)

LiteralId - 4-byte interned identifier, O(1) comparison
SuperiorityIndex - O(1) superiority lookup
IndexedTheory - O(1) rule lookup by head/body
HashSet - 4 bytes per entry vs ~24 for String

Alternative Optimizations (Not Tried)

If future profiling shows is_blocked_by_superior as a bottleneck:

Bit vectors - Replace HashSet with bit vector for proven literals
Arena allocation - Pre-allocate rules in contiguous memory
Rule ordering - Process rules in topological order
SIMD body checks - Vectorize body satisfaction for large bodies

Lessons Learned

Profile before optimizing - The target operation was already efficient
Single-pass algorithms resist caching - No repeated queries means no cache hits
Cache overhead matters - HashMap operations can exceed saved computation
Simple code is often fastest - Direct iteration beats fancy data structures

Code Location

The experimental code is on branch feature/lattice-proof-memoization:

8af967a feat(lattice): add lattice-based proof status memoization
9dd60e0 feat(lattice): add BlockedByChecker for is_blocked_by_superior
33e9923 perf(lattice): implement incremental cache invalidation
241d5e9 bench: add memoization comparison benchmarks
270aa98 experiment: add reason_lazy with lazy attacker tracking

The lattice module (lattice.rs) and memoized/lazy functions remain available for reference but are not used in production.

Keyboard shortcuts

Spindle-Rust