Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

RFD 0058 — The Tableau Model Engine (Modal Escape Hatch)

Status

Proposed. Slice 1 is the explicit-single-frame K3 modal tableau, built as a new tier executor. Slice 2 — the fibred composition of the Kripke frame over standpoints (this document’s §“Slice 2”) — is built. Slice 3 is scoped here as a roadmap but is NOT built; the refusal it will eventually lift stays a loud refusal (OE1104).

Summary

Argon’s reasoner is a tier-classified, Z-set, semi-naive Datalog engine. The modal surface (box/diamond over a Kripke frame, §11.2) is the one place the Datalog engine cannot reach: a box(P) is a universal over an accessibility relation, a diamond(P) an existential, and while the standpoint frame is translated to stratified Datalog (translate_standpoint_modals, §D3), the explicit Kripke frame — worlds and an accessible relation the modeler declares via std::kripke — has no evaluator. Today every such modal is refused with OE1104 (the held escape hatch).

This RFD introduces a tableau model engine as a new TierExecutor advertising Tier::Modal. A tableau is the standard decision procedure for modal/description logics: it builds a candidate Kripke model and checks satisfiability by saturating expansion rules until a clash or an open model. It is the right machinery for the modal escape hatch precisely because it can do what fixpoint Datalog cannot — quantify over the frame structurally.

Because a tableau is the sensitive piece of a financial-grade substrate — a wrong answer here is silently catastrophic — the engine is gated by a differential oracle against both the existing Datalog executor (on the decidable overlap) and the mechanized ModalFrame semantics, before it goes anywhere near production.

The escape hatch as a tier executor (not a second path)

The load-bearing invariant of the reasoner is that all evaluation flows through Engine::evaluate, dispatched to a TierExecutor by tier. The tableau is a tier executor, not a parallel evaluation path:

        AtomIR-shaped rules
               ↓ instantiate
   translate_standpoint_modals
     ├─ standpoint frame → stratified Datalog (recursive tier)
     ├─ explicit Kripke frame → AtomIR::Modal preserved      ← slice 1
     └─ everything else → OE1104 (narrowed)
               ↓ compile
   CompiledAtom::Modal  (new variant)                        ← slice 1
               ↓ Engine::evaluate dispatch by tier
   KripkeExecutor : TierExecutor (Tier::Modal)               ← slice 1
               ↓
   Z-set RelationCatalog (BTreeMap<Tuple, Weight>)

The executor reads the RelationCatalog — the Datalog-materialized base facts (accessible, the per-world classification of the inner predicate) seed the tableau. This is the Konclude pay-as-you-go move: saturation first, tableau only for the modal goals. The executor writes its derived modal facts back into the same catalog. There is no second store, no second engine — the executor is one more backend behind the same dispatch surface.

Slice 1 — scope (held precisely)

A box/diamond modal tableau over a single explicit Kripke frame, K3-valued, strict consistency, one frame. Concretely:

  • Frame: the modeler’s std::kripke Worlds and accessible relation — explicit facts in the catalog. Not the standpoint reach-closure (that is the already-built §D3 Datalog translation), not the rigidity/classification frame.
  • Operators: box(P) and diamond(P) where P is a single positive predicate atom whose evaluation is per-world.
  • Value algebra: K3 — Truth4 constrained to {Is, Not, Can}.
  • Consistency: strict. A proposition forced to both Is and Not at one world is a clash. Can (unknown, open-world) is an open branch, not a clash.

Slice 1 does not do, and these keep refusing with a tighter OE1104:

  • The fibred composition of the Kripke frame over standpoints (slice 2 — now built; see §“Slice 2”).
  • Rigid roles, nominals (slice 3).
  • The classification/rigidity frame (slice 3+).

Semantics (authoritative; cites the mechanization)

