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)