Reason Commands

zetl reason exposes the Reasoning Engine through eight subcommands. All require --features reason at build time — see Feature Gates.

(given reason-status-done)
(given reason-explain-done)
(given reason-why-not-done)
(given reason-require-done)
(given reason-what-if-done)
(given reason-conflicts-done)
(given reason-export-done)
(given reason-provenance-done)

Commands

`reason status`

What does the vault’s combined Spindle Lisp theory conclude? Filter by polarity (--positive, --negative), strength (--definite, --defeasible), or literal name (--literal "release*").

`reason explain <literal>`

Why does a conclusion hold? Produces a proof tree tracing the derivation through rules back to facts, with full Provenance (file, line, page). Output as JSON, table, natural language, or Graphviz dot.

`reason why-not <literal>`

Why can’t something be proved? Identifies missing facts, blocked rules, or active defeaters.

`reason require <literal>`

What facts would make a goal provable? Abductive reasoning — finds the minimal sets of missing facts. Useful for answering “what would it take to make release-candidate true?”

`reason what-if <spl>`

Hypothetical reasoning. Temporarily adds facts or rules and shows what changes. Accepts inline Spindle Lisp or a file via --file.

`reason conflicts`

Detects unresolved logical contradictions — pairs of competing rules with no (prefer ...) relation. Use --suggest for resolution hints and --fail-on-conflicts for CI.

`reason export`

Exports the combined theory as JSON or reconstructed Spindle Lisp with Provenance comments. Use --with-conclusions to include reasoning results.

`reason provenance <literal>`

Traces a conclusion back to source files, cross-referenced with the Link Graph. Shows which pages contributed the facts and rules behind a result.

Try it on this vault

zetl -d . reason status
zetl -d . reason explain "release-candidate" --format natural
zetl -d . reason conflicts
zetl -d . reason require "release-candidate"
zetl -d . reason what-if "(given docs-updated)" --goal "release-candidate"

Element

Provenance

Fact

File path, line number, page name

Rule

File path, line number, page name, rule label

Conclusion

Full proof tree of contributing rules and facts

Why it fits knowledge management

Decision documents, architecture records, and project plans all contain reasoning that is provisional. A conclusion like “use Redis” might be well-supported now but defeated by a future license audit. Spindle Lisp lets you express this directly in your notes, and zetl’s Reasoning Engine computes what follows.

Type

Syntax

Meaning

Fact

(given X)

X is unconditionally true

Strict

(always name body head)

If body, then head — no exceptions

Defeasible

(normally name body head)

If body, normally head — can be defeated

Defeater

(except name body head)

If body, block head — but don’t assert the opposite

Tag

Meaning

+D

Definitely provable — strict derivation, no defeating possible

-D

Definitely not provable

+d

Defeasibly provable — inferred, no active defeaters

-d

Defeasibly not provable — blocked or no derivation path

Reasoning Engine

The reasoning engine takes Spindle Lisp extracted by the Scanner from across the entire vault, merges it into a single theory, and computes conclusions using Defeasible Reasoning. Every conclusion carries full Provenance — you can trace any result back to the exact file and line that contributed to it.

Pipeline

Extract — Scanner finds SPL blocks in Markdown fences and .spl files

Parse — spindle-parser converts SPL text into rule objects

Provenance — source file, line number, and page name are attached to each rule and fact

Combine — all rules and facts are merged into a single theory

Validate — check for undefined labels, duplicate definitions

Reason — spindle-core computes conclusions

Annotate — each conclusion is traced back to its proof sources

(given spindle-core-integrated) (given four-conclusion-types)

Tag

Meaning

+D

Definitely provable

-D

Definitely not provable

+d

Defeasibly provable

-d

Defeasibly not provable

Data model

Node — a Markdown page, identified by its title (filename without .md)

Edge — a wikilink from one page to another, with optional alias, heading, or block reference

The graph is built by the Scanner and cached by the Cache for incremental re-scans.

(given directed-graph) (given multi-hop-traversal)

Queries

Command

Description

links

Forward links from a page, with configurable depth

backlinks

Pages linking to a target, with depth traversal

path

Shortest link path between any two pages

export

Full graph as JSON

These are exposed through Graph Queries. With the --with-conclusions flag, link results are cross-referenced with the Reasoning Engine to show what each linked page contributes to the vault’s logic.

Reason Commands

Commands

reason status

reason explain <literal>

reason why-not <literal>

reason require <literal>

reason what-if <spl>

reason conflicts

reason export

reason provenance <literal>

Try it on this vault

Backlinks

`reason status`

`reason explain <literal>`

`reason why-not <literal>`

`reason require <literal>`

`reason what-if <spl>`

`reason conflicts`

`reason export`

`reason provenance <literal>`