Explanation API and Output Formats

Spindle’s explanation system exposes the derivation path of defeasible reasoning conclusions. It records rejected alternatives and resolved conflicts alongside proof trees.

Explanation Coverage

Defeasible reasoning involves rules that can be overridden, conflicts between competing conclusions, and subtle interactions between superiority relations. A bare conclusion like +d ~flies tells you the result but not the story. The explanation system answers questions such as:

• Which rules fired to produce this conclusion?
• Were there competing rules that were defeated?
• How were conflicts resolved -- by superiority, definite priority, or team defeat?
• What is the full derivation chain from facts to conclusion?

These records support decision justification in legal reasoning, medical diagnosis, and access control.

Proof Trees

Structure

An explanation contains a proof tree. This recursive structure traces a literal’s derivation back to its supporting facts and rules.

The core types are:

• ProofNode -- represents the derivation of a single literal, containing:

  • literal -- the derived literal
  • derivation_type -- Definite (strict rules and facts only) or Defeasible (defeasible rules involved)
  • proof_step -- the rule application that produced this literal
  • blocked_alternatives -- alternative derivations the reasoner considered but rejected
  • conflicts_resolved -- conflict resolutions that occurred at this node

• ProofStep -- represents one application of a rule, containing:

  • rule_label -- the applied rule
  • rule_type -- Fact, Strict, Defeasible, or Defeater
  • rule_text -- string representation of the rule
  • body_proofs -- recursive ProofNode entries for each body literal
  • annotations -- metadata attached to the rule

• DerivationType -- either Definite or Defeasible

Navigating Proof Trees

A proof tree reads from conclusion down to facts. Each node’s proof_step identifies the applied rule. Its body_proofs contain the sub-trees for each premise.

For example, a theory contains the fact penguin, strict rule (always s1 penguin bird), and defeasible rule (normally r1 bird flies). Its proof tree for flies has this structure:

flies [defeasible, r1: bird -> flies]
  bird [definite, s1: penguin -> bird]
    penguin [definite, f1: penguin]

Each level corresponds to a ProofNode whose proof_step.body_proofs contains the children.

Blocked Alternatives and Conflict Resolutions

Blocked Alternatives

Some candidate rules for a literal or its complement face blockers. A BlockedProof records:

• literal -- what the blocked rule tried to prove
• rule_label -- the label of the blocked rule
• reason -- a BlockReason enum value:
  • Superiority -- blocked by a superior rule
  • Defeater -- blocked by a defeater
  • Conflict -- blocked due to an unresolved conflict
  • BodyUnprovable -- the rule’s body is unsatisfied
• blocking_rule -- the label of the rule that caused the blocking (if applicable)
• explanation -- a human-readable description

Conflict Resolutions

Rules deriving contradictory conclusions create a conflict. A ConflictResolution records:

• winning_rule -- the rule that prevailed
• losing_rule -- the defeated rule
• resolution_type -- a ResolutionType enum value:
  • Superiority -- resolved by an explicit superiority relation
  • DefinitePriority -- resolved because strict rules override defeasible ones
  • TeamDefeat -- resolved by team defeat (a group of rules collectively defeats the attacker)

Together, blocked alternatives and conflict resolutions provide a complete picture of why one derivation was chosen over another.

Output Formats

The Explanation type supports four output formats, each suited to different use cases.

Natural Language

#![allow(unused)]
fn main() {
let text = explanation.to_natural_language();
println!("{}", text);
}

Produces human-readable output with headers, indented proof trees, and numbered lists:

Explanation for +d ~flies
This was proven using defeasible rules and was not defeated by any conflicting rule.

Derivation:
  1. "~flies" was derived defeasibly
     Using defeasible rule: r2
     Prerequisites:
       1. "penguin" was established as a fact
          Using fact: f1

Blocked Alternatives:
  1. Rule 'r1' was blocked due to superiority: r2 is superior and concludes ~flies

Conflict Resolutions:
  1. 'r2' defeated 'r1' via superiority

The output includes description and source annotations when proof steps contain them.

JSON

#![allow(unused)]
fn main() {
let json = explanation.to_json();
}

Produces a structured JSON value with nested proof trees:

