OFBT Phase 1 demo — two correctness arguments

The case

OFBT's correctness is measured two ways. The Phase 1 demo argues both.

Internal canary discipline. The test suite asserts wrong shapes are absent, not just that right shapes are present. This catches an entire class of silent-failure bug where degraded output passes casual tests.
External CLIF ground truth. Lifted FOL is parity-checked against canonical published FOL specifications. OFBT's lifter doesn't define what OWL constructs mean — the W3C does, in the canonical CLIF axiomatization. The Phase 1 lifter is verified against that source.

Why both matter. A correctness check that only verifies positive shape (assertion 1) misses regressions where the right shape and a wrong shape both appear. A correctness check that only verifies against external sources (assertion 2) misses regressions where the lifter introduces a subtle divergence consistent with one upstream's choices but inconsistent with another's. Both disciplines together close failure modes neither catches alone.

Case A — PROV-O domain/range conditional translation

An rdfs:domain declaration says "this property's subject must be of this class." A common implementation mistake is to translate that as "every member of this class participates in this property with some target" — synthesizing an existential successor that the source ontology never asserted. OFBT translates it correctly: as a conditional implication. The test suite asserts both the right shape is present and the wrong shape is absent.

Why this matters for stakeholders. The wrong translation passes casual tests — a query that simply asks "is X an Entity?" returns the right answer either way. The wrong translation only surfaces later, when downstream reasoning relies on the false existential entailment and produces wrong inferences for individuals that have no participating partners. OFBT catches the wrong shape with a dedicated canary fixture, eliminating an entire class of silent-failure bug.

A.1. Input ontology

A PROV-O fragment: wasInfluencedBy with both domain and range declared as prov:Entity, plus one property assertion. From tests/corpus/p1_prov_domain_range.fixture.js.

OWL ontology (structured JS input per API §3.1)

Loading fixture…

A.2. Run the lifter

Loading bundle…

Lifted FOL output (JSON-LD-shaped term tree per API §4)

Press Run owlToFol on PROV-O to lift the input.

A.3. Right shape present

The lifted FOL must contain three axioms in this exact shape: a domain universal, a range universal, and the asserted property fact. The conditional translation reads ∀x,y. P(x,y) → D(x) — "if P relates x and y, then x is in D" — the correct semantics of rdfs:domain.

A.4. Wrong shape absent

The lifted FOL must not contain any of these forbidden patterns. The canary fixture tests/corpus/canary_domain_range_existential.fixture.js ships the forbidden-pattern contract; OFBT's test suite asserts their absence on every run via the assertForbiddenPatterns helper.

Case B — BFO/CLIF Layer A parity

OFBT's lifter doesn't define what OWL constructs mean — the W3C does, in owl-axiomatization.clif (Fabian Neuhaus, 2009; vendored at arc/upstream-canonical/owl-axiomatization.clif). The Phase 1 lifter is parity-checked against that canonical CLIF for every OWL construct it processes. This case lifts a BFO 2020 OWL fragment and shows the parity directly.

Layer A vs Layer B — the end-goal framing. CLIF parity citations split into two layers per arc/upstream-canonical/README.md:

