hermes.kernel

Verifier

The verifier checks a plan against the schema and a stated goal before anything runs. Ill-typed steps never reach the graph store.

Typing

Schema.from_kg(kg) reads classes, properties, rdfs:domain, rdfs:range, and the closure of rdfs:subClassOf. Kernel.check(plan, goal) builds a typing context for the plan's variables:

?x a C gives ?x : C.
?x p ?y gives ?x the domain of p and ?y its range.
Classes are compared up to subclass.

Two unrelated classes on one variable are a warning, not an error: RDF is open world and the schema need not declare disjointness. Source: kernel.py.

Errors

Error	Example message
Unknown term in a namespace the schema describes	`unknown property ex:hosts (did you mean ex:hosted?)`
Literal where an entity is required	`type mismatch: ex:hosted expects an entity of ex:OlympicGames, got the literal "Winter"`
Literal used as an entity, or the reverse	`type mismatch: ?s is a literal but ...`
Unbound variable	`unbound variable ?y in FILTER`
BIND onto a bound variable	`BIND target ?g is already bound`
Ungrouped projection	`?g is neither grouped nor aggregated`

Variables that occur only inside MINUS are not bound, as in SPARQL. The check runs in one pass over the plan; nothing is executed.

Goals

A goal states what the question asks for before the query exists:

{"op": "goal", "answer": ["?c"], "kind": "entity", "type": "ex:City", "many": true}

kind is entity, literal, number, or boolean; type is optional; many is false when one answer is expected. The verifier lists the open goals the plan does not yet meet: the answer variable is not bound or not projected, other variables are projected, a number is not an aggregate or a numeric value, an entity is a literal, the type is not established, a yes-or-no question is not an ASK, or, after execution, there is more than one solution when one was asked for.

The goal is written by the planner from the question, so it can be wrong. The verifier guarantees that a plan has the shape its goal asks for, not that the goal is the question.

The prover system

prover is the algebra agent with the verifier installed. The planner states the goal first. Each turn the prompt shows the plan state: the typing context and the open goals. finish is refused while an error or an open goal remains. The result adds kernel_rejections and goal. Source: prover.py.

context:
  ?c : ex:City
  ?g : ex:OlympicGames
open goals:
  goals accomplished