{
  "conclusion_type": "+d",
  "literal": "~flies",
  "proof_tree": {
    "literal": "~flies",
    "derivation_type": "defeasible",
    "proof_step": {
      "rule_label": "r2",
      "rule_type": "defeasible",
      "rule_text": "penguin -> ~flies",
      "body_proofs": [
        {
          "literal": "penguin",
          "derivation_type": "definite",
          "proof_step": {
            "rule_label": "f1",
            "rule_type": "fact",
            "rule_text": "penguin",
            "body_proofs": []
          }
        }
      ]
    }
  },
  "blocked_alternatives": [
    {
      "literal": "flies",
      "rule_label": "r1",
      "reason": "superiority",
      "blocking_rule": "r2",
      "explanation": "r2 is superior and concludes ~flies"
    }
  ],
  "conflicts_resolved": [
    {
      "winning_rule": "r2",
      "losing_rule": "r1",
      "resolution_type": "superiority",
      "superiority_label": "sup1"
    }
  ]
}

JSON-LD

#![allow(unused)]
fn main() {
let jsonld = explanation.to_jsonld();
}

Produces a JSON-LD document with semantic annotations for integration with linked data systems. The output includes:

• @context defining vocabulary prefixes:
  • spindle -- https://spindle.dev/ontology#
  • prov -- http://www.w3.org/ns/prov#
  • rdfs -- http://www.w3.org/2000/01/rdf-schema#
  • xsd -- http://www.w3.org/2001/XMLSchema#
• @type: "spindle:Explanation" on the root document
• @type: "spindle:ProofNode" on proof nodes
• @type: "spindle:ProofStep" on proof steps
• @type: "spindle:BlockedProof" on blocked alternatives
• @type: "spindle:ConflictResolution" on conflict resolutions

The JSON-LD serializer maps rule metadata provenance annotations to standard vocabularies:

• source / prov:wasAttributedTo for attribution
• description / rdfs:comment for descriptions
• confidence / spindle:confidence for trust scores
• @id for linked data identifiers

Graphviz DOT

#![allow(unused)]
fn main() {
let dot = explanation.to_dot();
}

Produces a DOT language graph for visual rendering. The color scheme encodes derivation semantics:

The graph uses bottom-to-top layout (rankdir=BT), so facts appear at the bottom and conclusions at the top. Edge labels identify rules.

Annotations and Metadata

The Annotations Type

Annotations is a metadata container with two fields:

• id -- a URI identifier, when present (@id in JSON-LD)
• entries -- a HashMap<String, String> of key-value pairs

Standard Vocabulary Keys

The annotation system recognizes standard vocabulary keys and provides convenience accessors that check multiple equivalent keys:

You can also use get(key) for any arbitrary key, or get_any(keys) to check a list of fallback keys.

Creating Annotations

#![allow(unused)]
fn main() {
use spindle_core::explanation::Annotations;

// Empty annotations
let annots = Annotations::new();

// With entries
let annots = Annotations::with_entries(vec![
    ("description", "Birds typically fly"),
    ("source", "ornithology-textbook"),
    ("confidence", "0.95"),
]);

// With a linked data identifier
let mut annots = Annotations::with_entries(vec![
    ("source", "legal-statute-42-usc-1983"),
]);
annots.id = Some("https://example.org/rules/r1".to_string());
}

Attaching Annotations to Proof Steps

#![allow(unused)]
fn main() {
use spindle_core::explanation::{ProofStep, Annotations};
use spindle_core::rule::RuleType;

let annots = Annotations::with_entries(vec![
    ("source", "expert-knowledge"),
    ("description", "Standard medical practice guideline"),
    ("confidence", "0.85"),
]);

let step = ProofStep::new("med_rule", RuleType::Defeasible, "symptom -> diagnosis")
    .with_annotations(annots);
}

All output formats preserve annotations. Natural-language output prints description and source inline. JSON-LD maps description, source, and confidence to rdfs:comment, prov:wasAttributedTo, and spindle:confidence, respectively.

CLI Usage

The explain Command

explain returns the full derivation proof tree for a provable literal:

spindle explain "~flies" theory.spl

Output includes the derivation chain, blocked alternatives, and conflict resolutions in natural language format.

For machine-readable output:

spindle explain "~flies" theory.spl --json

The why-not Command

why-not reports why a literal is not provable:

spindle why-not flies theory.spl

The output lists candidate derivation rules and their blockers. Blockers include missing premises, defeat by a stronger rule, and contradiction by a strict derivation.

For machine-readable output:

spindle why-not flies theory.spl --json

The JSON output includes is_provable to indicate whether the literal is actually provable, and would_derive with the rule label when available.

The conclusion debugging guide combines these commands to diagnose unexpected results.

Rust API Examples

