The case
Phase 1 shipped the lifter. Phase 2 shipped the projector + structural round-trip parity. Phase 3 ships the validator: evaluate(), checkConsistency(), the No-Collapse Guarantee, the unverifiedAxioms honest-admission surface, and the loadOntology-driven session lifecycle. The Phase 3 demo argues that checkConsistency() correctly catches Horn-detectable contradictions across the canonical adversarial corpus, with explicit discrimination between Horn-decidable inconsistency, non-Horn-fragment-escape, and the catchall silent-pass class.
Internal canary discipline — No-Collapse Guarantee. Three adversarial fixtures exercise the three discriminating outcomes: a Horn-decidable inconsistency (must return consistent: 'false'), a non-Horn inconsistency (must return 'undetermined' with populated unverifiedAxioms — honest admission of the Horn-fragment limit per spec §8.5.5), and a catchall silent-pass adversary (must NOT return consistent: 'true' regardless of which mechanism rules it out). Together they catch the canonical silent-failure mode: checkConsistency returning consistent: true on a KB classical FOL would judge inconsistent. A separate sub-case (A.7) verifies the API §8.1.2 hypothetical-axiom non-persistence guarantee via the two-call protocol.
Why this matters. A consistency checker that catches the Horn-decidable adversary but silently passes the non-Horn adversary leaks the No-Collapse contract: consumers see
consistent: 'true' on KBs that classical FOL would judge inconsistent. The three engineered adversaries together close the silent-failure-mode regression-density check — a result the corpus stub-evaluator at Phase 2 could not establish because stub semantics are bounded-Horn-only.
What this demo does NOT claim. Phase 3 does NOT yet ship Layer A consistency-check parity (the case where the implementation's verdict on a known-consistent Horn-translatable fragment matches the spec §8.5.1 affirmative-verdict requirement). The v0.1 implementation's Horn-fragment classifier flags simple disjointness as
unverifiedAxioms rather than affirming consistency on subsets where no individual triggers the body — a Layer A consistency-affirmation gap. Per the architect's Q-Frank-Step9-A corrective ruling 2026-05-10, the demo does not claim what the implementation cannot demonstrate; the closure path is forward-tracked via [project/v0.2-roadmap.md](../project/v0.2-roadmap.md) (v0.2 ELK closure absorbs the Horn-fragment classifier refinement). Phase 4's demo will exercise consistency-rejection on the BFO Disjointness Map (the Continuant ⊓ Occurrent canary firing consistent: 'false'); the consistency-affirmation direction waits on v0.2 ELK.
Phase 3 implementation state at this build
Phase 3 lands the validator pipeline in nine sequenced steps. This demo exercises what the Phase 3 exit deliverables expose; deferred refinements are listed in “What Phase 3 does NOT yet do.”
Shipped at Phase 3 exit.
- Session lifecycle per API §2 —
createSession/disposeSession; lazy Tau Prolog allocation on firstloadOntologycall; session-required + session-disposed gates on every consuming API. loadOntology(session, ontology, config?)per API §5.5 — lifts the input ontology, translates FOL→Prolog clauses per ADR-007 §11 + ADR-013 visited-ancestor cycle-guard pattern, asserts clauses into the session's Tau Prolog state, accumulatescumulativeAxioms+cumulativeSkippedper the multi-call session model.evaluate(session, query, params?)per API §7.1 — bounded-SLD resolution with the per-query 10K step cap (default per API §7.2) and per-session aggregate cap. ReturnsEvaluationResultwith the three-stateresultfield.checkConsistency(session, axiomSet?, params?)per API §8.1 — three-stateConsistencyResultper Q-3-Step6-A option (α) editorial correction;FOLFalse-in-head inconsistency proof for Horn-decidable contradictions;cumulativeSkipped-driven Horn-fragment-escape detection populatingunverifiedAxioms; hypothetical-axiom case (axiomSetparticipates per API §8.1.2 with non-persistence guarantee).- No-Collapse Guarantee surface per spec §8.5 — three-outcome check (
'true'/'false'/'undetermined') with the'undetermined'sub-cases differentiated byreasoncode (step_cap_exceededvscoherence_indeterminate);unverifiedAxiomspopulated with the FOL axioms outside the Horn-checkable fragment when reason iscoherence_indeterminate;witnessespopulated with minimal inconsistent subsets whenconsistent: 'false'. - Cycle-guarded Prolog clause emission per ADR-013 — visited-ancestor pattern catches the six identified cycle-prone predicate classes (transitive role + inverse, equivalent classes, role hierarchy with transitivity, …) before Tau Prolog enters non-terminating SLD recursion. Cycle detection escalates to a
SkippedAxiomentry with diagnostic scope notes. - Reserved reason-code surface per API §7 — 17 frozen reason codes at v0.1.7 +
no_strategy_appliesadded per Q-3-C; reuse-bounded-by-semantic-state-alignment discipline applied at Step 4 (open_world_undetermined) and Step 6 (inconsistent) per banked principles inarc/AUTHORING_DISCIPLINE.md.
Deferred to Phase 4+. Layer A consistency-affirmation closure (Horn-fragment classifier refinement distinguishing Horn-expressible-but-not-exercised from non-Horn-expressible — v0.2 ELK closure path per
project/v0.2-roadmap.md); ARC-content-driven inference (BFO 2020 Phase 4; IAO Phase 5; CCO Phase 6 per ADR-009 six-module expansion); regularityCheck(A, importClosure) import-closure machinery (Phase 4 entry packet); ELK / SROIQ external reasoner integration (v0.2 escape clause per spec §0.1 three-tier framing); per-class Skolem-witness satisfiability checking refinements beyond Step 6+ minimum (forward-tracked); the six remaining LossType trigger-matchers (arity_flattening, closure_truncated, una_residue, coherence_violation, bnode_introduced, lexical_distinct_value_equal — their machinery exists; trigger-matchers arrive in subsequent phases per the LossType-by-phase split). Forward-track items routed to Phase 4 entry packet per the Phase 3 exit retro election + Q-Frank-Step9-A corrective ruling.
Case A — No-Collapse Guarantee canary discipline
Three adversarial fixtures exercise the three discriminating outcomes of checkConsistency() against the No-Collapse Guarantee surface. Each fixture is engineered to catch a specific silent-failure failure mode; together they discriminate Horn-decidable inconsistency from non-Horn-incompleteness from the catchall silent-pass class.
Why this matters for stakeholders. A consistency checker is only useful if its
'true' verdict can be trusted. A naive Horn-only checker that runs SLD resolution to fixed-point and silently returns 'true' when no contradiction is derivable is useless on real KBs — real KBs contain disjunction, existential quantifiers, and property-chain constraints that the Horn fragment cannot exhaust. OFBT's discipline: when the check cannot decide the verdict, it must say so ('undetermined' with populated unverifiedAxioms), not silently pass. Case A is the regression-density check against the silent-pass class.
A.1. Inputs
Three fixtures from tests/corpus/:
- nc_self_complement —
EquivalentClasses(ParadoxClass, ObjectComplementOf(ParadoxClass)). Lifts to ∀x. (C(x) ↔ ¬C(x)). Horn-decidable contradiction; expected verdictconsistent: 'false',reason: 'inconsistent'. - nc_horn_incomplete_disjunctive —
SubClassOf(A, ObjectUnionOf(B, C))+ B⊂D + C⊂D +DisjointClasses(A, D)+ClassAssertion(A, alice). Classically inconsistent through disjunctive case-analysis (non-Horn). Expected verdictconsistent: 'undetermined',reason: 'coherence_indeterminate',unverifiedAxiomspopulated with the disjunctive + disjointness axioms. - nc_silent_pass_canary — engineered classically-inconsistent KB through compounded non-Horn pathways (disjunctive partition + existential-witnessing + inverse + property-chain). Expected verdict: MUST NOT be
consistent: 'true';'false'or'undetermined'both acceptable.
Three input ontologies (structured per API §3.1)
Loading fixtures…
A.2. Run the consistency checks
Loading bundle…
A.3. nc_self_complement — Horn-decidable inconsistency
The canonical equivalent-to-complement contradiction is decidable in the Horn-checkable fragment per spec §8.5.1: a Skolem witness for satisfiability + the iff unfolding gives C(c)∧¬C(c)→⊥. The check must return consistent: 'false' with the inconsistent reason; unverifiedAxioms must be empty (no axioms outside the fragment).
checkConsistency result
Press Run checkConsistency on all three fixtures to invoke.
A.4. nc_horn_incomplete_disjunctive — non-Horn inconsistency surfaced
The disjunctive-consequent axiom + DisjointClasses contradiction-trigger drives a classical inconsistency through case-analysis the Horn fragment cannot perform. The check must return consistent: 'undetermined' with reason: 'coherence_indeterminate' AND unverifiedAxioms populated with the disjunctive SubClassOf (the proximate non-Horn-fragment-escape; the disjointness DisjointWith(A, D) is Horn-expressible and not surfaced because the indeterminacy arises from the case-analysis the disjunctive consequent forces, not from the disjointness itself) — honest admission per spec §8.5.5 + API §8.1.1. A 'true' verdict here is the silent-pass failure mode for non-Horn inconsistency. Per Q-Frank-Step9-A Ask 2 (architect ruling 2026-05-10): the fixture's expectedUnverifiedAxiomsMinCount was amended from 2 to 1 because the implementation is correct on the merits — only the disjunctive-consequent axiom is non-Horn; the disjointness is Horn-expressible. The earlier "count-divergence forward-tracked" framing was withdrawn at the corrective ruling.
checkConsistency result
…
A.5. nc_silent_pass_canary — the catchall silent-pass adversary
A classically-inconsistent KB engineered through compounded non-Horn pathways. The canary's primary assertion is the negative one: MUST NOT return consistent: 'true'. Both 'false' (a tableau-extended implementation reaching the contradiction) and 'undetermined' with populated unverifiedAxioms (the v0.1 Horn-only path correctly admitting Horn-fragment-escape) are acceptable. 'true' is unacceptable regardless of the mechanism that would have ruled it out.
checkConsistency result
…
A.6. Discrimination matrix
The three fixtures together discriminate the No-Collapse behavioral surface across the in-fragment / non-Horn-incompleteness / silent-pass dimensions. A consistency checker that catches one but not the others is incomplete; OFBT's Phase 3 implementation must catch all three.
What this case establishes (and what it does not). Per architect Q-Frank-4 ruling 2026-05-07, the No-Collapse canary is a regression-density check against engineered failure modes, not a soundness argument. It catches the silent-pass behaviors the test author thought to construct; it does not certify that no other Horn-undetectable inconsistency exists in arbitrary KBs. The argument the canary makes is exactly: on these three engineered KBs, the implementation's verdict matches the No-Collapse contract. A full soundness argument would require either external reasoner integration (v0.2 ELK) or a structural proof over the FOL fragment. Per spec §0.1 three-tier framing, OFBT's v0.1 contract is "Horn-checkable inconsistency caught + non-Horn-fragment-escape honestly admitted"; this is exactly what Case A verifies.
A.7. Hypothetical-axiom non-persistence sub-case
Phase 3's checkConsistency(session, axiomSet) participates a hypothetical axiomSet in the consistency check WITHOUT persisting it in the session per API §8.1.2. A subsequent checkConsistency(session) call must see only the original session state. This sub-case demonstrates the contract on the hypothetical_clean fixture: a clean (consistent) hypothetical extension that narrows alice's membership without contradiction. The non-persistence guarantee is genuine Phase 3 content unrelated to the (pulled) Layer A consistency-check parity case — preserved here to keep its visibility per the Q-Frank-Step9-A corrective ruling.
Hypothetical extension input (FOL axiomSet per API §8.1.2)
Loading fixture…
Loading bundle…
Two-call results (Call 1 with axiomSet, Call 2 without)
Press Run two-call hypothetical protocol to invoke.
Why the two-call protocol is load-bearing. Per the
hypothetical_non_persistence.fixture.js design rationale: an implementation that incorrectly persists the hypothetical axioms (e.g., assertz without matching retract; or correctly retracts axioms but leaves derived facts behind; or mutates session state via shared references) silently corrupts the session for subsequent calls. The two-call protocol catches all three failure modes — if any axiom or derived fact persists, Call 2's verdict differs from the expected base-KB verdict.
What Phase 3 does NOT yet do
Phase 3 ships the validator pipeline + No-Collapse Guarantee surface + 16 corpus fixtures (4 No-Collapse adversarial + 4 hypothetical-axiom + 2 step-cap + 4 strategy-routing + 2 closed-predicate / cycle). The remaining gaps live in Phase 4+.
- BFO 2020 core ARC module + BFO Disjointness Map — Phase 4. The Phase 3 BFO Layer A consistency-check uses the standard-OWL subset only; the Phase 4 demo's Case A canary fires
consistent: 'false'on Continuant∩Occurrent + introduces Layer B (bfo-2020.clif) parity citations. - IAO information-bridge ARC module — Phase 5.
- CCO realizable-holding + mereotopology + measurement + aggregate + organizational + deontic ARC modules — Phase 6 per ADR-009 six-CCO-module expansion.
- OFI deontic ARC module + compatibility shim + bundle budget enforcement + coverage matrix CI — Phase 7 per ADR-008 Option A (OFI deontic deferred to v0.2 inside Phase 7's compat-shim landing).
- Per-class Skolem-witness satisfiability refinement — forward-tracked beyond Step 6+ minimum. The Phase 3 implementation handles
FOLFalse-in-head inconsistency proofs (sufficient for the lifted form ofDisjointClasses/DisjointWithcontradictions); deeper Skolem-driven satisfiability checks for arbitrary unsatisfiable class expressions are a future cycle. regularityCheck(A, importClosure)import-closure machinery — Phase 4 entry packet. Phase 2's projector chain projection emitsregularity_scope_warningunconditionally; Phase 4 closes this for chains regularity-confirmed under loaded ARC modules' import closure.- External reasoner integration (ELK / SROIQ) — v0.2+ per spec §0.1 three-tier framing escape clause. Phase 3's v0.1 contract is Horn-checkable + honest-admission of Horn-fragment-escape; v0.2 ELK closes the EL-profile gap and v0.3+ SROIQ closes the rest. Closure commitments consolidated in
project/v0.2-roadmap.md. - Layer A consistency-affirmation gap — v0.2 ELK closure per
project/v0.2-roadmap.md. The v0.1 implementation's Horn-fragment classifier flags simple disjointness asunverifiedAxiomsrather than affirming consistency on subsets where no individual triggers the body. Per the Q-Frank-Step9-A corrective ruling 2026-05-10, the demo does NOT claim Layer A consistency-check parity (the case was pulled from the demo per the banked principle that demos do not claim what the implementation cannot demonstrate). v0.2 ELK closure absorbs the Horn-fragment classifier refinement (distinguishing Horn-expressible-but-not-exercised from non-Horn-expressible) alongside ELK's broader Horn-fragment expansion. - Six remaining LossType trigger-matchers — the audit-artifact machinery supports all 8 LossTypes; trigger-matchers for
arity_flattening(Phase 4 BFO ternary parthood),closure_truncated(Phase 3 evaluator-time concern, partially landed),una_residue(Phase 3 evaluator-time concern),coherence_violation(Phase 3 No-Collapse adversarial corpus),bnode_introduced(Phase 3 evaluator-derived Skolem introduction),lexical_distinct_value_equal(Phase 4 datatype handling) phase in across the build sequence. - Case C — Lossy round-trip demonstration — Phase 4 exit deliverable per Q-Frank-Step9-A Ask 4 (architect ruling 2026-05-10). The Annotated Approximation strategy + Loss Signature ledger + Recovery Payload artifacts have been shipping since Phase 2 (
naf_residueandunknown_relationtrigger-matchers) but have never been demonstrated in a per-phase demo. Phase 4 demo's Case C will exercise lossy round-trip against real Annotated Approximation output (BFO ternary parthood surfacesarity_flattening; CCO content surfaces additional triggers); committed as Phase 4 exit deliverable, not forward-track. - Phase 4 entry packet forward-tracks — routed at Phase 3 exit retro + Q-Frank-Step9-A corrective ruling 2026-05-10: parallel-registry reconciliation (DECISIONS.md ADR-NN vs spec §13 ADR-NN); substantive-scope-weighting methodology refinement (counter at 5 vs ~3 projected); at-risk-tag-conservatism observation; cycle_equivalent_classes Class-3 fixture re-binding; nc_bfo_continuant_occurrent + nc_sdc_gdc Phase-4-deferred fixtures; LossType trigger-matcher subsystem cleanup; Realization regularity-check upgrade; Phase 2 reactivation surface as Phase 4 demo opening (cumulative-discipline-credibility); purpose-built Layer A consistency-check parity fixture question; banking-correction discipline retro analysis. NOT inherited: the disposition-split discipline (withdrawn per Q-Frank-Step9-A Ask 5).
Provenance
- Spec sections
- Behavioral spec §0.1 (three-tier framing — v0.1 Horn-checkable / v0.2 ELK / v0.3+ SROIQ); §5.4 (resolution depth bound); §6.3 (default OWA negation +
closedPredicates); §8.1 (round-trip parity criterion); §8.2 (consistency check semantics); §8.5 (No-Collapse Guarantee); §8.5.1 (Horn-checkable fragment scope); §8.5.2 (three-outcome check + outcome ordering); §8.5.4 (limitations — sound for Horn-expressible contradictions); §8.5.5 (surfacing Horn-fragment limit to consumers). API spec §2 (session lifecycle); §5.5 (loadOntology); §7.1 (evaluate); §7.2 (per-query step cap); §7.4 (configurable throw-on-cap); §8.1 (checkConsistencysignature + ConsistencyResult); §8.1.1 (unverifiedAxiomsfield + honest-admission discipline); §8.1.2 (hypothetical-axiom case + non-persistence guarantee); §10.3 (session-required + session-disposed errors). - Case A No-Collapse adversarial fixtures
tests/corpus/nc_self_complement.fixture.js(Horn-decidable inconsistency; closed at Step 9.4-amendment-4 commit 7526973);tests/corpus/nc_horn_incomplete_disjunctive.fixture.js(non-Horn-disjunctive Horn-fragment-escape;expectedUnverifiedAxiomsMinCountamended 2 → 1 per Q-Frank-Step9-A Ask 2 ruling 2026-05-10);tests/corpus/nc_silent_pass_canary.fixture.js(catchall silent-pass adversary). All three atverifiedStatus: Verifiedat Phase 3 exit per the Step 9.3 promotion pass.- A.7 hypothetical-axiom sub-case fixture
tests/corpus/hypothetical_clean.fixture.js— clean (consistent) hypothetical extension; positive control for thecheckConsistency(session, axiomSet)non-persistence guarantee per API §8.1.2. Sibling fixtures (test suite, not exercised in demo):hypothetical_inconsistency,hypothetical_horn_incompleteness,hypothetical_non_persistence.- Case B (Layer A consistency-check parity) — PULLED per Q-Frank-Step9-A 2026-05-10
- Case B was authored in earlier drafts of this demo using
tests/corpus/p1_bfo_clif_classical.fixture.js. Per the architect's Q-Frank-Step9-A corrective ruling 2026-05-10 (Ask 1), the case was pulled because the v0.1 implementation does not yet satisfy spec §8.5.1's required affirmative verdict on this canonical positive control. The Layer A consistency-affirmation gap is forward-tracked viaproject/v0.2-roadmap.md(v0.2 ELK closure path), not via soft demo framing. The fixture stays at its existingverifiedStatus: Verifiedstatus for Phase 1 lift correctness + Phase 2 round-trip parity (those parity claims still hold); Phase 3 consistency-check parity is not claimed. - Implementation
src/composition/check-consistency.ts—checkConsistency()three-state surface +FOLFalse-in-head inconsistency proof + Horn-fragment-escape detection viacumulativeSkippedaggregation + hypothetical-axiom non-persistence semantic.src/composition/evaluate.ts—evaluate()bounded-SLD invocation + per-query step cap.src/composition/load-ontology.ts—loadOntology()lifecycle + FOL→Prolog translation orchestration.src/composition/session.ts—createSession/disposeSession+ cumulative axiom/skipped tracking.src/kernel/fol-to-prolog.ts— FOL→Prolog clause translator per ADR-007 §11 + ADR-013 visited-ancestor cycle-guard pattern.src/kernel/evaluate-types.ts— EvaluableQuery + EvaluationResult type surface.- Test runner
tests/evaluate-phase3.test.ts—evaluate()+checkConsistency()tests against the No-Collapse adversarial corpus + hypothetical-axiom + step-cap + strategy-routing fixtures.tests/determinism.test.ts+tests/no-network.test.ts+tests/snapshot.test.ts— spec tests (unmodified per the operational boundary).- Phase 3 entry packet + step-N micro-cycles
project/reviews/phase-3-entry.md— ratified entry packet + 9-step ledger + corpus-before-code 8/8 split per Q-3-E.project/reviews/phase-3-step3-architectural-gap.md(loadOntology API §5.5 + ADR-007 §11 placement).project/reviews/phase-3-step4-architectural-gap.md(cwa_open_predicate reason-code reuse + verification ritual operationalized).project/reviews/phase-3-step5-architectural-gap.md(ADR-013 visited-ancestor pattern).project/reviews/phase-3-step6-architectural-gap.md(three-state ConsistencyResult + reason-code reuse forinconsistent).project/reviews/phase-3-retroactive-corrective.md(FOL @type discriminator corrections in 4 hypothetical fixtures).project/reviews/phase-3-step9-architectural-gap.md(Q-3-Step9-A original ruling + Q-Frank-Step9-A corrective overlay 2026-05-10).project/reviews/phase-3-reactivation-results.md(per-canary publication artifact: 3× survived against realevaluate()).- Stakeholder critique + corrective ruling
demo/Phase3DemoCritique.md— Frank's stakeholder critique 2026-05-10 surfacing the Layer A "documented v0.1 spec-divergence" framing concern + the disposition-split discipline post-hoc-canonization concern + the count-divergence forward-tracking concern. Architect's Q-Frank-Step9-A corrective ruling 2026-05-10 issued 3 banking withdrawals + 7 new bankings + 1 meta-banking; this demo's Case B pull, count-divergence resolution, and ADR-007 §10 promotion all derive from that ruling. Frank's letter banked as canonical exemplar of the post-hoc-discipline-canonization risk pattern.- ADR references
- ADR-002 (no external OWL reasoner dependency for v0.1 validation — v0.2 ELK escape clause). ADR-003 (structural round-trip parity as primary correctness criterion; the No-Collapse Guarantee per spec §8.5 is the orthogonal correctness criterion Case A exercises). ADR-007 §1 (cycle-guard layer translation), §10 (meta-typing-predicate elision — Accepted at Q-Frank-Step9-A Ask 3 ratification 2026-05-10), §11 (FOL→Tau Prolog clause translation rules per-variant table). ADR-010 (vendored canonical source license-verification discipline). ADR-011 (audit-artifact
@idcontent-addressing). ADR-013 (visited-ancestor cycle-guard pattern; ratified Step 5 architectural-gap micro-cycle 2026-05-08; six cycle-prone predicate classes). - v0.2 closure-path consolidation
project/v0.2-roadmap.md— consolidated artifact listing every "v0.X closes Y" commitment from across Phases 1-3 with source phase / source gap / scope / owner / timeline; authored at Phase 3 close per Q-Frank-Step9-A Ask 6 ruling 2026-05-10 to phase out the soft "v0.2 ELK closes that" placeholder pattern. The Layer A consistency-affirmation gap (the case Case B was pulled for) is the load-bearing entry.- Authoring discipline
arc/AUTHORING_DISCIPLINE.md— SME pre-handoff verification ritual (8 categories; binding from Phase 3 Step 4 forward); Phase 3 Banked Principles section (~48 principles transcribed verbatim per the verbatim-transcription discipline; cycle-stratified by entry packet, Step 3-6 micro-cycles, retroactive corrective, Step 9 architectural-gap with Q-Frank-Step9-A corrective overlay including 3 banking withdrawals + 7 new bankings + 1 meta-banking).