OFBT Phase 2 Demo

Two correctness arguments: (A) class-expression reconstruction canary, (B) BFO/CLIF Layer A structural round-trip parity.

The case

Phase 1 shipped the lifter (OWL → FOL). Phase 2 ships the projector (FOL → OWL) and closes the round-trip. The Phase 2 demo argues both that the projector reconstructs the right shape on a known-difficult construct (class expressions) AND that the round-trip preserves canonical OWL semantics against a published external ground truth.

  1. Internal canary discipline. The projector's pattern-match correctly reconstructs the input shape from the lifted FOL. The test suite asserts both the right shape's presence after round-trip and the wrong shape's absence (no conflations between superficially-similar restriction kinds).
  2. External CLIF structural round-trip parity. A BFO 2020 OWL fragment is lifted to FOL, then projected back to OWL. The projected OWL shape is parity-checked against the input AND each axiom's canonical CLIF semantics from the W3C OWL CLIF axiomatization. "Structural" is load-bearing here: the v0.1 contract is content-equivalence at the lifted-FOL level modulo the Loss Signature ledger (spec §8.1). Stronger semantic senses (model-theoretic, axiomatic, entailment-preserving) are deferred to v0.2+ when Phase 3's evaluate() ships.
Why both matter. A round-trip that reconstructs surface shape but swaps semantic content (e.g., someValuesFrom ↔ allValuesFrom) passes naive equality but produces wrong inferences downstream. A round-trip that preserves OWL surface but diverges from canonical CLIF passes self-referential checks but doesn't satisfy the standard. Both disciplines together catch failure modes neither catches alone.

Phase 2 implementation state at this build

The projector lands in stages. This demo exercises only what is shipped today; deferred constructs are listed in “What Phase 2 does NOT yet do.”

Shipped (Steps 1, 2, 3a, 3b, 3c, 4a on origin/main).
  • Direct Mapping single-axiom rules — ABox (Class / ObjectProperty / DataProperty assertions, plus reserved-predicate ABox SameIndividual / DifferentIndividuals at Step 3c) + TBox SubClassOf + RBox Symmetric / Transitive / Functional / Domain / Range / DisjointWith.
  • Pair-matching — EquivalentClasses (from a converse-SubClassOf pair); InverseObjectProperties (from a converse-implication pair).
  • Class-expression reconstruction — recursive reconstruction of intersection, union, complement, someValuesFrom, allValuesFrom, hasValue in the SubClassOf consequent (including class expressions in subClass position at Step 3c).
  • Annotated Approximation strategy at Step 4a — FOL shapes that don't map to OWL 2 DL Direct Mapping route to Annotated Approximation with structurally-valid Loss Signatures emitted.
  • LossSignature emission machinery — content-addressed @id per ADR-011 (ofbt:ls/<sha256-hex>); 2 of 8 LossType triggers shipping today (naf_residue for unmarked-negation contexts; unknown_relation for predicates outside loaded ARC modules); other 6 LossTypes' machinery present but trigger-matchers arrive in their corresponding later phases.
  • RecoveryPayload emission machinery — content-addressed @id per ADR-011 (ofbt:rp/<sha256-hex>); preserves original FOL for re-lifting.
  • The prefixes parameter per API §3.10.4 — output emits CURIE form when supplied; full URIs when omitted.
  • Frozen LOSS_SIGNATURE_SEVERITY_ORDER exported as a frozen array constant per API §6.4.1; mutation attempts throw.
