Skip to content

How reasoning works

The reasoning layer turns a set of givens and candidate propositions into an explanation DAG — a single graph that records every fact, every derivation step, and every check, so that any conclusion can be traced back to the inputs that justify it.

The three node kinds

Every node in the graph is one of:

  • Given — an input fact the author asserted (rectangle).
  • Derived — a fact the solver produced by a rule (stadium).
  • Check — a candidate proposition to be classified; checks are sinks and can never be premises (diamond).

Derivations that produce a new fact are themselves first-class nodes (circles). A rule with several premises shows them all flowing into one derivation step, which flows into the conclusion:

premise fact ─┐
              ├─► derivation step ─► conclusion fact
premise fact ─┘

This is why a single fact can have several independent derivations without overloading a single edge label, and why the graph stays acyclic by construction: edges only ever flow forward into freshly created nodes.

Checks are always leaves, never intermediate steps, so an explanation that justifies a check skips the intermediate node: each premise gets a dotted edge straight into the check, labelled with the explanation's rule. Nodes are grouped into rows — Givens, Reasoning, Derived facts, Checks — by colour and a floating text label rather than a Mermaid subgraph, since a subgraph's background rectangle can visually mask an edge that crosses it.

A worked example: the flight puzzle

In the canonical flight puzzle, Drew departs eight hours before 17:30, and Blake departs one hour before Drew

Here is the executable flight puzzle example demonstrating DSL constraints, reasoning, and solver verification:

Source: src/guardrail_calculus/examples/flight_puzzle.py

"""The flight puzzle: one module that is both the program and the document.

Four travellers, one shared timeline. Module level holds only the schemas;
the problem is the `Flight` instance its `@puzzle` entry point builds, every
subject block inline (workflow-entry-points.md). Importing the module binds
`flight_puzzle` to a `PuzzleProblem`; parsing it with `lower_source` reads
the same problem without running anything, and the two ask the same request
(tests/unit/test_entry_points.py).

This one file replaced two, `flight_puzzle.py` built with the builders and
`flight_puzzle.guard` written as text, which held the same puzzle twice.
"""

from typing import Any

from guardrail_calculus import (
    DEPARTURE,
    EntityKind,
    SubjectFacts,
    SubjectRef,
    clock_from_hhmm,
    data_schema,
    duration_hours,
    occurrence,
    puzzle,
    ref,
    subject,
)


__all__ = [
    "Flight",
    "Traveller",
    "flight_puzzle",
]


@data_schema
class Traveller:
    """A traveller: when they depart is their departure's, not a field."""


@data_schema
class Flight:
    avery: SubjectFacts[Any, Any, SubjectRef[Traveller]]
    blake: SubjectFacts[Any, Any, SubjectRef[Traveller]]
    casey: SubjectFacts[Any, Any, SubjectRef[Traveller]]
    drew: SubjectFacts[Any, Any, SubjectRef[Traveller]]


@puzzle
def flight_puzzle() -> Flight:
    r = ref[Flight]
    avery_departs = occurrence("avery_departs", DEPARTURE, agent=r.avery.own)
    blake_departs = occurrence("blake_departs", DEPARTURE, agent=r.blake.own)
    casey_departs = occurrence("casey_departs", DEPARTURE, agent=r.casey.own)
    drew_departs = occurrence("drew_departs", DEPARTURE, agent=r.drew.own)
    return Flight(
        avery=subject(name="Avery", kind=EntityKind.PERSON)
        .occurs(avery_departs)
        .check(
            "A",
            avery_departs.at(clock_from_hhmm(620)).annotate("Avery departs at 06:20."),
        )
        .block(),
        blake=subject(name="Blake", kind=EntityKind.PERSON)
        .occurs(blake_departs)
        .given(
            blake_departs.at(drew_departs.time - duration_hours(1)).annotate(
                "Blake departs one hour before Drew."
            )
        )
        .check(
            "B",
            blake_departs.at(avery_departs.time).annotate(
                "Blake and Avery depart at the same time."
            ),
        )
        .check(
            "C",
            blake_departs.at(clock_from_hhmm(830)).annotate("Blake departs at 08:30."),
        )
        .check(
            "D",
            (blake_departs.time > avery_departs.time).annotate(
                "Blake departs after Avery."
            ),
        )
        .block(),
        casey=subject(name="Casey", kind=EntityKind.PERSON)
        .occurs(casey_departs)
        .given(
            casey_departs.at(avery_departs.time).annotate(
                "Casey departs at the same time as Avery."
            )
        )
        .check(
            "E",
            (casey_departs.time + duration_hours(8) <= clock_from_hhmm(1520)).annotate(
                "Casey's 8-hour journey ends by 15:20."
            ),
        )
        .block(),
        drew=subject(name="Drew", kind=EntityKind.PERSON)
        .occurs(drew_departs)
        .given(
            drew_departs.at(clock_from_hhmm(1730) - duration_hours(8)).annotate(
                "Drew departs 8 hours before 17:30."
            )
        )
        .block(),
    )

