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