Reasoning, evaluation, and evidence#

When you evaluate a rule against a factgraph, you do not just get back a set of answers. You get back answers that can each explain themselves, condition by condition, in a way that replays to the same result every time. This page discusses how a rule turns into result rows, why each row can carry its own proof, and what makes that proof deterministic. It is the conceptual companion to Evaluation and explanation, which lists the precise types and signatures.

A rule produces rows, and rows are addresses, not just data#

Evaluation takes a rule (or rule expression) plus a closed head and returns an EvaluateResult: an ordered, immutable collection of EvaluateRow. Each row is the binding of the head’s ports to concrete values, the values for which the rule held. So far this is unremarkable; it is what any query returns.

What is unusual is that a row is content-addressed. A row carries a row_id, a digest, and a closed_head_digest, and the result that contains it carries a result_id and a ResultFingerprint. None of these are opaque handles handed out by a server. They are derived, by hashing, from the inputs and the outputs of the evaluation. The row_id is row_id_for(run_id, bindings), a SHA-256 over the canonical encoding of the bindings; the result_id is result_id_for(...) over the engine, the expression digest, the rule-set digest, the view-snapshot digest, the optional config digest, the run id, and the head’s id and content digest. The ResultFingerprint collects exactly those component digests (expr_digest, rule_set_digest, view_snapshot_digest, config_digest, result_digest, run_id).

This is the first design decision worth naming. By making identity a function of content rather than a generated token, the result becomes a thing you can compare, store, and re-derive. Two evaluations of the same expression over the same facts under the same semantics produce the same result_id and the same row digests, except for the run_id, which is freshly minted per run (new_run_id) and is the only part deliberately unique. The fingerprint, in other words, separates “what was asked and answered” (stable) from “which physical run produced it” (unique). That separation is what later lets a proof prove that it belongs to a particular answer over a particular world.

The closed head: pinning a single claim before you ask why#

A row on its own says “these bindings satisfied the rule.” To explain a single, fully-grounded claim, you first have to say which claim. That is the role of closing the head. EvaluateRow.close() turns an open head (ports as variables) into a Rule whose ports are pinned to the row’s values: for a value port it adds an equality constraint to the bound constant, and for an entity-reference port it expands the entity into its identity predicates (_build_closed_head_from_row and _entity_identity_closure_atoms). The closed head is then re-inspected, and if any port is still unbound, construction fails with RuleExprError. A row’s closed_head_digest is the hash of that closed rule.

fg.eval.explain(...) requires you to hand it a head that is already closed, and it checks this up front (_require_manual_explain_closed_head). The reason is conceptual, not bureaucratic: an explanation answers a yes/no question about one specific grounded claim, so the claim must be fully grounded before the question is even well-formed. Asking “why did some user qualify?” is not a question evidence can answer; “why did this user qualify?” is.

This also explains the shape of explain’s two outcomes. If the closed head matches a row in the result, you get a passed explanation built from that row. If it matches no row, you get a failed explanation with failure_class="closed_head_false", and crucially you still get evidence: the engine is replayed against the same view to show, condition by condition, where the derivation stopped. A negative answer is as explainable as a positive one. That is why the evidence model has three verdicts, not two.

The evidence model: three verdicts, a tree of rules and atoms#

The proof attached to an explanation is an EvidenceGraph. Its paths are EvidenceTrees (and, for temporal engines, EvidenceTimelines). A tree holds EvidenceRules, each tagged with a role of head or body, and each rule holds EvidenceAtoms. An atom is a single condition: a Fact (a predicate over terms), a Compare (an ordering or equality), a Builtin, or an Aggregate. Every atom carries a verdict, and the verdict is one of exactly three kinds:

• Holds: the condition was satisfied, with a certainty and optional supporting Sources.
• Fails: the condition was evaluated and was not satisfied.
• NotReached: the condition was never evaluated, because an earlier condition it depended on did not bind. NotReached records blocked_by, the variable that was missing.

The three-way split is the heart of the model. A two-valued proof can tell you a rule failed but not whether a given condition was tried and rejected or simply never got the chance. The distinction matters for debugging and for honesty: a not_reached atom is not evidence against the claim, it is evidence that the question was cut short upstream. Statuses propagate the same way at every level. _atom_status, _tree_status, and the rule-level status all say: all-holds is holds, all-not-reached is not_reached, any-fails is fails. So a tree’s overall status is a faithful roll-up of its atoms’ verdicts, and the same three words describe an atom, a rule, a tree, and the graph.

Each EvidenceAtom also carries an atom_id and a baked repr_text, a human-readable rendering of the condition with the row’s actual values substituted (for example, an entity rendered through its schema repr, a float decoded for display). Rendering happens once, at probe time, against the schema and the view facts, so the proof is self-describing without needing the schema later to be read back.

How the native engine builds the proof: replaying the derivation#