Additionally shipped (Steps 4b, 5, 6, 7, 8).
  • Cardinality n-tuple matcher (Step 4b per ADR-012's architect-ratified Option β) — cardinality projects as native OWL Restriction with minCardinality / maxCardinality / cardinality fields under Direct Mapping. Phase 1's p1_restrictions_cardinality fixture round-trips byte-clean.
  • Strategy router with tiered fallthrough (Step 5 per spec §6.2) — explicit per-axiom strategy attribution; Tier-2 Direct Mapping → Tier-3 Property-Chain Realization → Tier-default Annotated Approximation → documented diagnostic for no-strategy-applies.
  • Property-Chain Realization (Step 6 per spec §6.1.2 + architect Q-Step6-1 ruling 2026-05-XX, parenthetically clarified per architect Q-Frank-3 ruling 2026-05-07) — chain detection with always-emit regularity_scope_warning Recovery Payload note per spec §6.2.1's literal framing. What v0.1 Realization actually emits: the OWL ObjectPropertyChain axiom and the regularity warning (unconditional in Phase 2; the architect ratified always-emit-with-loss-marker as the v0.1 form of Realization, not deferred-Realization). What Phase 4 Realization will emit: the chain axiom alone for chains regularity-confirmed under regularityCheck(A, importClosure) against loaded ARC modules' import closure; the warning persists only when the regularity check cannot certify the chain. The v0.1 contract is conservative: every chain ships with the warning until Phase 4's import-closure machinery can clear it.
  • roundTripCheck() (Step 7 per API §6.3 + spec §8.1) — wraps owlToFol + folToOwl composition with the spec parity-criterion contract; emits equivalent: true for clean round-trips; equivalent: true modulo Recovery Payloads for reversible-regime fixtures; equivalent: false with documented diff for true-loss fixtures.
  • Stub-evaluator harness + parity canaries (Step 8 per architect Q3 ruling 2026-05-06) — tests/corpus/_stub-evaluator.js implements bounded SLD resolution per the SME-authored leading-JSDoc contract; 3 parity canaries exercise round-trip query-preservation (positive entailment, OWA against CWA-collapse, cross-section visual-equivalence-trap). Phase 3 entry packet's gate item re-exercises every stub-evaluated canary against the real evaluate() per API §7.1.
Deferred to Phase 3+. Validator + evaluate() per API §7.1 (Phase 3 deliverable); checkConsistency() per API §8.1 + No-Collapse Guarantee per spec §8.5 (Phase 3); ARC-content-driven inference (Phase 4 BFO 2020 + Phase 5 IAO + Phase 6 CCO modules per ADR-009); regularity-check upgrade to regularityCheck(A, importClosure) with import-closure machinery (Phase 4 entry packet per architect Q-Step6-1 ruling); lifter ObjectPropertyChain support (Phase 3 OR Phase 4 per architect Q-Step6-3 — projector-only at Step 6; lifter support deferred until corpus demand surfaces).

Case A — Class-expression reconstruction canary

Class expressions (SubClassOf(C, ObjectSomeValuesFrom(P, F)), etc.) lift to nested FOL containing existentials, universals, conjunctions, and atom-on-individual patterns that look superficially similar. A naive shape-blind projector might collapse someValuesFrom to allValuesFrom, swap an existential filler for an intersection, or drop a hasValue's named individual to a class atom. OFBT's projector reconstructs each form correctly. The test suite asserts both the right shape's presence after round-trip and the wrong shape's absence.

Why this matters for stakeholders. A round-trip that emits OWL syntactically valid but semantically shifted (e.g., the input said “every Parent has at least one Person child” and the round-trip output says “every Parent's children are all Persons”) is a silent-failure bug whose downstream queries return wrong answers. The class-expression canary is the strongest single-construct test for projector correctness because the source FOL shapes for these constructs are pattern-match-distinguishable rather than structurally distinct.

A.1. Input ontology

Three SubClassOf axioms with class-expression consequents: someValuesFrom, allValuesFrom, hasValue. From tests/corpus/p1_restrictions_object_value.fixture.js.

Input OWL ontology (structured JS per API §3.1)
Loading fixture…

A.2. Run the round-trip

Loading bundle…

A.3. Lifted FOL (intermediate)

Lifted FOL (3 universal-implication axioms with class-expression-shaped consequents)
Press Run owlToFol → folToOwl to lift and project.

A.4. Projected OWL (round-trip output)

Projected OWL ontology (structured per API §3.1; should match input shape modulo prefixes / ontologyIRI placeholders)

A.5. Right shape present stub-validated

Each input axiom must round-trip to a SubClassOf with a Restriction consequent of the matching kind. The reconstruction recursively rebuilds the class expression from the lifted FOL.

Stub-validated. The verdicts in this panel are validated by the Phase 2 stub-evaluator harness (tests/corpus/_stub-evaluator.js, bounded-Horn-resolution per the SME-authored leading-JSDoc contract). Stub semantics are sufficient for structural shape verification but cannot exercise non-Horn entailments, deeper proof trees beyond the resolution bound, or model-theoretic equivalence. Phase 3 entry packet inherits the per-canary publication commitment per Q-Frank-4 ruling 2026-05-07: each Phase 2 stub-validated canary is re-exercised against the real evaluate() and the per-canary outcome is published (survived / failed-revealed-stub-limit / not-yet-reactivated). The SME risk estimate authored at Phase 3 entry tags each canary expected-to-survive / at-risk-horn-fragment-closure / requires-non-horn-evaluator.

A.6. Absence of known failure-mode patterns

The projected OWL must not exhibit any of the following conflation patterns — each is a class-expression silent-failure mode that a shape-blind projector would emit.

What this panel establishes (and what it does not). Per architect Q-Frank-4 ruling 2026-05-07, the wrong-shape canary is a regression-density check against known-bad patterns, not a soundness argument. It catches the specific failure modes the test author thought to look for; it does not certify that no other wrong shape is possible. A full soundness argument would require a structural proof over the OWL 2 DL grammar showing the projector cannot emit any wrong shape parametric over input, which is not a v0.1 deliverable. The canary is strictly better than no canary, and the failure modes listed here are exactly the silent-failure surface a logic-stakeholder would test for first; the authoring discipline as new failure modes are discovered is documented in the SME canary-extension note.

Case B — BFO/CLIF Layer A structural round-trip parity

A BFO 2020 OWL fragment is lifted to FOL, then projected back to OWL. The projected OWL is parity-checked against the input and against canonical Layer A CLIF semantics from arc/upstream-canonical/owl-axiomatization.clif (Fabian Neuhaus, 2009; vendored under CC BY 4.0 per owl-axiomatization.clif.SOURCE's license-verification block).

Layer A vs Layer B — framing. Per arc/upstream-canonical/README.md:
  • Layer A — OWL semantics in CLIF (what SubClassOf, Transitive, InverseObjectProperties etc. mean). Phase 2's projector preserves these semantics across the round-trip.
  • Layer B — specific ontology content in CLIF (BFO's Continuant, Occurrent, ternary parthood etc.). Phase 4+ ARC content covers this; Layer B is not exercised in Phase 2.
Phase 2's CLIF discipline cites Layer A only. Cumulative Layer A + Layer B coverage extends as ARC content lands.

B.1. Input ontology

BFO 2020 standard-OWL subset: 5 SubClassOf + 1 DisjointWith + 1 Transitive + 1 InverseOf = 8 axioms. From tests/corpus/p1_bfo_clif_classical.fixture.js (the same fixture exercised in the Phase 1 demo's Case B).

Input OWL ontology (structured JS per API §3.1)
Loading fixture…

B.2. Run the round-trip

Loading bundle…

B.3. Lifted FOL (intermediate — 9 axioms)

The 8 input OWL axioms lift to 9 FOL axioms because InverseObjectProperties decomposes into a bidirectional implication pair per ADR-007 §4. The projector's pair-matching re-collapses them in B.4.

Lifted FOL (9 axioms)
Press Run owlToFol → folToOwl to lift and project.

B.4. Projected OWL (round-trip output — back to 8 axioms)

Pair-matching identifies the bidirectional part_ofhas_part implication pair and emits a single InverseObjectProperties axiom. The TBox SubClassOf and DisjointWith axioms project as Direct Mapping single-axiom rules.

Projected OWL ontology (structured per API §3.1)

B.5. Structural round-trip parity panel stub-validated

For each input axiom: the projected OWL must contain a structurally-equivalent axiom. The check is shape-equivalence modulo the projector's emission of empty-array fields and source-provenance placeholders (Step 5 wires source-provenance threading; today's manifest carries projectorVersion: "OFBT-0.1.0" and operatingMode: "permissive").

Stub-validated. The verdicts in this panel are validated by the Phase 2 stub-evaluator harness — bounded-Horn-resolution sufficient for structural shape verification but not for non-Horn entailments or model-theoretic equivalence. Phase 3 reactivation re-exercises each canary against the real evaluate() and publishes per-canary outcomes per Q-Frank-4 ruling 2026-05-07.

B.6. Layer A CLIF parity panel

For each fixture-input axiom: the canonical CLIF axiom block from owl-axiomatization.clif paired with OFBT's lifted FOL. Multiple inputs that exercise the same OWL construct cite the SAME canonical block. Each badge reflects the verification state recorded in the fixture's clifGroundTruth array; badges are rendered at runtime from the fixture file's verificationStatus field, not hardcoded into this HTML.

How to verify these badges reflect reality. Same protocol as the Phase 1 demo: badges render at runtime from tests/corpus/p1_bfo_clif_classical.fixture.js's clifGroundTruth[i].verificationStatus field; the fixture's flip from [VERIFY] to Verified happened at Step 9.2 close (commit 209a531). The vendored CLIF file's SHA-256 (480193e9…5912) is pinned in the SOURCE sidecar; the LICENSE file's SHA-256 (f5b745ef…cc3f) and verified canonical commit (294fa416…b0cd) are pinned in the same sidecar's license-verification block per ADR-010 (Phase 2 entry verification ritual surfaced and corrected an unverified BSD-3-Clause assertion to the actual CC BY 4.0 license). See arc/AUTHORING_DISCIPLINE.md "SME-Persona Verification of Vendored Canonical Sources" + project/GOVERNANCE.md + project/DECISIONS.md ADR-010.

Per the architect-ratified meta-typing-predicate elision (ADR-007 §10): canonical CLIF includes (Class X) and (OWLObjectProperty R) typing predicates. OFBT's lifted FOL omits these per the encoding choice; the projector reconstructs without them. Round-trip is sound w.r.t. OWL semantics for v0.1.

Case C — Lossy round-trip (Annotated Approximation strategy)

Cases A and B exercise round-trip-clean fixtures where every input axiom maps cleanly to OWL 2 DL. Case C exercises the load-bearing Annotated Approximation strategy — the path the projector takes for FOL shapes that exceed OWL 2 DL expressivity. This is where OFBT's bidirectional value proposition matters most: a real consumer ingesting real ARC content will encounter expressivity gaps, and how OFBT handles them is the difference between honest-admission semantics and silent-loss semantics.

Why Case C exists. Per architect Q-Frank-6 ruling 2026-05-07 (acknowledging Frank's stakeholder critique §6: "the most consequential capability of the system is invisible in the demo"), Case C makes the Annotated Approximation strategy visible: stakeholders see the ObjectPropertyChain-style fallback OWL output, the LossSignature ledger entries, the RecoveryPayload contents, and the downstream-consumer protocol for re-evaluating against the FOL substrate. This is the strategy that handles "FOL shapes that don't fit OWL 2 DL," and Phase 4+ ARC content will exercise it heavily.

C.1. Input FOL axioms

A hand-authored FOL axiom set exercising both Annotated-Approximation-routing trigger paths in a single projector invocation:

From tests/corpus/strategy_routing_annotated.fixture.js. Projector-direct fixture (no lift step; the input is FOL directly). Demonstrates multi-Loss-Signature emission + the frozen severity-ordering contract.

Input FOL axioms array (structured per API §3.6)
Loading fixture…

C.2. Run the projection

Loading bundle…

C.3. Projected OWL (Annotated Approximation output)

Each input axiom emits a structurally-valid OWL annotation per spec §6.1.3 carrying ofbt:originalFOL (machine-readable FOL string), ofbt:roundTripID (content-addressed identifier), and ofbt:strategy ("annotated-approximation"). Consumer tooling that doesn't read the audit artifacts sees the annotation; consumer tooling that does read them recovers the FOL substrate.

Projected OWL ontology (Annotated Approximation form)
Press Run folToOwl on lossy FOL input to project.

C.4. Loss Signature ledger

At least two Loss Signatures expected per the fixture's prose contract. The implementation emits one unknown_relation LossSignature per unique uncatalogued predicate (per-predicate, not per-axiom), so this input emits 1 naf_residue (from the negation in axiom 1) plus 3 unknown_relation entries (one each for Person, KnownProfession, unfamiliarBond) = 4 total. Each carries a content-addressed @id (ofbt:ls/<sha256-hex> per ADR-011), a lossType field, severity rank, original FOL form, and machine-readable scope notes. The frozen LOSS_SIGNATURE_SEVERITY_ORDER exported per API §6.4.1 means consumers who request severity-ordered output get all naf_residue (rank 2) entries before any unknown_relation (rank 5) entries.

C.5. Recovery Payload set

Recovery Payloads preserve the FOL state for downstream re-lifting. Each carries a content-addressed @id (ofbt:rp/<sha256-hex> per ADR-011), the original FOL axiom (so the lifter can reconstruct it on re-lift), and the strategy that produced the payload.

C.6. Strategy attribution + severity-ordering contract

The Step 5 strategy router records each axiom's routing destination in the Projection Manifest. Both axioms route to annotated-approximation per spec §6.2's tiered fallthrough (Tier-2 Direct Mapping → Tier-3 Property-Chain Realization → Tier-default Annotated Approximation). The severity-ordering contract per API §6.4.1 is checked by sorting the emitted Loss Signatures and verifying the rank-monotonic invariant holds (all naf_residue entries precede all unknown_relation entries in the sorted ledger). The structural assertions match the fixture's prose contract (≥2 Loss Signatures with both expected lossTypes present); a fixture-vs-implementation count divergence note appears at the bottom of this panel for transparency.

C.7. Downstream consumer protocol

A consumer ingesting Annotated Approximation output has three paths, depending on what the consumer needs:

  1. Treat the OWL annotation as the canonical artifact. The structural annotation is valid OWL; OWL-only tooling consumes it as-is. The consumer accepts that the annotation captures FOL content the OWL syntax cannot natively express, and downstream OWL reasoners will treat it as opaque metadata.
  2. Read the Loss Signature ledger. The ledger names exactly what was approximated, with lossType and scopeNotes fields. A consumer running a Phase-3-warning surface (per Fandaws Consumer Requirement §7.1's honest-admission discipline) translates Loss Signatures into "this axiom required approximation" warnings for the user.
  3. Use the Recovery Payload to re-lift to FOL. The payload preserves the original FOL form. A consumer with FOL-capable inference (Phase 3+'s evaluate()) re-lifts the annotation, recovers the FOL state, and reasons over the substrate directly. This is the bidirectional translator's load-bearing claim: nothing is lost; everything is recoverable.
What this case establishes (and what it does not). Case C demonstrates structural Annotated Approximation behavior — the strategy fires, the audit artifacts emit with content-addressed identifiers, the severity ordering holds, the Recovery Payload preserves the FOL state. It does not certify that the re-lifted FOL is semantically equivalent to the original FOL under all classical-FOL evaluations; that's Phase 3+ semantic-equivalence territory per Q-Frank-1's structural/semantic distinction. The structural claim Case C makes is exactly: lift → approximate → annotate → recover gives back the same FOL structure modulo the recorded approximation. The semantic claim Phase 3 will make on top of that is: every entailment of the FOL state is preserved through the round trip.

What Phase 2 does NOT yet do

Phase 2 ships the projector + audit artifacts + strategy router + cardinality matcher + chain realization + roundTripCheck + 12 corpus fixtures + the parity-canary harness. The remaining gaps live in Phase 3+.

Provenance

Spec sections
Behavioral spec §6.1 (three-strategy projection — Direct Mapping / Property-Chain Realization / Annotated Approximation); §6.1.2 (Property-Chain Realization); §6.2 (strategy selection algorithm — Tier-2 / Tier-3 / Tier-default); §6.2.1 (regularity check + regularity_scope_warning contract); §6.3 (default OWA negation + closedPredicates Phase-3-deferred); §7 (audit artifacts taxonomy); §7.3 (RecoveryPayload reversible-regime contract); §7.5 (content-addressed @id discipline per ADR-011); §8.1 (round-trip parity criterion); §8.5 (No-Collapse Guarantee — Phase-3-deferred). API spec §6.1 (owlToFol); §6.2 (folToOwl); §6.3 (roundTripCheck); §6.4 (LossSignature / RecoveryPayload / ProjectionManifest schemas); §6.4.1 (LossSignature severity-ordering frozen contract + LOSS_SIGNATURE_SEVERITY_ORDER exported as frozen array); §7.1 (evaluate — Phase 3 deliverable; Phase 2 stub-evaluator harness fills the corpus-test gap); §3.10.4 (prefixes parameter).
Case A round-trip fixture
tests/corpus/p1_restrictions_object_value.fixture.js — the input ontology and expected lifted FOL (Phase 1 verified-status fixture exercised through Phase 2's projector for round-trip).
Case B Layer A fixture
tests/corpus/p1_bfo_clif_classical.fixture.js — BFO 2020 standard-OWL subset with clifGroundTruth citations against the vendored Layer A source.
Vendored Layer A canonical source
arc/upstream-canonical/owl-axiomatization.clif — W3C OWL CLIF axiomatization (Fabian Neuhaus, 2009; BFO repository, CC BY 4.0); 1660 lines, SHA-256 480193e9…5912. Provenance + license-verification block at owl-axiomatization.clif.SOURCE; verified canonical LICENSE commit 294fa416…b0cd, LICENSE SHA-256 f5b745ef…cc3f, master HEAD at verification 857be9f1…f3a7.
Implementation
src/kernel/projector.tsfolToOwl + matchSubClassOfWithExpression (Step 3b: class-expression reconstruction in SubClassOf consequent); reserved-predicate ABox + remaining TBox/RBox forms (Step 3c); Annotated Approximation strategy + LossSignature emission machinery + content-addressed @id generation per ADR-011 (Step 4a); matchInverseObjectPropertiesPair (Step 3a: pair-matching); single-axiom Direct Mapping pattern matchers (Steps 2 + 3a). src/kernel/projector-types.ts — audit artifact type definitions + frozen LOSS_SIGNATURE_SEVERITY_ORDER. src/kernel/canonicalize.tsstableStringify implementation supporting ADR-011 @id hash-input canonicalization.
Test runner
tests/projector-phase2.test.ts — Phase 2 round-trip tests against Phase 1 corpus + Phase 2 projection-specific fixtures (138+ tests passing through Step 4a).
Vendoring discipline
arc/upstream-canonical/README.md — Layer A vs Layer B framing. arc/AUTHORING_DISCIPLINE.md "SME-Persona Verification of Vendored Canonical Sources" subsection — verification ritual + license-verification-at-vendoring-time discipline (tightened per ADR-010, applies to all vendored canonical sources regardless of format).
ADR references
ADR-007 §1 (cycle-guard layer translation: lifter emits classical FOL), §4 (fresh-allocator-per-direction in liftBidirectionalSubsumption — load-bearing for the InverseObjectProperties two-axiom decomposition that Phase 2's pair-matching re-collapses), §7 (cardinality-witness Skolem convention — load-bearing for Step 4b's n-tuple matcher), §10 (banked: meta-vocabulary encoding choice). ADR-010 (vendored canonical source license-verification corrective action; CC BY 4.0). ADR-011 (audit-artifact @id content-addressing scheme — SHA-256 of stableStringify of discriminating fields; LossSignature 5-field set + RecoveryPayload 3-field set; lower-case hex; ofbt:ls/ + ofbt:rp/ prefixes; behavioral-contract evolution stricter than schema-contract evolution per Q-3 architect banking 2026-05-07). ADR-012 (cardinality routing — Direct Mapping with n-tuple matching per architect-ratified Option β at Step 4 spec-binding cycle 2026-05-07; Step 4b implementation per ADR-007 §7 lifted shapes).
Phase 2 entry packet
project/reviews/phase-2-entry.md — AMENDED + RE-CONFIRMED entry packet (architect 2026-05-06); §3.4 stub-evaluator harness contract; §3.7 + §10.8 cross-section defense-pair refinement; §6.1 license-verification gate item.
Step ledger context
Phase 2 progress through Step 4a: Steps 1 (skeleton), 2 (Direct Mapping single-axiom), 3a (pair-matching TBox + RBox), 3b (class-expression reconstruction), 3c (reserved-predicate ABox + remaining forms), 4a (Annotated Approximation + LossSignature emission + ADR-011 + Q-G fixture). Steps 4b (cardinality), 5 (strategy router), 6 (Property-Chain Realization), 7 (roundTripCheck) sequence next per the Phase 2 entry packet's Step ledger.