Bounded Modal and Epistemic Evaluation

GestaltDB evaluates finite world models over the existing bitemporal claim history. Accessibility is not inferred: each agent and frame has explicit, temporal links created with assert_world_accessibility. belief, knowledge, and modal are independent frames, so BELIEVES and KNOWS cannot silently collapse to the same relation.

Semantics

Every formula has independent truth and falsity support. The resulting ClaimStatus is supported, refuted, both, or unknown. NOT swaps support and refutation. AND and OR use the standard four-valued, paraconsistent truth tables; a contradiction therefore does not entail an unrelated proposition.

BELIEVES, KNOWS, and NECESSARY require their formula in every accessible world and are refuted by a refuting accessible world. POSSIBLE is supported by a supporting accessible world and refuted only when every accessible world refutes its formula. A modal expression with no matching positive accessibility facts is unknown, not vacuously true. Negative accessibility claims do not create links.

Atoms read all visible claims in their world unless the atom includes an agent field. Accessibility always requires the evaluating agent. Reads are pinned to one GraphReadView at the requested valid time and system horizon. max_depth bounds formula nesting and max_states bounds memoized expression/world states; exhaustion raises ModalEvaluationLimitError.

Python API

graph_db.assert_world_accessibility(
    agent="alice",
    from_world="actual",
    to_world="alice-belief-1",
    kind="belief",
    valid_from="2025-01-01T00:00:00Z",
)
graph_db.assert_claim(
    subject="bob",
    predicate="LOCATED_IN",
    object="paris",
    polarity="positive",
    agent="source:registry",
    world="alice-belief-1",
    confidence=0.9,
    valid_from="2025-01-01T00:00:00Z",
)

result = graph_db.entails(
    "alice",
    {"subject": "bob", "predicate": "LOCATED_IN", "object": "paris"},
    "BELIEVES",
    world="actual",
    valid_time="2025-06-01T00:00:00Z",
    max_depth=4,
    max_states=1000,
)
assert result.status.value == "supported"

system_time or through_commit selects a historical system horizon. The result contains a conservative confidence and a deterministic explanation with the read horizon, visited states, accessibility versions, claim validity and system times, source metadata, and rule-derivation provenance.

Validated Formula Shape

An atom is {"subject": ..., "predicate": ..., "object": ...}; use objectKind: "literal" for a literal object and optional agent to scope atomic evidence. Logical and nested modal forms are:

{"operator": "NOT", "formula": atom}
{"operator": "AND", "operands": [left, right]}
{"operator": "OR", "operands": [left, right]}
{"operator": "KNOWS", "agent": "bob", "formula": atom}
{"operator": "BELIEVES", "agent": "bob", "formula": atom}
{"operator": "POSSIBLE", "agent": "bob", "formula": atom}
{"operator": "NECESSARY", "agent": "bob", "formula": atom}

Unknown fields, unknown operators, missing agents for modal operators, and non-finite expression shapes are rejected before evaluation.

Cypher Procedure

kg.entails is explicitly allowlisted. Its options require world and validTime and accept systemTime, throughCommit, maxDepth, and maxStates. systemTime and throughCommit are mutually exclusive.

CALL kg.entails(
  'alice',
  {subject: 'bob', predicate: 'LOCATED_IN', object: 'paris'},
  'KNOWS',
  {world: 'actual', validTime: 1735689600000000, maxDepth: 4, maxStates: 1000}
)
YIELD status, confidence, explanation
RETURN status, confidence, explanation