Spindle-Rust

A Rust implementation of the SPINdle defeasible logic reasoning engine.

This project is part of the SPINdle family:

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

Features

• Defeasible Logic Reasoning: Implements non-monotonic reasoning with four rule types:

  • Facts (>>) - Unconditional truths
  • Strict rules (->) - Must hold if antecedent is true
  • Defeasible rules (=>) - Normally hold unless defeated
  • Defeaters (~>) - Block conclusions without proving anything

• Reasoning Mode:

  • Standard DL(d) - Traditional forward chaining

• Temporal Reasoning: Allen interval algebra with 13 temporal relations

• Superiority Relations: Conflict resolution via rule preferences

• First-Order Variables: Datalog-style grounding with ?x variable syntax

• Arithmetic Expressions: Numeric computation in rule bodies

  • Operators: +, -, *, /, div, rem, **, abs, min, max
  • Variable binding: (bind ?total (+ ?price ?tax))
  • Comparison guards: (> ?age 18), (<= ?score 100)
  • Three numeric types: Integer, Decimal (arbitrary-precision), Float
  • Cross-type matching: Integer(2) equals Decimal(2.0) equals Float(2.0)

• Predicate Model & Vocabulary: Structural predicate identity independent of reasoning

  • First-class declarations: (predicate assign-to ((task symbol) (agent symbol)))
  • Structured metadata targets: (meta (predicate assign-to 2) (description "..."))
  • Derived, deterministic theory signatures and vocabularies (signatures, argument profiles, provenance)
  • Non-semantic shape validation — never changes conclusions

• Input Format:

  • SPL (Spindle Lisp) - Lisp-based DSL

• Explanations: Proof trees with natural language and JSON output

• Trust-Aware Reasoning: Source attribution and trust-weighted conclusions

• Query Operators:

  • What-if: Hypothetical reasoning
  • Why-not: Explanation of failures
  • Abduction: Finding hypotheses to prove goals

• WebAssembly Support: Run in browsers and Node.js via wasm-bindgen

Installation

cargo install --path crates/spindle-cli

Versioning Policy

This project is currently pre-1.0 and follows strict Semantic Versioning for 0.y.z releases:

• Breaking changes bump y (for example, 0.1.3 -> 0.2.0)
• Backward-compatible changes and fixes bump z (for example, 0.1.3 -> 0.1.4)
• 1.0.0 will be used once API stability guarantees are in place

Usage

# Reason about a theory (SPL format)
spindle examples/penguin.spl

# Show only positive conclusions
spindle --positive examples/penguin.spl

# Validate a theory file
spindle validate examples/penguin.spl

# Show statistics
spindle stats examples/penguin.spl

SPL Format

; Facts
(given bird)
(given penguin)

; Defeasible rules
(normally r1 bird flies)
(normally r2 penguin (not flies))

; Superiority
(prefer r2 r1)

; Predicates with variables
(given (parent alice bob))
(normally r3 (parent ?x ?y) (ancestor ?x ?y))

; Predicate declaration + structured metadata target (optional)
(predicate ancestor ((descendant symbol) (forebear symbol)))
(meta (predicate ancestor 2) (description "Transitive parent relation."))

; Arithmetic: bind and compare
(given (item widget 25))
(given (tax-rate 0.1))
(normally r4
  (and (item ?name ?price) (tax-rate ?rate)
       (bind ?total (+ ?price (* ?price ?rate))))
  (total-cost ?name ?total))
(normally r5
  (and (total-cost ?name ?t) (> ?t 20))
  (expensive ?name))

Library Usage

use spindle_core::prelude::*;

let mut theory = Theory::new();

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

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

// Superiority: penguins override birds
theory.add_superiority(&r2, &r1);

// Reason
use spindle_core::reason::reason;
let conclusions = reason(&theory);

WebAssembly Usage

Build the WASM package:

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

Use in JavaScript/TypeScript:

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

await init();

const spindle = new Spindle();

// Add theory programmatically
spindle.addFact("bird");
spindle.addFact("penguin");
spindle.addDefeasibleRule(["bird"], "flies");
spindle.addDefeasibleRule(["penguin"], "~flies");
spindle.addSuperiority("r2", "r1");

// Or parse SPL
spindle.parseSpl(`
  (given bird)
  (given penguin)
  (normally r1 bird flies)
  (normally r2 penguin (not flies))
  (prefer r2 r1)
`);

// Reason
const conclusions = spindle.reason();
// => [{conclusion_type: "+D", literal: "bird", positive: true}, ...]

// Query
const result = spindle.query("~flies");
// => {status: "provable", literal: "~flies", conclusion_type: "+d"}

// What-if hypothetical reasoning
const whatIf = spindle.whatIf(["wounded"], "~flies");
// => {provable: true, new_conclusions: [...]}

// Why-not failure explanation
const whyNot = spindle.whyNot("flies");
// => {literal: "flies", would_derive: "r1", blockers: [...]}

// Abduction
const abduce = spindle.abduce("flies", 3);
// => {goal: "flies", solutions: [[...], [...]]}

Crate Structure

• spindle-core - Core reasoning engine
  • reason/ - Standard DL(d) forward chaining with Reasoner trait
  • pipeline/ - Composable PipelineStage stages (validate, temporal, wildcard, ground)
  • query/ - Query operators with QueryOperator trait (what-if, why-not, abduction)
  • explanation/ - Proof trees with ExplanationFormatter trait (natural language, JSON, JSON-LD, DOT)
  • analysis/ - Theory analysis (conflicts, validation, superiority suggestions)
  • arith - Arithmetic expression AST, evaluation, and type promotion
  • body - Body literals with arithmetic constraints (BodyLiteral, BodyArg)
  • term - Typed term values (Symbol, Integer, Decimal, Float)
  • temporal - Allen interval algebra
  • grounding - Datalog-style variable grounding with arithmetic evaluation
  • trust - Trust-weighted reasoning
• spindle-parser - SPL format parser
  • spl/ - Lexer, expression dispatch, literal/rule/metadata handlers
  • spl/arith - Arithmetic expression and constraint parsing
• spindle-cli - Command-line interface
• spindle-wasm - WebAssembly bindings for JavaScript/TypeScript

Testing

1,500+ tests covering:

• Core reasoning (facts, rules, conflicts, superiority)
• Arithmetic expressions, type promotion, and numeric evaluation
• Edge cases (cycles, empty theories, defeaters)
• Stress tests (long chains, wide theories)
• Query operators (what-if, why-not, abduction)
• Property-based tests (proptest)
• Pipeline integration tests
• Regression tests for known bugs
• Golden explanation tests

cargo test

Documentation

Full documentation is available at docs/ or build locally:

cd docs && mdbook serve

References

• SPINdle Project - Original Java implementation by NICTA/Data61
• Nute, D. (1994). "Defeasible Logic" - Foundational paper
• spindle-racket - Racket implementation

License

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