CLI Reference

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

Installation

cargo install --path crates/spindle-cli

Synopsis

spindle <COMMAND> [OPTIONS]
spindle reason [OPTIONS] [FILE]
spindle query <LITERAL> [FILE] [OPTIONS]
spindle explain <LITERAL> [FILE] [OPTIONS]
spindle why-not <LITERAL> [FILE] [OPTIONS]
spindle requires <LITERAL> [FILE] [OPTIONS]
spindle vocabulary [FILE] [OPTIONS]
spindle what-if <LITERAL> [FILE] --given <LITERAL> [OPTIONS]
spindle abduce <LITERAL> [FILE] [OPTIONS]
spindle capabilities [OPTIONS]
spindle explain-code <CODE>

Commands

reason

reason performs defeasible reasoning on a theory.

spindle reason examples/penguin.spl

Text output shows a Proved: list of positive literals in canonical SPL syntax, with each exact literal listed once. Facts therefore do not appear twice for +D and +d. Negation and distinct temporal windows are preserved. If no positive conclusion is proved, the command says so; this does not mean every literal is refuted. For distinctions between numeric types, use --json --v2: text can render distinct typed values such as integer 1 and float 1e0 alike.

--detailed

Show all four proof tags, including constructive refutations and implicit modal opponents. Literals still use SPL syntax, such as +d (may (play)).

spindle reason --detailed examples/penguin.spl

--detailed affects text presentation only. JSON v1/v2 retain their existing fields and full conclusion lists, including both +D and +d for a fact. Standard literal_struct.mode.name values use the SPL words must, may, and forbidden; custom names are preserved and no mode is null. mode.negation remains outer negation, while literal_struct.negated is inner negation. Consumers matching the former O/P/F names must update.

--v2

--v2 selects JSON schema version v2 (spindle.reason.v2) for the JSON output envelope. The v2 schema includes typed term arguments in the literal_struct fields, giving downstream consumers richer structure than the v1 flat-string representation.

spindle reason examples/penguin.spl --json --v2

Without --v2, the default schema is spindle.reason.v1.

--trust

--trust includes trust-weight annotations on each conclusion. In JSON, each conclusion carries a trust_degree (0.0--1.0), a trust_sources list when present, and trust_details containing ordered diminished_by challenges and named above_threshold results. Both JSON versions expose these fields.

spindle reason examples/penguin.spl --json --trust

validate

validate checks syntax without reasoning.

spindle validate examples/penguin.spl
spindle --json validate --stdin < examples/penguin.spl

Output on success:

Valid theory file

With --json success output:

{
  "valid": true,
  "diagnostics": []
}

Output on error:

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

stats

stats shows theory statistics.

spindle stats examples/penguin.spl
spindle --json stats --stdin < examples/penguin.spl

Output:

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

With --json success output:

{
  "stats": {
    "total_rules": 8,
    "facts": 2,
    "strict": 1,
    "defeasible": 4,
    "defeaters": 1,
    "superiorities": 1
  },
  "diagnostics": []
}

query

query reports whether a literal holds in the theory.

spindle query flies examples/penguin.spl
spindle query "~flies" examples/penguin.spl
spindle query "(not flies)" examples/penguin.spl
spindle query flies examples/penguin.spl --json

The literal argument supports multiple formats: p, ~p, (not p), or complex SPL expressions.

Returns a QueryStatus:

Output:

QueryStatus: Provable

With --json:

{"literal":"flies","status":"Refuted"}

explain

explain shows the derivation proof tree for a literal.

spindle explain "-flies" examples/penguin.spl
spindle explain "-flies" examples/penguin.spl --json

Shows the proof tree detailing how the reasoning engine derived the conclusion.

Output:

Explanation for -flies:
  -flies ← [defeasible] r3: penguin -> -flies
    penguin ← [fact]
  Blocked alternatives:
    r1: bird -> flies (defeated by r3 via superiority)
  Conflict resolutions:
    r3 > r1 (superiority)

With --json, the output is a JSON or JSON-LD structure containing an Explanation with proof nodes, blocked alternatives, and conflict resolutions.

