Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

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

ConclusionMeaning
+D birdbird is definitely provable (it’s a fact)
+d birdbird is defeasibly provable
+d fliesflies is defeasibly provable via r1
-D fliesflies 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