Layer A — OWL semantics in CLIF (what SubClassOf, Transitive, InverseObjectProperties etc. mean). Phase 1's lifter implements this.
Layer B — specific ontology content in CLIF (what BFO's Continuant, Occurrent, ternary parthood etc. mean). Phase 4+ ARC content covers this.

Phase 1 cites Layer A only. Each subsequent phase's demo extends CLIF coverage as ARC content lands. Cumulative coverage across phases is the discipline.

B.1. Input ontology

BFO 2020 standard-OWL subset: 5 SubClassOf + 1 DisjointWith + 1 Transitive + 1 InverseOf = 8 axioms. Uses ONLY constructs whose canonical Layer A semantics are defined in owl-axiomatization.clif; no ARC content required. From tests/corpus/p1_bfo_clif_classical.fixture.js.

BFO 2020 OWL subset (structured JS input)

Loading fixture…

B.2. Run the lifter

Loading bundle…

Lifted FOL output (9 axioms — the InverseOf decomposes per ADR-007 §4)

Press Run owlToFol on BFO subset to lift the input.

B.3. Layer A 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 — that's the right shape for "lifter correctness against canonical OWL semantics." Each badge reflects the verification state recorded in the fixture's clifGroundTruth array: ✓ Verified means an SME-persona content-check confirmed the cited line range against the vendored canonical source; [VERIFY] means the citation is awaiting that verification pass.

How to verify these badges reflect reality. The badges are not hardcoded to the demo HTML — they're rendered at runtime from the fixture file's clifGroundTruth[i].verificationStatus field. The fixture file lives in the repository at tests/corpus/p1_bfo_clif_classical.fixture.js. The flip from [VERIFY] to Verified happened at Step 9.2 close (commit 209a531, CI run 25330758341); the commit body documents the SME-persona content-check against arc/upstream-canonical/owl-axiomatization.clif at the cited line ranges. The vendored CLIF file's SHA-256 is pinned in arc/upstream-canonical/owl-axiomatization.clif.SOURCE for tamper-evidence. See arc/AUTHORING_DISCIPLINE.md Section "SME-Persona Verification of Vendored Canonical Sources" for the protocol; project/GOVERNANCE.md for the broader review discipline.

Per the architect-ratified meta-typing-predicate elision: canonical CLIF includes (Class X) and (OWLObjectProperty R) typing predicates. OFBT's lifted FOL omits these per the encoding choice "every IRI used in a class position is implicitly a Class; every IRI used in an object-property position is implicitly an OWLObjectProperty." The lifted FOL is the canonical-form BODY with meta-typing antecedents elided. Sound w.r.t. OWL semantics for v0.1; banked for ADR-007 §10 at Phase 1 exit doc pass.

What Phase 1 does NOT yet do

Phase 1 ships only the lifter. The Phase 1 demo verifies structural correctness; entailment, structural round-trip parity (Phase 2), and consistency checking (Phase 3) land in later phases.

Case A entailment-query verification — "does prov:Entity(project_alpha) evaluate to true?" requires the validator (Phase 3) plus PROV-O ARC content (Phase 4). The same fixture re-activates with entailment expectations at Phase 4 via the documented cross-phase activation pattern.
Case B Layer B citations against bfo-2020.clif (BFO's specific class-hierarchy and disjointness CLIF declarations) require Phase 4 ARC content + Layer B vendoring. The Phase 4 demo extends the parity panel with Layer B rows.
Structural round-trip parity (lift → project → re-lift → compare) requires the projector (Phase 2). That demo lands at Phase 2 exit.
Consistency check (No-Collapse Guarantee per spec §8.5) requires the validator (Phase 3). That demo lands at Phase 3 exit.

Provenance

Spec sections: Behavioral spec §5.2 (axiom injection patterns), §5.3 (TBox lifting), §5.8 (lifting rule for domain/range axioms); API spec §3.7.1 (high-priority correctness contract); API spec §3.7.1.1 (worked example tree); API spec §3.7.1.2 (forbidden translations); ADR-007 §1 architectural commitment (lifter emits classical FOL).
Case A right-shape fixture: tests/corpus/p1_prov_domain_range.fixture.js — the input ontology and expected lifted FOL.
Case A wrong-shape canary: tests/corpus/canary_domain_range_existential.fixture.js — the forbidden patterns asserted absent via assertForbiddenPatterns.
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 — the W3C OWL CLIF axiomatization (Fabian Neuhaus, 2009; BFO repository, BSD-3-Clause); 1660 lines, SHA-256 480193e9…78035912. Provenance sidecar at owl-axiomatization.clif.SOURCE.
Implementation: src/kernel/lifter.ts — liftRBoxAxiom (Step 3 for domain/range); liftClassExpression (Step 2 for TBox subClassOf/disjointness); liftRBoxAxiom ObjectPropertyCharacteristic + InverseObjectProperties cases (Step 5).
Test runner: tests/lifter-phase1.test.ts — uses assertForbiddenPatterns for Case A canary; deepStrictEqual for both fixtures' expected FOL.
Vendoring discipline: arc/upstream-canonical/README.md — Layer A vs Layer B framing; vendoring policy; refresh cadence; per-phase cumulative CLIF coverage rationale.
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), §7 (cardinality-witness convention — not exercised here), §8 (RDFC-1.0 b-node Skolem prefix — not exercised here), §9 (reserved-predicate full-URI canonical form), §10 (banked: meta-vocabulary encoding choice; Phase 1 exit doc pass).