Solving it and rendering the graph with graph_to_d3_html yields the D3 DAG below — the two givens combine through one derivation step to prove Blake's departure, which is then recognised as equivalent to check C:

Note

This diagram is generated from the live FactGraph during the MkDocs build. The Mermaid renderer remains available through graph_to_mermaid and graph_to_mermaid_markdown for text-oriented snapshots and Markdown-only targets.

Classifying a check

A check is classified by asking the solver two questions against the base facts: is the check satisfiable, and is its negation satisfiable (refutable)? The pair of answers maps to a Status:

%%{init: {"themeCSS": ".node rect, .node circle, .node ellipse, .node path, .node polygon { fill: color-mix(in srgb, var(--fg-ink) 5%, var(--fg-paper)); stroke: var(--fg-row-check-border); stroke-width: 1.5px; rx: 6px; filter: drop-shadow(0 1px 3px rgb(15 23 42 / 22%)); } .label, .label span { color: var(--fg-ink); font-family: var(--md-mermaid-font-family); } .label text { fill: var(--fg-ink); } .label foreignObject { line-height: normal; overflow: visible; } .edgePath .path, .flowchart-link { stroke: var(--fg-edge); } .edgePath .arrowheadPath { fill: var(--fg-edge); stroke: none; } marker { fill: var(--fg-edge) !important; } .edgeLabel, .edgeLabel p, .edgeLabel span, .labelBkg { background-color: var(--fg-paper); color: var(--fg-edge); } .edgeLabel rect { fill: var(--fg-paper); opacity: 1; } .cluster rect { fill: var(--fg-paper); stroke: var(--fg-line); stroke-width: 2px; rx: 14px; } .cluster span { color: var(--fg-ink); font-family: var(--md-mermaid-font-family); } .node[class*=\"verdict-\"] rect { stroke-width: 2px; rx: 999px; } .node[class*=\"verdict-\"] .nodeLabel { font-weight: 700; font-family: ui-monospace, SFMono-Regular, Menlo, monospace; } .node.verdict-verified rect { stroke: var(--fg-verified); } .node.verdict-verified .nodeLabel { color: var(--fg-verified); } .node.verdict-falsified rect { stroke: var(--fg-falsified); } .node.verdict-falsified .nodeLabel { color: var(--fg-falsified); } .node.verdict-unknown rect { stroke: var(--fg-unknown); } .node.verdict-unknown .nodeLabel { color: var(--fg-unknown); } .node.verdict-inconsistent rect { stroke: var(--fg-inconsistent); } .node.verdict-inconsistent .nodeLabel { color: var(--fg-inconsistent); } .node.dead rect { stroke: var(--fg-falsified); stroke-width: 2px; } .node.dead .nodeLabel { color: var(--fg-falsified); } .node.unread rect { stroke: var(--fg-unknown); stroke-dasharray: 4 3; } .node.unread .nodeLabel { color: var(--fg-unknown); } .node.flagged rect { stroke: var(--fg-inconsistent); stroke-width: 3px; } .node.flagged .nodeLabel { color: var(--fg-inconsistent); }"}}%%
flowchart LR
    %% Drawn in the canvas's own tokens, in both schemes, by the directive
    %% above: the verdict boxes in the verdict tokens, so a box here, a pill
    %% in the prose and a chip on the canvas are one colour
    %% (docs/stylesheets/mermaid-canvas.css says how and why).
    subgraph " "
      direction LR
      A["satisfiable: yes<br/>refutable: no"] --> V["VERIFIED"]
      B["satisfiable: no<br/>refutable: yes"] --> F["FALSIFIED"]
      C["satisfiable: yes<br/>refutable: yes"] --> U["UNKNOWN"]
      D["satisfiable: no<br/>refutable: no"] --> I["INCONSISTENT_BASE"]
    end
    class V verdict-verified;
    class F verdict-falsified;
    class U verdict-unknown;
    class I verdict-inconsistent;

UNKNOWN is the interesting verdict: the check is consistent but not entailed — a genuine gap. In workflow terms that is an input region no rule decides, and it is what the planned synthetic-failsafe mechanism turns into a safe, audited default rather than silent undefined behaviour.

If the solver cannot decide either question (e.g. an encoding it does not support), the verdict is UNDECIDED — reported honestly rather than guessed.