Over a Kripke frame with accessibility R (spec/lean/Argon/Reasoning/Modal.lean, spec/lean/Argon/Standpoint/ModalFrame.lean):

  • box(w, P) = ∀ w'. R(w, w') → P(w') — necessity is the intersection over accessible worlds (Modal.lean box).
  • diamond(w, P) = ∃ w'. R(w, w') ∧ P(w') — possibility is the union (Modal.lean diamond).
  • Duality: diamond w P ↔ ¬ box w (¬P) (diamond_iff_not_box_not, proven).

Slice 1’s R is the user’s explicit accessible facts; the abstract KripkeFrame of Modal.lean is instantiated with those facts directly (not the reach reflexive-transitive closure ModalFrame.lean builds for standpoints).

Dead-end worlds (the faithful K(m) semantics). A world with no accessible successor is a dead-end. box(w, P) = ∀ w'. R(w, w') → P(w') is vacuously true there (the universal over an empty set), and diamond(w, P) = ∃ w'. … is vacuously false (the existential over an empty set). This is not a design choice but the standard semantics of base multi-modal logic K(m): by the DL↔modal correspondence (Schild, “A correspondence theory for terminological logics,” IJCAI 1991), the description logic ALC is a notational variant of K(m), in which ∀r.C (= box) is vacuously true at an element with no r-successors — exactly standard DL ∀-rule behavior. It is also what Modal.lean’s box/diamond compute. The executor therefore anchors a box rule over every frame world — a dead-end world’s vacuously-true box derives the head — and a diamond rule derives nothing at a dead-end. (Anchoring only over worlds-with-successors would silently drop a dead-end’s vacuously-true box — an under-derivation, not the faithful semantics.)

The frame split. This dead-end case is specific to slice 1’s generic frame. Slice 1’s explicit accessible frame is base K: arbitrary, dead-ends allowed, hence vacuous box. The standpoint frame (ModalFrame.lean’s reflexive-transitive reach closure) is S4 — reflexive, hence serial — so every world reaches at least itself and there are NO dead-ends; the vacuous-box case cannot arise there. The two frames are distinct modal logics over distinct accessibility relations, and slice 1 is the K one.

Value algebra — why K3 is correct for one frame

spec/lean/Argon/Standpoint/Consistency.lean mechanizes the strict consistency policy and proves (append_strict_inK3) that under the default strict policy every cell stays in the K3 fragment {Is, Not, Can}. The information-determined-inconsistent value Both arises only at cross-standpoint federation (append_strict_fails_iff: a strict append fails exactly when it would create a (T, F) conflict, and that conflict is the cross-source case). Slice 1 is a single frame under strict consistency, so by this invariant every label is in K3. The carrier is Truth4 (oxc-protocol/src/storage.rs), with info_join the AFT bilattice operation; slice 1 uses only the K3-closed sub-table (Both never produced).

  • Clash = a proposition forced to both Is and Not at one world — the K3 inconsistency strict rejects.
  • Can (open-world unknown) = an open branch, not a clash. This is the open-world modal trap: box(P) holds only if P is Is at every accessible world; a Can/unknown world does NOT satisfy box (unknown ≠ true).

DL ≅ modal correspondence (why a role tableau ports)

Schild 1991: a tableau over an accessibility role is exactly a modal tableau — ∃accessible.P = diamond P, ∀accessible.P = box P. This is why the description-logic role-tableau machinery (studied from a separate read-only DL reasoner as an architectural reference) ports to Argon’s modal frame, re-skinned to Argon’s Truth4 label shape. No DL-reasoner code is copied; the pattern is ported.

Machinery (ported architecture, re-skinned)

The portable, proven tableau machinery — adapted, never copied:

  • Trail-based zero-copy undo + dependency-directed backjumping. Every mutation (a label cell set, an edge added, a node created) pushes a trail entry; undo replays the trail in reverse to a mark. Backjumping computes the earliest branch the current clash depends on and unwinds to it, skipping irrelevant choice points. This is the dominant performance win over cloning state per branch.
  • The expansion loop with dirty-node tracking and pre-computed rule data. Only nodes whose label changed are re-processed; the rule that fires on each label cell is classified once. The ∃/∀-rules of DL become the diamond/box-rules over accessible.
  • Blocking. A single explicit frame is finite (explicit accessible facts), so slice 1 terminates by the finite frame. Subset/equality blocking is still implemented for the general/cyclic case so a cyclic accessible relation terminates. The blocking comparison is K3-label info-order dominance, not set inclusion: a node is blocked by an ancestor whose label dominates it in the information order.
  • Clash detection. Adapted to the K3 Is ∧ Not clash at a single world.

The DL-specific data shapes (concept-label bitvectors, SROIQ role algebra, absorption/NNF/EL pre-passes) are NOT ported — Argon’s label is Truth4-per- proposition over worlds.

Routing — narrowing the refusal, not dropping it

Today two sites refuse modals:

  1. translate_standpoint_modals (instantiate) refuses an unframed modal with OE1104 (InstantiateError::ModalNotEvaluated).
  2. The rule compiler (compile_atom) refuses a surviving AtomIR::Modal with OE1104 (RuleCompileError::ModalNotEvaluated) as a backstop.

Slice 1 inserts the explicit-Kripke-frame recognition: when the modal’s inner predicate is evaluated over a frame backed by std::kripke’s accessible, AtomIR::Modal is preserved (not translated, not refused), compiled to a new CompiledAtom::Modal { op, inner } variant, and handled by the KripkeExecutor. Every other shape — standpoint frame (translated as before), no frame / rigidity, rigid roles, nominals — KEEPS refusing OE1104. The refusal is narrowed to exactly slice 1’s complement, never silently accepted.

CompiledAtom is internal to oxc-reasoning and is NOT mirrored in any @[language_interface] Lean inductive, so adding CompiledAtom::Modal does not touch the Lean↔Rust drift gate. (AtomIR::Modal and ModalOp are already mirrored and unchanged.)

Soundness floor (the hard gate)

  1. Differential oracle. The KripkeExecutor’s result MUST agree with (a) the semi-naive Datalog executor on any program in the decidable overlap, and (b) the ModalFrame semantics — box(P) = the intersection (∀ over accessible), diamond(P) = the union (∃). A differential test runs over an explicit frame where box ≠ diamond (a proposition true at some accessible worlds, false or unknown at others) so a swap or collapse of the two operators fails it.
  2. Termination. Tested on a cyclic accessible relation — blocking must fire. A non-terminating tableau is a failure.
  3. K3 clash soundness / open-world box. box(P) holds only if P is Is at every accessible world; a Can/unknown accessible world must NOT satisfy box. Tested explicitly (the classic open-world modal trap).
  4. Scope refusal. Standpoint-frame, rigid-role, nominal, and classification- frame modals still refuse OE1104 — tested that slice 1 did not silently accept them.

Slice 2 — the Kripke frame fibred over standpoints

Slice 2 lifts the slice-1 single-frame modal tableau to the fibred composition of Argon’s two modal frames: it evaluates the explicit-Kripke box/diamond (slice 1’s tableau) independently per standpoint, then info-joins the per-standpoint K3 results across standpoints (the already-shipped FDE federation, §11 / Federation.lean). The four-valued Both arises exactly when two standpoints disagree on a modal fact — genuine perspectival disagreement — and nowhere else.

Why fibred, not a product (decidability)

A genuine product of two S4 modalities (S4×S4) is undecidable. Slice 2 deliberately avoids that boundary. The composition is a fibration: the Kripke accessibility relation is evaluated entirely within a single standpoint’s catalog (slice 1, unchanged), and the standpoint dimension enters only after the per-standpoint modal answer is fixed, as a flat info-join over the per-standpoint results. This is the fusion (independent join) of the two logics, not their product — decidable by the Wolter transfer theorem for fusions (Wolter, “Fusions of modal logics revisited,” 1998) composed with finite-frame model-checking of each per-standpoint Kripke frame (every explicit accessible frame is finite; slice 1 already terminates on it). The two accessibility relations never interleave: a standpoint boundary is never crossed inside a box/diamond expansion, and a Kripke world-step is never taken across standpoints. That isolation is the decidability argument and the soundness argument both.

Scope (held precisely)

  • In: the explicit std::kripke frame (slice 1’s box/diamond over accessible) fibred over a query’s across [...] standpoint set (or a standpoint {} block). Per-standpoint K3 result, info-joined across standpoints under the query’s FederationPolicy (paraconsistent: Both surfaces; strict: K3-projected at the boundary).
  • Out (still refused / not coupled): the classification / mutation- reachability frame (slice 3); rigid roles and nominals (slice 3); a genuine product or cross-nested box_standpoint(box_kripke(P)) (refused — see §“Cross-nesting guardrail”); a standpoint-frame modal and a Kripke modal composed in one operator (the cross-family coupling, refused).

The soundness crux — per-standpoint K3, then federate (Can vs Not)

For federation to manufacture the correct Both on genuine disagreement and never a false Both from mere ignorance, each standpoint’s modal result must reach federation as its faithful K3 value — Is / Not / Can — distinguishing determined-false from open-world-undetermined:

  • federate(Is, Not) = Both — genuine perspectival disagreement (one standpoint says the modal necessarily holds, another says it is determined-false). Correct.
  • federate(Is, Can) = Is — one standpoint confirms the modal; another simply does not know (its frame has an undetermined successor, no determined-false). This must not become Both. (Federation.lean federate_eq_both_iff: the result is .both iff some source said .both or two sources genuinely disagree — hasIs ∧ hasNot. A Can contributes to neither hasIs nor hasNot, so it cannot induce Both.)

The trap. Slice 1’s decide/decide_box/decide_diamond and its denotational oracle collapse Can → Not: decide_box returns Not both when an accessible successor is determined-false and when a successor is merely Can (open-world unknown). This collapse is correct for the single frame: slice 1’s derivation boundary is fail-closed (only Is derives the head, so Not and Can are indistinguishable there — both yield “no derivation”). But it is catastrophic at federation: a standpoint whose box(P) is genuinely Can (an accessible world is unknown, none determined-false), reported as Not, would federate with another standpoint’s Is to a false Both — a silent-wrong manufactured from ignorance.

Resolution (the linchpin — flagged for review). Slice 2 introduces a separate federation-outcome function that returns the faithful K3 value, WITHOUT changing slice-1’s single-frame projection. For box(P) at world w over a standpoint’s frame, scanning the accessible successors:

  • Is iff every accessible successor has P = Is (necessity confirmed);
  • Not iff some accessible successor has P = Not (a determined-false witness defeats necessity);
  • Can otherwise — no successor is Not, but some successor is Can (necessity is open-world undetermined: it could still go either way);
  • vacuously Is at a dead-end world (∀ over no successors), per the K(m) semantics slice 1 already pins.

The ordering matters: a Not successor dominates a Can successor — box is Not if any successor is determined-false, regardless of how many others are Can, because determined-false already defeats necessity. For diamond(P) at w (dual):

  • Is iff some accessible successor has P = Is (a witness);
  • Not iff every accessible successor has P = Not (every possibility foreclosed);
  • Can otherwise — no Is witness, but some successor is Can (a witness could still emerge);
  • vacuously Not at a dead-end (∃ over no successors).

This is the standard Kleene K3 reading of box = ⋀ / diamond = ⋁ over the three-valued successor labels (Is = ⊤, Not = ⊥, Can = the middle), with the dead-end conventions slice 1 fixes. It is computed directly from the frame (KripkeFrame::prop_at, which already returns the faithful Is/Not/Can), so it needs no change to the tableau procedure or its oracle. The per-standpoint federatable value is exactly this K3 value; slice-1’s fail-closed decide and its denotational oracle are untouched (slice 1’s single-frame contract is unchanged and its differential gate still holds).

A frame whose seed forces Is ∧ Not at one world is a clash (slice-1 strict-consistency rejection); that standpoint contributes nothing for the clashing cell (it does not contribute a determined value, i.e. it is treated as Can for that cell at federation — the strict-consistency reject is local to the one frame and must not poison the federation with a phantom determined value).

Routing — per-standpoint loop then federate

Two new pieces, both narrowing existing seams (no second engine, no second store):

  1. Frame-aware dispatch fix (closes a latent silent-wrong). translate_standpoint_modals (instantiate) previously checked is_explicit_kripke_modal only inside its roots.is_empty() branch — so a Kripke modal appearing inside an across [...] query or a standpoint {} block (roots non-empty) was mis-routed into the standpoint-frame Datalog translation (synth_standpoint_modal), silently producing a wrong extent instead of preserving AtomIR::Modal for the tableau. The fix checks is_explicit_kripke_modal first, independent of roots: a Kripke modal is preserved as AtomIR::Modal (→ tableau) in every standpoint context. A non-Kripke modal with no frame still refuses OE1104; a non-Kripke modal with a standpoint frame still translates as before.

  2. Per-standpoint query-routing loop. When a federated query carries a non-empty across set and a Kripke CompiledAtom::Modal, the runtime, for each standpoint s in the across set, materializes s’s per-standpoint catalog (materialize_predicates_for_standpoint(s) — DEFAULT ∪ standpoint-own), runs the slice-1 KripkeExecutor over that per-standpoint catalog, and reads the faithful K3 federatable value per head tuple. The contributions are then info-joined by the already-shipped query_derive_federated under the query’s FederationPolicy. The federation for a modal head bypasses the plain (in_pos, in_neg) classify_source_rows path — that path can only ever produce Is/Can for a modal head (the executor’s fail-closed projection writes Is-only), so it cannot carry the Not federation needs.

Cross-nesting guardrail (non-negotiable, from the decidability theory)

Cross-nesting of the two modal families — box_standpoint(box_kripke(P)) and its converse — is the coupling the undecidability boundary lives at; only additive (fibred / fusion) composition is sound and decidable. This is already refused by the existing nested-modal gate (lower_modal/atom_lower.rs): the gate refuses any modal whose inner atom_contains_modal, uniformly, before frame recognition runs — so box(box(…)), diamond(box(…)), and the cross-family box(box_kripke(…)) are all rejected with the modal refusal at lowering time. The cross-family case is a special case of that uniform refusal; no extension is required. Slice 2 pins it with a dedicated cross-family test so a future relaxation of the gate cannot silently open the undecidable door.

Soundness floor (slice 2)

  1. Differential oracle (fibred). Extend slice-1’s denotational oracle to the fibred case: run the per-standpoint tableau, take each standpoint’s faithful K3 federatable value, info-join them, and compare against a denotational fibred oracle — box/diamond evaluated per standpoint over each standpoint’s frame (the K3 reading above), info-joined. The test ranges over frames where standpoints disagree (→ Both), agree (→ K3), and where one standpoint is Can/unknown while another is Is (→ Is, not Both). The Can-vs-Not distinction is the central oracle-covered property.
  2. Mis-routing closed. A Kripke modal in an across / standpoint context routes to the tableau, not the standpoint-frame translation (tested).
  3. Cross-nesting refused. box_standpoint(box_kripke(P)) (and converse) are refused (tested).
  4. Soundness factoring. Slice-2 soundness = slice-1 tableau soundness (the per-standpoint K3 value is the slice-1 frame semantics, distinguishing the Can it previously projected away) × Federation.lean federate_eq_both_iff (federation is Both iff genuine disagreement) × a fibred-isolation argument (a standpoint boundary is never crossed inside a modal expansion, a Kripke step is never taken across standpoints — so the two frames compose additively, not as a product). Faithful to ModalFrame.lean / Modal.lean / Federation.lean / Consistency.lean.

Roadmap (NOT built here)

  • Slice 3 — rigid roles, nominals, the classification/rigidity frame. The rigidity frame (worlds = configurations an individual’s classification holds in), rigid roles, and nominals (singleton concepts). The full §11.2 static-discharge table.

Each slice lifts a strictly smaller piece of the OE1104 refusal; until a slice ships, its complement keeps refusing.

Module placement

The tableau lives as a tableau module inside oxc-reasoning (oxc-reasoning/src/tableau/), alongside the other executors. It is not a new top-level crate: the executor is one more backend behind TierExecutor, it shares the catalog and Truth4 carrier, and a new top-level directory is not warranted for slice 1.