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.
- 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).
- 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.
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.”
origin/main).
- Direct Mapping single-axiom rules — ABox (Class / ObjectProperty / DataProperty assertions, plus reserved-predicate ABox
SameIndividual/DifferentIndividualsat 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
@idper ADR-011 (ofbt:ls/<sha256-hex>); 2 of 8 LossType triggers shipping today (naf_residuefor unmarked-negation contexts;unknown_relationfor predicates outside loaded ARC modules); other 6 LossTypes' machinery present but trigger-matchers arrive in their corresponding later phases. - RecoveryPayload emission machinery — content-addressed
@idper ADR-011 (ofbt:rp/<sha256-hex>); preserves original FOL for re-lifting. - The
prefixesparameter per API §3.10.4 — output emits CURIE form when supplied; full URIs when omitted. - Frozen
LOSS_SIGNATURE_SEVERITY_ORDERexported as a frozen array constant per API §6.4.1; mutation attempts throw.
- Cardinality n-tuple matcher (Step 4b per ADR-012's architect-ratified Option β) — cardinality projects as native OWL
RestrictionwithminCardinality/maxCardinality/cardinalityfields under Direct Mapping. Phase 1'sp1_restrictions_cardinalityfixture 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_warningRecovery Payload note per spec §6.2.1's literal framing. What v0.1 Realization actually emits: the OWLObjectPropertyChainaxiom 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 underregularityCheck(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) — wrapsowlToFol+folToOwlcomposition with the spec parity-criterion contract; emitsequivalent: truefor clean round-trips;equivalent: truemodulo Recovery Payloads for reversible-regime fixtures;equivalent: falsewith documented diff for true-loss fixtures.- Stub-evaluator harness + parity canaries (Step 8 per architect Q3 ruling 2026-05-06) —
tests/corpus/_stub-evaluator.jsimplements 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 realevaluate()per API §7.1.
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.
A.1. Input ontology
Three SubClassOf axioms with class-expression consequents: someValuesFrom, allValuesFrom, hasValue. From tests/corpus/p1_restrictions_object_value.fixture.js.
Loading fixture…
A.2. Run the round-trip
A.3. Lifted FOL (intermediate)
Press Run owlToFol → folToOwl to lift and project.
A.4. Projected OWL (round-trip output)
…
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.
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.
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).
arc/upstream-canonical/README.md:
- Layer A — OWL semantics in CLIF (what
SubClassOf,Transitive,InverseObjectPropertiesetc. 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.
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).
Loading fixture…
B.2. Run the round-trip
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.
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_of ↔ has_part implication pair and emits a single InverseObjectProperties axiom. The TBox SubClassOf and DisjointWith axioms project as Direct Mapping single-axiom rules.
…
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").
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.
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:
- Axiom 1:
∀x. Person(x) → ¬KnownProfession(x)— classical negation over an unbound predicate (thenaf_residuetrigger; severity rank 2 perLOSS_SIGNATURE_SEVERITY_ORDER) - Axiom 2:
unfamiliarBond(alice, bob)— binary atom over a predicate IRI outside any loaded ARC module (theunknown_relationtrigger; severity rank 5)
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.
Loading fixture…
C.2. Run the projection
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.
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:
- 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.
- Read the Loss Signature ledger. The ledger names exactly what was approximated, with
lossTypeandscopeNotesfields. 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. - 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 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+.
- Validator +
evaluate()per API §7.1 — Phase 3. The Phase 2 stub-evaluator harness (tests/corpus/_stub-evaluator.js) is a corpus-test-time bounded-Horn-resolution harness; the realevaluate()ships richer semantics (closed-predicate support per spec §6.3, Skolem-witness derivation, non-Horn fallback per spec §8.5). checkConsistency()+ No-Collapse Guarantee per API §8.1 + spec §8.5 — Phase 3. Required for the consistency-check ring per the validation-pipeline three-ring discipline.- ARC-content-driven inference — Phases 4-7. BFO 2020 core ARC module (Phase 4); IAO information-bridge (Phase 5); CCO realizable-holding + mereotopology + measurement + aggregate + organizational + deontic (Phase 6 per ADR-009 six-CCO-module expansion); compatibility shim + bundle budget enforcement + coverage matrix CI (Phase 7 per ADR-008 Option A — OFI deontic deferred to v0.2).
- Regularity-check upgrade per spec §6.2.1 — Phase 4 entry packet. Phase 2's chain projection always emits
regularity_scope_warningper architect Q-Step6-1 ruling. Phase 4 activatesregularityCheck(A, importClosure)against loaded ARC modules; chains regularity-confirmed under import closure emit WITHOUT the warning (a non-breaking strengthening of the contract per ADR-011's behavioral-contract evolution discipline). - Lifter
ObjectPropertyChainsupport per ADR-007 §1 / spec §5.2 — Phase 3 OR Phase 4 entry packet. Step 6 ships projector-only chain detection per architect Q-Step6-3 ruling; lifter support deferred until corpus demand surfaces (cycle-guarded chain rule emission for SLD inference at Phase 3, OR ARC content with chain axioms at Phase 4). - Source-provenance threading in the
ProjectionManifest— placeholder fields remain (ontologyIRI,versionIRI,projectedFrom); future cycle wires source-IRI threading from the lifter side. Forward-tracked. - Six remaining LossType trigger-matchers — the Step 4a machinery supports all 8 LossTypes (per ADR-011), but only
naf_residue+unknown_relationhave trigger-matchers shipping today.arity_flatteningarrives at Phase 4 (BFO ternary parthood);closure_truncated+una_residuearrive at Phase 3 (evaluator-time concerns);coherence_violationarrives at Phase 3 No-Collapse adversarial corpus;bnode_introducedat Phase 3 evaluator-derived Skolem introduction;lexical_distinct_value_equalat Phase 4 datatype handling. - Phase 3 entry re-exercise of parity canaries against the real
evaluate()— per Phase 2 entry packet §3.4 (Q3 phase3Reactivation discipline) and Q-Frank-4 architect ruling 2026-05-07 (per-canary publication commitment). The class-expression canary above asserts structural shape; the v0.1 contract is structural round-trip parity (spec §8.1). Stronger semantic senses (model-theoretic, axiomatic, entailment-preserving — a full semantic round-trip via lift → project → re-lift → query-evaluation match) require Phase 3's realevaluate().
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_warningcontract); §6.3 (default OWA negation +closedPredicatesPhase-3-deferred); §7 (audit artifacts taxonomy); §7.3 (RecoveryPayload reversible-regime contract); §7.5 (content-addressed@iddiscipline 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_ORDERexported as frozen array); §7.1 (evaluate— Phase 3 deliverable; Phase 2 stub-evaluator harness fills the corpus-test gap); §3.10.4 (prefixesparameter). - 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 withclifGroundTruthcitations 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-256480193e9…5912. Provenance +license-verificationblock atowl-axiomatization.clif.SOURCE; verified canonical LICENSE commit294fa416…b0cd, LICENSE SHA-256f5b745ef…cc3f, master HEAD at verification857be9f1…f3a7.- Implementation
src/kernel/projector.ts—folToOwl+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@idgeneration 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 + frozenLOSS_SIGNATURE_SEVERITY_ORDER.src/kernel/canonicalize.ts—stableStringifyimplementation supporting ADR-011@idhash-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 theInverseObjectPropertiestwo-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@idcontent-addressing scheme — SHA-256 ofstableStringifyof 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.