why-not

why-not explains why a literal is not provable.

spindle why-not flies examples/penguin.spl
spindle why-not flies examples/penguin.spl --json

Lists the blocking rules and the reasons they prevent the literal from being derived. Useful for debugging unexpected results. When the literal is provable, the JSON output includes is_provable: true and blocked_by will be empty.

Output:

Why not flies?
  Rule r1: bird -> flies
    Status: Defeated
    Defeated by: r3 (penguin -> -flies) via superiority r3 > r1

Possible blocking reasons:

requires

requires finds minimal sets of facts needed to derive a literal through abduction.

spindle requires flies examples/penguin.spl
spindle requires flies examples/penguin.spl --max 5
spindle requires flies examples/penguin.spl --json

The --max option limits the number of solutions returned (defaults to 10).

As of the v2 contract (IMPL-011), requires verifies all candidate solutions by default. The reasoning engine checks each candidate set of facts to verify that it makes the goal provable. The JSON output includes verification_mode: "verified" and a verification object with raw_examined, accepted, and rejected counts. Only accepted solutions appear in the solutions array. The JSON envelope uses schema spindle.requires.v2.

Output:

Verified requirements for flies:
  1. Add facts: {bird, -penguin}
  2. Add facts: {flies}

Each result is a minimal, verified set of assumptions. Adding those assumptions to the theory makes the literal provable.

capabilities

capabilities lists the commands, features, and JSON schema versions this Spindle build supports. Useful for tooling that needs to discover available functionality at runtime.

spindle capabilities
spindle capabilities --json

Output:

Spindle Capabilities:

Commands: reason, query, requires, explain, why-not, vocabulary, what-if, abduce, validate, stats, capabilities, explain-code

Features:
  --stdin: yes
  --at: yes
  --json: yes
  --v2: yes
  --trust (including diminishment and thresholds): yes
  --extensions: yes
  Trust overlay: no
  Given flags: no

Schema versions:
  reason: spindle.reason.v1
  reason_v2: spindle.reason.v2
  vocabulary: spindle.vocabulary/1
  query: spindle.query.v1
  requires: spindle.requires.v2
  explain: spindle.explain.v1
  why-not: spindle.why_not.v1

With --json, the output is a JSON object with schema spindle.capabilities.v1 containing commands, features, and schemas fields.

explain-code

explain-code reports the meaning and common causes of a stable error code.

spindle explain-code RULE_NOT_FOUND
spindle explain-code SPL_PARSE_ERROR

This command does not accept --json; output is always human-readable text. It provides guidance for unfamiliar error codes in JSON error envelopes.

JSON Envelope Schema Versions

Reasoning and diagnostic envelopes use schema_version. Vocabulary uses schema; what-if and raw abduction use the corresponding WASM result shapes. The following schema versions are defined:

Options

--json

--json outputs results in JSON format, including for validate and stats. The explain-code command does not accept this option. When --json is present, success and failure paths are machine-readable JSON.

spindle reason examples/penguin.spl --json
spindle query flies examples/penguin.spl --json
spindle explain "-flies" examples/penguin.spl --json
spindle --json validate --stdin < examples/penguin.spl

Parse/usage failures also emit JSON envelopes when --json is present:

spindle --json

--at <TIME>

--at sets the reference time for temporal ("as-of") reasoning. The value MUST be an ISO 8601 / RFC 3339 timestamp.

spindle reason --at 2024-06-15T12:00:00Z examples/temporal.spl
spindle query p --at 2024-06-15T12:00:00Z examples/temporal.spl

--stdin

--stdin reads the theory from standard input instead of a file. Mutually exclusive with providing a file path.

cat examples/penguin.spl | spindle reason --stdin
spindle --json validate --stdin < examples/penguin.spl

--positive

--positive filters detailed text or JSON to positive proof tags (+D, +d). The default concise text view already shows only proved literals.

spindle reason --detailed --positive examples/penguin.spl
spindle reason --json --positive examples/penguin.spl

