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: docs/snippets/flight_puzzle.py

from __future__ import annotations

from dataclasses import dataclass
from typing import Any

from guardrail_calculus import (
    ClockTime,
    Duration,
    SubjectFacts,
    _,
    ref,
    subject,
)


@dataclass(frozen=True)
class FlightPuzzleDemo[
    AveryT: SubjectFacts[Any, Any, Any],
    BlakeT: SubjectFacts[Any, Any, Any],
    CaseyT: SubjectFacts[Any, Any, Any],
    DrewT: SubjectFacts[Any, Any, Any],
]:
    avery: AveryT
    blake: BlakeT
    casey: CaseyT
    drew: DrewT


r = ref[FlightPuzzleDemo]


flight_puzzle_demo = FlightPuzzleDemo(
    avery=(
        subject()
        .check(
            "A",
            (_.departure @ ClockTime.from_hhmm(620)).annotate(
                "Avery departs at 06:20."
            ),
        )
        .block()
    ),
    blake=(
        subject()
        .given(
            (_.departure @ (r.drew.own.departure - Duration.hours(1))).annotate(
                "Blake departs one hour before Drew."
            )
        )
        .check(
            "B",
            (_.departure @ r.avery.own.departure).annotate(
                "Blake and Avery depart at the same time."
            ),
        )
        .check(
            "C",
            (_.departure @ ClockTime.from_hhmm(830)).annotate(
                "Blake departs at 08:30."
            ),
        )
        .check(
            "D",
            (_.departure > r.avery.own.departure).annotate(
                "Blake departs after Avery."
            ),
        )
        .block()
    ),
    casey=(
        subject()
        .given(
            (_.departure @ r.avery.own.departure).annotate(
                "Casey departs at the same time as Avery."
            )
        )
        .check(
            "E",
            (_.departure + Duration.hours(8) <= ClockTime.from_hhmm(1520)).annotate(
                "Casey's 8-hour journey ends by 15:20."
            ),
        )
        .block()
    ),
    drew=(
        subject()
        .given(
            (_.departure @ (ClockTime.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:

flowchart LR
    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
    classDef v fill:#E8F5E9,stroke:#1B5E20;
    classDef f fill:#FFEBEE,stroke:#B71C1C;
    classDef u fill:#FFF3E0,stroke:#E65100;
    classDef i fill:#ECEFF1,stroke:#37474F;
    class V v;
    class F f;
    class U u;
    class I i;

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.