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

from __future__ import annotations

from dataclasses import dataclass
from typing import Any, TypeAlias

from guardrail_calculus import (
    SubjectFacts,
    SubjectRef,
    clock_from_hhmm,
    duration_hours,
    ref,
    subject,
    subject_ref,
)
from guardrail_calculus.dimension_value_builtins import ClockRef


@dataclass(frozen=True)
class FlightSubject:
    """The subject schema for the flight puzzle, declaring a departure observable."""

    departure: ClockRef


@dataclass(frozen=True)
class FlightPuzzle[
    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


SubjectRefFacts: TypeAlias = SubjectFacts[None, Any, SubjectRef[FlightSubject]]

FlightPuzzleRefs: TypeAlias = FlightPuzzle[
    SubjectRefFacts,
    SubjectRefFacts,
    SubjectRefFacts,
    SubjectRefFacts,
]


r = ref[FlightPuzzleRefs]
_ = subject_ref[FlightSubject]


# roadmap V8 Stage 3: the departure times were previously threaded through a
# TypeVar(bound=ClockTime)/RuntimeTimes[...] reflection mechanism
# (FlightPuzzleFactory.of(...) read four literal types back out of a class's
# __orig_bases__ and reified them via ClockTime.from_hhmm). That mechanism
# is structurally impossible for a value-authored dimension: PointVal's
# __class_getitem__ returns the bare runtime class, discarding its subscript,
# so a spelled type like PointVal[TimeAlgebraFamily, Literal[1730]] carries no
# retrievable arguments at runtime (confirmed empirically, not assumed) --
# unlike ClockTime, a real PEP 695 generic whose subscript survived as
# __args__. The whole apparatus existed only to bridge "spell a literal once,
# as a type" and "construct a matching runtime value"; the values API needs
# no bridge, since a literal-preserving constructor call does both directly
# (clock_from_hhmm(1730) is simultaneously the construction and the precise
# static witness). Ordinary module-level values replace it.
_p1730 = clock_from_hhmm(1730)
_p1520 = clock_from_hhmm(1520)
_p830 = clock_from_hhmm(830)
_p620 = clock_from_hhmm(620)


def _build_flight_puzzle():
    return FlightPuzzle(
        avery=(
            subject()
            .check(
                "A",
                (_.departure @ _p620).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 @ _p830).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) <= _p1520).annotate(
                    "Casey's 8-hour journey ends by 15:20."
                ),
            )
            .block()
        ),
        drew=(
            subject()
            .given(
                (_.departure @ (_p1730 - duration_hours(8))).annotate(
                    "Drew departs 8 hours before 17:30."
                )
            )
            .block()
        ),
    )


flight_puzzle = _build_flight_puzzle()

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.