Generating an Explanation

#![allow(unused)]
fn main() {
use spindle_core::explanation::explain;
use spindle_core::literal::Literal;
use spindle_core::theory::Theory;

let mut theory = Theory::new();
theory.add_fact("bird");
theory.add_defeasible_rule(&["bird"], "flies");

let literal = Literal::simple("flies");
if let Some(explanation) = explain(&theory, &literal) {
    // Natural language output
    println!("{}", explanation.to_natural_language());

    // Structured JSON
    let json = explanation.to_json();
    println!("{}", serde_json::to_string_pretty(&json).unwrap());

    // JSON-LD for semantic web
    let jsonld = explanation.to_jsonld();

    // Graphviz DOT for visualization
    let dot = explanation.to_dot();
}
}

The explain function returns None if the literal is not positively provable in the theory.

Building Explanations Manually

For custom explanation construction (useful in testing or when building explanations outside the standard reasoning pipeline):

#![allow(unused)]
fn main() {
use spindle_core::explanation::*;
use spindle_core::conclusion::ConclusionType;
use spindle_core::literal::Literal;
use spindle_core::rule::RuleType;

// Build a proof tree bottom-up
let fact_step = ProofStep::new("f1", RuleType::Fact, "penguin");
let fact_node = ProofNode::new(Literal::simple("penguin"), DerivationType::Definite)
    .with_proof_step(fact_step);

let rule_step = ProofStep::new("r2", RuleType::Defeasible, "penguin -> ~flies")
    .with_body_proofs(vec![fact_node]);
let conclusion_node = ProofNode::new(Literal::negated("flies"), DerivationType::Defeasible)
    .with_proof_step(rule_step);

// Record a blocked alternative
let blocked = BlockedProof::new(
    Literal::simple("flies"),
    "r1",
    BlockReason::Superiority,
    "Rule r2 is superior and concludes ~flies",
).with_blocking_rule("r2");

// Record a conflict resolution
let conflict = ConflictResolution::new("r2", "r1", ResolutionType::Superiority)
    .with_superiority("sup1");

// Assemble the explanation
let explanation = Explanation::new(
    ConclusionType::DefeasiblyProvable,
    Literal::negated("flies"),
)
.with_proof(conclusion_node)
.with_blocked(vec![blocked])
.with_conflicts(vec![conflict]);
}

Inspecting Proof Trees Programmatically

#![allow(unused)]
fn main() {
fn walk_proof(node: &ProofNode, depth: usize) {
    let indent = "  ".repeat(depth);
    let dtype = match node.derivation_type {
        DerivationType::Definite => "definite",
        DerivationType::Defeasible => "defeasible",
    };
    println!("{}{} [{}]", indent, node.literal, dtype);

    if let Some(ref step) = node.proof_step {
        println!("{}  via rule: {}", indent, step.rule_label);

        if let Some(desc) = step.annotations.description() {
            println!("{}  description: {}", indent, desc);
        }

        for child in &step.body_proofs {
            walk_proof(child, depth + 1);
        }
    }
}

if let Some(ref tree) = explanation.proof_tree {
    walk_proof(tree, 0);
}
}

Use Case: Visual Proof Graphs with DOT Output

The DOT output format integrates directly with Graphviz for generating visual proof graphs.

Generating a Graph

# Generate DOT and render to PNG
spindle explain "~flies" theory.spl --json \
  | jq -r '.proof_tree' \
  > /dev/null  # Use the Rust API instead for DOT

# Or from Rust:

#![allow(unused)]
fn main() {
use spindle_core::explanation::explain;
use spindle_core::literal::Literal;
use std::fs;
use std::process::Command;

let literal = Literal::negated("flies");
if let Some(explanation) = explain(&theory, &literal) {
    let dot = explanation.to_dot();

    // Write DOT file
    fs::write("proof.dot", &dot).unwrap();

    // Render with Graphviz
    Command::new("dot")
        .args(["-Tpng", "proof.dot", "-o", "proof.png"])
        .status()
        .unwrap();

    // Or render to SVG for web embedding
    Command::new("dot")
        .args(["-Tsvg", "proof.dot", "-o", "proof.svg"])
        .status()
        .unwrap();
}
}

Reading the Graph

The generated graph uses a consistent visual language:

• Blue boxes at the bottom represent facts and strict derivations. These are the foundation of the proof and cannot be defeated.
• Green boxes represent defeasible derivations. New information can override these conclusions.
• Red dashed boxes in the "Blocked Alternatives" cluster show derivations that were considered but rejected. The label includes the rule label and the reason for blocking.
• Orange diamonds in the "Conflict Resolutions" cluster show how conflicts between competing rules were resolved, including the winning and losing rules and the resolution mechanism.

Edges flow upward from premises to conclusions. Each edge label identifies the applied rule.

Example DOT Output

For a penguin theory with r2 > r1:

digraph Explanation {
  rankdir=BT;
  node [fontname="Helvetica"];
  edge [fontname="Helvetica"];

  title [label="+d ~flies" shape=plaintext fontsize=14 fontcolor=black];

  n1 [label="~flies\n[defeasible: r2]" shape=box style=filled fillcolor="#d4edda"];
  n2 [label="penguin\n[fact: f1]" shape=box style=filled fillcolor="#cce5ff"];
  n2 -> n1 [label="r2"];
  title -> n1 [style=invis];

  // Blocked alternatives
  subgraph cluster_blocked {
    label="Blocked Alternatives";
    style=dashed;
    color=red;
    b3 [label="flies\n(rule: r1)\nblocked: superiority" shape=box style="dashed,filled" fillcolor="#ffcccc"];
  }

  // Conflict resolutions
  subgraph cluster_conflicts {
    label="Conflict Resolutions";
    style=dashed;
    color=orange;
    c4 [label="r2 > r1\n(superiority)" shape=diamond style=filled fillcolor="#ffe0b3"];
  }
}

Use Case: Semantic Web Integration with JSON-LD

The JSON-LD output allows Spindle explanations to participate in the linked data ecosystem.

Publishing Explanations as Linked Data

#![allow(unused)]
fn main() {
use spindle_core::explanation::{explain, Annotations, ProofStep};
use spindle_core::literal::Literal;

let literal = Literal::simple("liable");
if let Some(explanation) = explain(&theory, &literal) {
    let jsonld = explanation.to_jsonld();

    // Serialize for publication
    let output = serde_json::to_string_pretty(&jsonld).unwrap();
    println!("{}", output);
}
}

The resulting JSON-LD document can be:

• Consumed by any JSON-LD processor (e.g., jsonld.js, Apache Jena)
• Expanded, compacted, or flattened using standard JSON-LD algorithms
• Converted to RDF triples for storage in a triple store
• Queried with SPARQL alongside other linked data

Provenance Tracking

When rules carry annotations with source and confidence information, the JSON-LD output maps these to standard provenance vocabulary:

{
  "@context": {
    "spindle": "https://spindle.dev/ontology#",
    "prov": "http://www.w3.org/ns/prov#",
    "rdfs": "http://www.w3.org/2000/01/rdf-schema#",
    "xsd": "http://www.w3.org/2001/XMLSchema#"
  },
  "@type": "spindle:Explanation",
  "conclusionType": "+d",
  "literal": "liable",
  "proofTree": {
    "@type": "spindle:ProofNode",
    "literal": "liable",
    "derivationType": "defeasible",
    "proofStep": {
      "@type": "spindle:ProofStep",
      "@id": "https://example.org/rules/r1",
      "ruleLabel": "r1",
      "ruleType": "defeasible",
      "wasAttributedTo": "legal-statute-42-usc-1983",
      "rdfs:comment": "Civil rights violation implies liability",
      "spindle:confidence": "0.9"
    }
  }
}

Linking to External Ontologies

By using standard vocabulary keys in annotations, you can link Spindle explanations to domain ontologies:

#![allow(unused)]
fn main() {
let mut annots = Annotations::with_entries(vec![
    ("dc:source", "https://www.law.cornell.edu/uscode/text/42/1983"),
    ("prov:wasAttributedTo", "https://example.org/agents/legal-expert"),
    ("rdfs:comment", "Section 1983 civil rights liability"),
]);
annots.id = Some("https://example.org/rules/civil-rights-liability".to_string());
}

This enables downstream systems to dereference rule sources, look up agent information, and integrate the explanation into a broader knowledge graph.

Limitations

1. Positive proofs only: The explain function returns None for literals that are not positively provable. The why-not CLI command and query module provide negative explanations.
2. Grounded theories: Explanations work on grounded theories. Explanation generation requires bound variables.
3. No incremental updates: A full reasoning pass produces explanations. Changes to the theory require re-running the reasoner.
4. Annotation attachment: Programmatic explanation construction requires manual annotation attachment to proof steps. The explain function does not yet automatically populate annotations from rule metadata.