How to evaluate a rule and read its proof#

This guide shows you how to build a rule with build_application_rule, run it against a graph, and read the proof behind each result row, for when you need both the answer and a human-readable account of why it holds.

Prerequisites#

A FactGraph with the facts your rule body needs. Field atoms such as User(u).status == "active" match field claims written by fg.fields.set. See How to write and read facts.
Be aware of how existence atoms compile. An existence atom such as User(u) lowers to the User:exists predicate, and a field atom like User(u).status == "active" lowers to both the User:exists predicate and the field predicate. So any rule body that mentions an entity variable carries an implicit User:exists requirement. fg.entities.create(...) emits only the entity’s identity claims; it does not emit a :exists claim (the :exists co-emission is transitional and not performed by the current write path, see the guard note in factgraph.sdk.store). A rule body that relies on existence therefore will not match entities created through the SDK write path until a :exists claim is present for them.
The rule-authoring imports come from factgraph.sdk.dsl. The schema base classes (Entity, Identity, Field) come from factgraph.sdk.

Steps#

Define a schema and create the entities the rule will match. create emits the identity claims for the entity; fg.fields.set adds field claims.

from factgraph.sdk import Entity, FactGraph, Field, Identity

class User(Entity):
    user_id: str = Identity()
    status: str = Field()

fg = FactGraph.create(schema_classes=[User])

alice = fg.entities.create(User, user_id="alice")
fg.fields.set(alice, "status", "active")

Build the rule with build_application_rule. Bind logic variables with the vars(...) context manager (it requires explicit names), then write the body as a list of ergonomic atoms over Entity(var). Declare a ports mapping from public port names to the logic variables that appear in the body. Pass repr= to give the rule a narrative template whose %port placeholders are filled from the row bindings.
```
from factgraph.sdk.dsl import build_application_rule, vars

with vars("u") as (u,):
    rule = build_application_rule(
        id="active_user",
        when=[User(u).status == "active"],
        ports={"user": u},
        repr="active user %user",
    )
```
The body atoms are ergonomic forms over Entity(var): User(u) is an existence atom, User(u).status == "active" adds the field equality (and an existence atom), User(u).user_id == "u-2" matches on identity, User(u).status == var binds a field to a logic variable, and LivesIn(li).user == User(u) is a cross-entity reference. The body must be AND-only: Case, nested OR-branch lists, raw Pred(...), RuleRef, and bare attribute refs are rejected with DSLToApplicationRuleError. Every named port variable must appear in the body, and an anonymous Entity(...) variable cannot be used as a port. See the rule-authoring reference for all atom forms and constraints.
Evaluate the rule with fg.eval.evaluate. Pass the rule as the body and as the closed head=. The engine= keyword is optional and resolves to "native" when omitted; pass "souffle", "problog", or "pyreason" to use another engine (see Choosing a reasoning engine).
```
result = fg.eval.evaluate(rule, head=rule)
```
evaluate returns an EvaluateResult. Index it (result[0]), iterate it, or use result.count(), result.first(), and result.exists().
To verify: result.count() reflects how many entities satisfy every atom in the body, including the implicit User:exists atom. A row’s bindings are wrapped values, so the bound entity reference is result[0].bindings["user"]["value"]. Because the SDK write path does not emit a :exists claim on create, this body, which carries an existence atom, will report result.count() of 0 for entities created this way until a User:exists claim exists for them.
Read the proof for a row by calling row.explain(), which returns an Explanation. Check explanation.status ("passed", "failed", "unsupported", or "invalid_request"); for a failed row read explanation.failure_class. Render the proof with the .repr property (a tuple of lines, the structured proof tree) or with .narrate() (a tuple of lines, the prose account that uses the rule and atom repr templates). Both return None when the status is "unsupported" or "invalid_request".
```
row = result[0]
explanation = row.explain()

assert explanation.status == "passed"
print("\n".join(explanation.repr))      # structured proof tree
print("\n".join(explanation.narrate())) # prose account
```
To verify: with a repr= template on the rule, the narrated lines render the bound entity, for example active user alice rather than the raw encoded reference.
To inspect individual atoms instead of the rendered text, walk the evidence: explanation.evidence.paths holds proof paths, each path.rules holds head and body rules, and each rule.atoms holds atoms with a repr_text and a verdict. See the evaluation reference for the EvidenceGraph model.

Variations#

Replay a single closed row with fg.eval.explain. Take a passing row, close it with row.close() to get a closed-head Rule, then call fg.eval.explain(rule, head=closed). This returns an Explanation directly. The head= must be closed (all ports bound); an open head raises RuleExprError.
```
closed = result[0].close()
explanation = fg.eval.explain(rule, head=closed)
```
Inspect a closed head that does not hold. When the closed head selects no matching facts, fg.eval.explain(...) still returns an Explanation with status == "failed" and failure_class == "closed_head_false", carrying failed evidence you can render the same way.