The native proof is not reconstructed from the answer; it is produced by re-walking the derivation over the very facts that were evaluated. probe_native takes the lowered plan, the row’s bindings as the initial environment, and a snapshot of the view facts, then walks each branch of the rule body atom by atom (_probe_branch, _probe_atom). At each atom it extends the current set of variable environments by matching against the facts; if the atom binds new rows it Holds and the environments grow, if it has all its inputs but matches nothing it Fails, and if a variable it needs is unbound it is NotReached with that variable as blocked_by. Body atoms are grouped back under the rule occurrence they came from, joins between occurrences become EvidenceJoins carrying their own status, and the head becomes the single head-role rule. The result is one EvidenceTree per branch; a disjunction (an OR of branches) becomes multiple trees, which is exactly what the narrative renders as alternative derivation paths.

Two properties follow from doing it this way. First, the proof reflects the real evaluation order and the real data, not an idealized re-derivation, so a not_reached in the proof corresponds to an actual gap in binding. Second, because the walk is a pure function of the plan, the bindings, the view facts, and the schema, it is reproducible: feed it the same inputs and it produces the same tree. The environments are deduplicated and sorted by a canonical key (_dedupe_envs, _env_sort_key) precisely so that the order of rows and the structure of the tree do not depend on incidental iteration order. This is determinism enforced by construction rather than promised by convention.

Why it replays the same way#

Determinism here is not a single feature, it is the conjunction of several deliberate choices, each visible in the code.

Identity is content-derived. Every id and digest is a SHA-256 over a canonical byte encoding (canonical_bytes_for_evaluate), which sorts mapping keys, normalizes tuples and dates, and rejects non-finite floats. Equal inputs hash to equal tokens, so the same question over the same world yields the same result_id, the same row_ids, and the same closed_head_digests.

The world is pinned. The view_snapshot_digest folds in the database id, the base transaction, the schema digest, and the active assertion ids. The proof is built against that same view. Because the ledger is append-only (see About the append-only ledger and provenance), the snapshot a result was computed over does not mutate underneath it; replaying against the same base transaction sees the same facts.

The semantics are pinned. When a non-native engine is used with a SemanticsProfile, the profile is hashed into config_digest and into the result. The same expression evaluated under a different profile is, correctly, a different result.

Evidence is bound to its context. Before an explanation is returned, the live row is checked against the result by _row_anchor_matches, which compares row_id, digest, the derived evidence-ref id, and closed_head_digest. A row that no longer matches yields an unsupported explanation with code STALE_ROW; a row from a different result yields ROW_NOT_IN_RESULT; a DetachedRowError guards a row that has lost its link to a result entirely. The EvidenceGraph.metadata of a passed explanation must contain exactly the v1 set of context keys, and each must equal the value re-derived from the row and result (_validate_evidence_metadata_for_row_result); a graph that fails this check is rejected as GRAPH_VALIDATION_FAILED. The effect is that a proof cannot quietly drift away from the answer it claims to explain. If the proof and the result disagree, you are told, rather than shown a plausible fiction.

Certainty: one shape, several readings#

Verdicts and trees carry a Certainty, a frozen (lo, hi, kind) interval where kind is boolean, probabilistic, or possibilistic. Native (and Souffle) reasoning is boolean: BOOLEAN_CERTAINTY is (1.0, 1.0, "boolean"), and the renderer omits any certainty suffix when the interval is exactly [1.0, 1.0]. Probabilistic and possibilistic engines reuse the same interval shape with a different kind, and the narrative renders them differently: a point probability as with probability p, an interval as with bound [lo, hi]. One data shape spans all three readings, which is what lets the higher layers, and the human-readable output, treat boolean and uncertain reasoning uniformly while still printing each correctly. The per-engine details live in Engines and semantics.

Rendering: deterministic prose from the same tree#

An Explanation exposes two views of its evidence: .repr, a compact structural listing, and .narrate(), a human narrative. Both are pure functions of the graph (walk_evidence, narrate_evidence); both cache their output and return None for the unsupported and invalid_request statuses, where there is no evidence to render. The narrative orders rules with the head first and bodies after by a fixed sort key, renders each atom with its baked repr_text and a verdict icon, and reconstructs the derivation line and, for probabilistic results, the probability formula. Because the renderer reads only the tree and the tree is itself deterministic, the prose is deterministic too.

This is what the cross-engine conformance suite exercises: it evaluates the same rule on the native, Problog, and Souffle engines and asserts that the normalized narratives and the per-atom verdict matrices match across engines. That test is the strongest practical statement of the model’s intent. The proof is meant to be a property of the reasoning, not an artifact of which engine happened to run it.

What this is, and what it is not#

The evidence model is a record of a derivation, not a planner or a solver. It tells you, faithfully and reproducibly, why a specific grounded claim did or did not follow from a specific set of facts under a specific semantics. It does not search for the facts that would make a claim true, and it does not optimize. The legacy candidate/accept flow (CandidateSet, Inference) is not part of this surface and is noted only for context. The value on offer is narrower and, for an auditable system of record, more useful: every answer can show its work, and the work checks out the same way twice. For how this feeds auditability, see About auditability.

Related: Evaluation and explanation for the precise types and methods; Engines and semantics for engine and certainty details; How to evaluate a rule and read the proof for acting on this; About the append-only ledger and provenance for why the world a result was computed over does not move.