An explicit negative literal, such as (not (flies)), can be positively proved; --positive retains it. The option filters proof tags, not literal negation.

--debug-errors

--debug-errors shows full error details including source chains and unredacted file paths. Useful for diagnosing unexpected failures.

spindle reason examples/penguin.spl --debug-errors

File Format Detection

The CLI auto-detects format by extension:

Exit Codes

Examples

Basic Reasoning

# Reason about a theory
spindle reason penguin.spl

Querying and Explaining

# Check if a literal holds
spindle query flies penguin.spl

# Get a proof tree for a derived conclusion
spindle explain "-flies" penguin.spl

# Debug why something is not provable
spindle why-not flies penguin.spl

# Find what facts would make a literal provable
spindle requires flies penguin.spl --max 5

# Get JSON output for scripting
spindle query flies penguin.spl --json

Validate Before Reasoning

spindle validate theory.spl && spindle reason theory.spl

Compare Runs

# Compare two revisions or theories
spindle reason theory-a.spl > run-a.txt
spindle reason theory-b.spl > run-b.txt
diff run-a.txt run-b.txt

Scripting

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

Environment Variables

SPINDLE_LOG=debug spindle reason theory.spl

Aggregate programs and query matching

spindle reason examples/aggregation.spl --json --v2
spindle query '(total-payment alice 20)' examples/aggregation.spl

Aggregation uses the normal reason and query commands without an extra flag. The CLI supplies the builtin function prelude. Use --extensions for portable lookup functions and named aggregators; arbitrary function implementations are available through the Rust embedding API.

Bounded temporal goals match identical windows, including in requires. A containing window is not an exact match. Atemporal goals match any family member. See Query Operators.

Vocabulary and hypothetical queries

spindle vocabulary theory.spl --json returns spindle.vocabulary/1: structural predicate symbols (functor/arity), declarations, profiles, provenance and shape or declaration diagnostics. It inspects the original theory without grounding.

spindle what-if '(q 2)' theory.spl --given '(p 2)' --json evaluates hypothetical facts without modifying the file. Repeat --given for multiple facts. Its output contains provable, new_conclusions, new_conclusions_struct (typed literals), and changed_conclusions. Facts are added before grounding.

spindle abduce q theory.spl --max 10 --json returns raw candidates with facts (display strings), facts_struct (typed literals), rules_used and confidence. Use requires when candidates must be verified. Both commands accept --at and --extensions.

Query literals use SPL, including typed arguments, modal forms and temporal windows. Legacy comma notation such as p(2) is also accepted. Invalid input now reports INVALID_LITERAL instead of silently treating it as an atom.

Portable extensions

Both CLI and WASM accept a spindle.extensions.v1 JSON document. The CLI's global --extensions FILE option loads it; WASM uses registerExtensions(jsonString). Registrations supply finite pure lookup functions and named integer aggregators.

{
  "schema_version": "spindle.extensions.v1",
  "functions": [{
    "name": "classification",
    "arguments": ["integer"],
    "returns": "symbol",
    "rows": [{
      "args": [{"type": "integer", "value": 2}],
      "result": {"type": "symbol", "value": "small"}
    }]
  }],
  "aggregators": [{"name": "total", "reducer": "+", "identity": 0}]
}

Supported declared types are symbol, integer, decimal, and float, with values encoded using the typed term format. Decimal values are strings; integers outside JavaScript's exact range should be strings. Matching is type-sensitive. Names cannot replace builtins; duplicate names/keys, invalid terms, and signature mismatches are rejected. Missing lookup rows return evaluation failure; ordinary grounding discards that candidate binding.

An aggregator names a binary reducer, an optional integer identity (null means empty input fails the premise), and optional count: true. Custom reducers must be associative and commutative and return integers for every intermediate value. The ordinary aggregate restrictions remain in force.

spindle reason examples/lookup-functions.spl \
  --extensions examples/lookup-functions.json --json --v2

The same registry is used by reason, query, explain, why-not, requires, what-if, and abduce. This portable format does not execute arbitrary host code; Rust embedding retains the unrestricted pure-function registration API.