8 Explanation System

9.0

8 Explanation System🔗ℹ

package: spindle

The explanation system provides detailed derivation traces and supports multiple output formats for understanding reasoning results.

8.1 Explanation Structures🔗ℹ

procedure
(explanation? v) → boolean?
v : any/c

Returns #t if v is an explanation.

procedure
(explanation-conclusion-type e) → symbol?
e : explanation?

Get the conclusion type (+D, -D, +d, -d).

procedure
(explanation-literal e) → literal?
e : explanation?

Get the literal being explained.

procedure
(explanation-proof-tree e) → (or/c proof-node? #f)
e : explanation?

Get the proof tree (derivation).

8.2 Proof Trees🔗ℹ

procedure
(proof-node? v) → boolean?
v : any/c

Returns #t if v is a proof node.

procedure
(proof-node-literal n) → any/c
n : proof-node?

Get the literal at this node.

procedure
(proof-node-derivation-type n) → symbol?
n : proof-node?

Get derivation type (definite or defeasible).

procedure
(proof-node-proof-step n) → (or/c proof-step? #f)
n : proof-node?

Get the proof step used.

procedure
(proof-step? v) → boolean?
v : any/c

Returns #t if v is a proof step.

procedure
(proof-step-rule-label s) → string?
s : proof-step?

Get the rule label used.

procedure
(proof-step-rule-type s) → symbol?
s : proof-step?

Get the rule type.

procedure
(proof-step-body-proofs s) → (listof proof-node?)
s : proof-step?

Get proofs for body literals (recursive structure).

8.3 Annotations🔗ℹ

Rules and conclusions can carry metadata annotations.

procedure
(annotations? v) → boolean?
v : any/c

Returns #t if v is an annotations container.

procedure
(annotations-ref a key [default]) → any/c
  a : annotations?
  key : string?
  default : any/c = #f

Get annotation value by key.

procedure
(annotations-description a) → (or/c string? #f)
a : annotations?

Get the description annotation.

procedure
(annotations-source a) → (or/c string? #f)
a : annotations?

Get the source/provenance annotation.

procedure
(annotations-confidence a) → (or/c number? #f)
a : annotations?

Get the confidence annotation.

8.4 Output Formats🔗ℹ

8.4.1 Natural Language🔗ℹ

procedure
(explanation->natural-language e) → string?
e : explanation?

Convert explanation to human-readable text.

Output includes:

Conclusion summary
Derivation steps with descriptions
Alternative derivations considered
Conflict resolutions

8.4.2 JSON-LD🔗ℹ

procedure
(explanation->jsonld e) → hash?
e : explanation?

Convert explanation to JSON-LD (linked data).

Includes @context with standard vocabularies:

dc: — Dublin Core (provenance)
prov: — W3C Provenance
spindle: — Spindle vocabulary

procedure
(explanation->json-string e) → string?
e : explanation?

Convert to JSON string.

8.4.3 GraphViz DOT🔗ℹ

procedure
(explanation->dot e) → string?
e : explanation?

Convert explanation to GraphViz DOT format for visualization.

(define dot (explanation->dot my-explanation))
(display-to-file dot "proof.dot")

8.4.4 Provenance Chain🔗ℹ

procedure
(explanation->provenance e) → string?
e : explanation?

Convert to tree-formatted provenance chain showing the derivation path with sources and attributions.

8.5 Example🔗ℹ

(require spindle spindle/explanation)

(define-values (ast errors) (parse-dfl-string theory-text))
(define theory (ast->theory ast))
(define conclusions (reason-with-explanations theory))

(for ([c conclusions])
  (when (explained-conclusion-explanation c)
    (displayln (explanation->natural-language
                (explained-conclusion-explanation c)))))

1	Overview
2	Getting Started
3	Core API Reference
4	DFL Syntax Reference
5	SPL Syntax Reference
6	Query Operations
7	Process Mining
8	Explanation System
9	Examples
10	Advanced Topics
	Index

8.1	Explanation Structures
8.2	Proof Trees
8.3	Annotations
8.4	Output Formats
8.5	Example