Formalization: Axioms, Restrictions, and the Profile Limit

📍 Where we are: Part IV · Formalization — turning the conceptual classes and relations into formal OWL 2 axioms a reasoner acts on. Methodology: SAMOD, whose test-first loop says each axiom earns its place only by serving a competency question we can run.

A taxonomy is a list of nouns under one another. An ontology is a list of nouns plus the rules that let a machine reason over them — and this chapter is where the rules get written for the part of the model everything else hangs from: the cell-bank genealogy and the purification lineage of the mAb campaign. We take the classes and relations already conceptualized — WCB-CHO-001 and its master and research tiers, the derivedFrom chain that runs from a frozen vial all the way down to a vialed drug product — and add the OWL 2 axioms that give them teeth: subclass inheritance, domain and range as typing rules, transitivity for genealogy, functional properties that catch a double-entered provenance record, existential and cardinality restrictions for cell-bank completeness, and disjointness for the category errors that wreck batch traceability. We also meet the one rule we want but cannot have — the profile limit on transitivity — and name it honestly, because pretending it away at the root of a manufacturing graph is how a model quietly becomes untrustworthy.

The simple version

A bakery's sourdough starter is the ancestor of every loaf, and a kitchen inspector enforces standing rules without being asked each time: "every working jar descends from exactly one master jar" (functional property), "a jar is never also the oven that bakes the loaf" (disjointness), "if this loaf came from that jar and that jar from the master, then this loaf came from the master" (transitivity), "no working jar leaves the shelf without at least one quality check on file" (cardinality). Classes and instances give you shapes and things. Axioms are the standing rules that let a machine check and extend the whole genealogy on its own — so a reasoner can trace any loaf to its starter without anyone writing down every intermediate link. One rule, though, the inspector cannot phrase in this language — that the genealogy never loops — so we hand that one to a second inspector (SHACL) and say so out loud.

Start from the questions

Axioms are not decoration; each is here to make a competency question answerable about a real cell bank, a real batch, a real lineage. Four CQs govern this chapter, and each carries a manufacturing question behind its structural surface. CQ-22 asks whether the long-range transitive derivedFrom edges are inferred and whether equipment is inferred a BFO material entity — which is the formal way of asking can the graph trace drug substance DS-001 back to the working cell bank without anyone hand-asserting the link? CQ-23 asks whether the disjointness guards catch planted conflations — can a naive multi-source load smuggle in "the batch is the run" or "the batch is the bioreactor," the two errors that silently break genealogy? CQ-17 asks whether the working cell bank is fully characterized so it conforms to the cell-bank gate — is this bank actually safe to release into a campaign: identity, sterility, viral safety, genetic stability all on file? And CQ-18 asks whether the bank sits within its validated passage limit — have the cells been grown so long that productivity or product quality may have drifted? Hold these four; every axiom block below points at one, and each is a question a quality unit would otherwise answer by spreadsheet archaeology.

Formalize: subclass and domain/range as rules

The cheapest axiom does real work. rdfs:subClassOf says one class is a kind of another, so any fact true of the parent is inherited — declare bp:WorkingCellBank rdfs:subClassOf bp:CellBank rdfs:subClassOf bp:Material and the working bank automatically is a material that can carry a derivedFrom edge and a release status, with the constraint stated once at the general class. Domain and range then pin what a property may connect, and they are rules, not documentation: assert an edge and the reasoner types its ends.

# bioproc.ttl — derivedFrom: a transitive object property with domain and range as typing rules.
bp:derivedFrom a owl:ObjectProperty , owl:TransitiveProperty ;
    rdfs:label "derived from" ;
    rdfs:domain bp:Material ; rdfs:range bp:Material ;
    skos:definition "Relates a material to the parent material it originated from; transitive, so lineage is inferable to any depth." .

Because bp:derivedFrom has range bp:Material, writing BATCH-2026-001 derivedFrom X infers that X is a material — so if an operator's ID or a vessel slips into a parent slot during a multi-source load, and that thing is already declared bp:Equipment or a Person, the disjointness below makes the graph contradictory and the bad edge is caught instead of silently corrupting the lineage. A loose edge becomes a typed one, and typing is the first line of defence on a genealogy that must hold for the regulatory life of the product.

Formalize: the transitive spine — and the profile limit

Transitivity is the single most valuable axiom in the book, because the entire promise of the digital thread — trace any lot to its cell bank, scope any recall to its descendants — rests on it. owl:TransitiveProperty on bp:derivedFrom tells any reasoner that if POLpool-001 derivedFrom VFpool-001 and VFpool-001 derivedFrom VIpool-001, then POLpool-001 derivedFrom VIpool-001 — and, hop after hop, that DS-001 derivedFrom WCB-CHO-001 and on up to the research bank RCB-CHO-001. Only the immediate parent edges are stated: the seed train lays the first edge off the bank, the bioreactor the next, capture and polishing and UF/DF the rest. The running example's lineage is eleven materials deep, so the eleven ancestors of DS-001 are reached without anyone asserting a single long-range link [1]. This is what lets a lineage question reach the frozen vial from the drug substance in a single hop of meaning — the cell bank is where manufacturing genealogy begins, and transitivity is what makes that beginning reachable from anywhere downstream.

The packing hierarchy gets a parallel treatment with bp:contains, and campaign-level occurrents with bp:hasTemporalPart — three transitive properties, each making a different reach inferable, and the deliberate separation of containment from lineage is itself a modeling commitment:

# bioproc.ttl — two more transitive properties; containment is deliberately NOT lineage.
bp:hasTemporalPart a owl:ObjectProperty , owl:TransitiveProperty ; rdfs:label "has temporal part" ;
    rdfs:domain bp:Process ; rdfs:range bp:Process ;
    skos:definition "Relates a campaign-level occurrent to the sub-processes it spans." .
bp:contains a owl:ObjectProperty , owl:TransitiveProperty ; rdfs:label "contains" ;
    rdfs:domain bp:Package ; rdfs:range bp:Material ;
    skos:definition "The packing containment hierarchy (carton contains vials, case contains cartons, pallet contains cases). DELIBERATELY NOT a sub-property of derivedFrom: containment is mutable and is not lineage." .

That last comment is doing real bioprocess work. A vial is contained in a carton, but the carton is not where the vial came from — packing is mutable and reversible, genealogy is permanent and directional. Folding the two together would let a repacking event masquerade as a derivation and corrupt the very recall scope transitivity exists to compute. Keeping bp:contains off the derivedFrom spine is how the model refuses to confuse "is currently boxed with" and "descended from."

Now the rule we want but cannot write. We would like bp:derivedFrom to be irreflexive (no material derives from itself) and asymmetric (if DS-001 derives from the cell bank, the cell bank does not derive from DS-001) — together those would make a lineage cycle a flagged contradiction, the formal statement of a domain fact: genealogy edges only ever point backward in time, toward earlier materials. But bp:derivedFrom is already transitive, and a transitive property is non-simple; OWL 2 DL forbids a non-simple property from also carrying owl:IrreflexiveProperty or owl:AsymmetricProperty, because doing so pushes the logic out of the decidable profile where reasoning is guaranteed to terminate [2]. The source file states this constraint inline rather than hiding it:

# bioproc.ttl — the profile constraint, stated where derivedFrom is defined.
#  NB: bp:derivedFrom is owl:TransitiveProperty, so OWL 2 DL FORBIDS also typing it asymmetric or
#  irreflexive (a non-simple property may not carry those) — lineage acyclicity is therefore a SHACL/
#  convention guarantee, not an OWL one. This is a real profile constraint, called out in the chapter.

So acyclicity of the genealogy is not an OWL guarantee here. That a derivedFrom chain runs backward in time is a domain fact about how manufacturing works — a batch cannot be its own ancestor — and we enforce it with SHACL and with the ETL convention that edges only ever point to earlier materials. Naming that limit is part of modeling rigorously, not a footnote to it — the specification listed decidable among the non-functional requirements precisely so this trade-off would be honored rather than faked, because a reasoner that does not terminate is worse than useless on a graph a release decision depends on.

Formalize: functional properties for de-duplication

A functional property holds at most one value per subject — and in the cell-line slice, "at most one" is a biological truth before it is a logical one. A line is created by exactly one transfection event; a working bank descends from exactly one selected clone; a line expresses its product in exactly one host species. Three of the cell-line relations carry owl:FunctionalProperty, and each does inferential work: assert two values and a reasoner concludes they are owl:sameAs the same individual, a built-in de-duplication that catches a double-entered provenance record before it splits one cell line's history into two contradictory lineages [1].

# bioproc.ttl — functional object properties: at most one value per subject.
bp:hasHostOrganism a owl:ObjectProperty , owl:FunctionalProperty ; rdfs:label "has host organism" ;
    rdfs:domain bp:Material ; rdfs:range bp:HostOrganism .   # functional: a line/bank has exactly one host
bp:hasClone a owl:ObjectProperty , owl:FunctionalProperty ; rdfs:label "has clone" ;
    rdfs:domain bp:CellBank ; rdfs:range bp:Clone .          # functional: a bank descends from one clone
bp:createdBy a owl:ObjectProperty , owl:FunctionalProperty ; rdfs:label "created by" ;
    rdfs:domain bp:CellLine ; rdfs:range bp:Transfection .   # functional: a line is created by one transfection

The createdBy functional property also models the transfection as an occurrent with real material inputs and outputs — TF-001 takes CONSTRUCT-mAb-A (the expression vector carrying the antibody gene) as input and yields CELLLINE-001 as output. The line is made, in one event; keeping that event a process rather than a string attribute is what later lets the graph answer "how was this line created?" rather than only "what is it?" — and the functional axiom guarantees the answer is single-valued, so the provenance of every descendant batch resolves to one transfection, not a fork.

Formalize: restrictions — existential and qualified cardinality

Subclass links make a taxonomy; class restrictions make necessary conditions a reasoner can enforce. Two anchor the cell-line slice and underwrite CQ-17. The existential restriction (owl:someValuesFrom) says every cell line is the output of some transfection — a line that was never transfected is malformed, which is the model's way of insisting that an engineered production line has a defined genetic origin. The qualified min-cardinality restriction says every working cell bank bears at least one characterization result of the right class — the formal twin of "is the bank characterized?", the question that decides whether a bank is fit to seed a GMP campaign at all.

# bioproc.ttl — class axioms (full DL; owlrl acts on a subset, a HermiT/ELK reasoner on all).
#  Necessary condition: every cell line is the output of some transfection (existential restriction).
bp:CellLine rdfs:subClassOf [ a owl:Restriction ;
    owl:onProperty bp:createdBy ; owl:someValuesFrom bp:Transfection ] .
#  A working cell bank must bear at least one characterization result (qualified min-cardinality).
bp:WorkingCellBank rdfs:subClassOf [ a owl:Restriction ;
    owl:onProperty bp:hasCharacterization ;
    owl:minQualifiedCardinality "1"^^xsd:nonNegativeInteger ; owl:onClass bp:CharacterizationResult ] .

The characterizations the restriction demands are not generic completeness fields — they are the four evidenced qualities a regulator expects of a cell substrate, and each prevents a distinct disaster: an identity / authentication result (the bank is the line you think it is), a sterility / mycoplasma result (no contaminating organism), an adventitious-agent / viral safety result (no virus that survives into product), and a genetic stability result (the line still expresses the right antibody after banking). A working bank with any one missing is a bank you cannot safely seed a batch from. These are necessary conditions under the open world: a working bank with no characterization recorded is "incomplete," not contradictory — the reasoner will not invent the gap. The closed-world gate that turns a missing viral-safety result into an outright failure — and answers CQ-17 in the runnable pipeline — is the SHACL release/cell-bank shapes.

Axioms at work: asserted immediate derivedFrom edges (solid) let a reasoner infer the long-range link (dashed) by transitivity, domain and range type the ends, and a disjointness bar between Batch and CellCultureProcess turns "a batch is not a run" into an enforced rule. Original diagram by the authors, created with AI assistance.

Formalize: disjointness — the category guards that protect traceability

Disjointness catches the exact conflations that wreck batch traceability — and they are not hypothetical. A naive multi-source load, pulling from a process historian and an inventory system at once, routinely fuses the material (the batch) with the equipment (the bioreactor that held it) or with the process (the fermentation run that produced it), because all three share a name on the plant floor. At the top of the model the BFO categories are declared pairwise disjoint, and two specific guards sit downstream: a batch is never the run that produced it (the continuant/occurrent guard), and a material is never the vessel that held it (the material/equipment guard) [3].

# bioproc.ttl — disjointness: the continuant/occurrent and material/equipment guards, plus the tier guard.
bp:Material owl:disjointWith bp:Process , bp:Equipment , bp:Quality , bp:RealizableEntity , bp:InformationArtifact .
bp:Process  owl:disjointWith bp:Quality , bp:RealizableEntity , bp:InformationArtifact , bp:Equipment .
bp:Batch owl:disjointWith bp:CellCultureProcess .
#  A bank belongs to exactly one tier: the three tiers are pairwise disjoint.
[] a owl:AllDisjointClasses ; owl:members ( bp:ResearchCellBank bp:MasterCellBank bp:WorkingCellBank ) .

owl:disjointWith handles the binary cases (Material vs Equipment, Batch vs CellCultureProcess); owl:AllDisjointClasses handles the three cell-bank tiers in one compact axiom so a bank cannot be both research and working. The tier guard is not bureaucratic tidiness — the RCB / MCB / WCB hierarchy exists because each tier answers a different release question, and a bank that is silently "both" would let a research-grade, under-characterized aliquot pass for a release-ready working bank. Assert two disjoint types on one IRI and a full DL reasoner reports the graph inconsistent — which is exactly what CQ-23 checks against planted conflations, because at the root of a genealogy the difference between a batch, the run that made it, and the vessel that held it is the difference between a traceable thread and a confident lie.

What OWL-RL does — and does not — enforce

There is a divide here that decides whether a model is honest about a release decision. The runnable pipeline reasons with OWL-RL, a lightweight rule-based profile, not a full DL reasoner. OWL-RL does compute the transitive closure and the domain/range typing — so CQ-22's long-range lineage (DS-001 reaching WCB-CHO-001 and RCB-CHO-001) and "equipment is a BFO material entity" fall straight out of it. But OWL-RL does not act on owl:disjointWith, owl:AllDisjointClasses, or the qualified-cardinality restriction. A bank wrongly typed as both research and working, or a batch typed as both a bp:Batch and a bp:Bioreactor, slips past owlrl silently — and a silent slip in a category guard is precisely the failure that propagates into a corrupted recall scope. A full DL reasoner (HermiT/ELK in Protégé) catches those directly; in the runnable validator, SHACL guards carry the closed-world catch:

# shapes.ttl — the closed-world guards that catch what OWL-RL does not (the runnable CQ-23 catch).
bp:BatchNotProcessShape a sh:NodeShape ;
    sh:targetClass bp:Batch ;
    sh:not [ sh:class bp:CellCultureProcess ] ;
    sh:message "A Batch (material/continuant) must not also be a CellCultureProcess (occurrent)." .

bp:MaterialNotEquipmentShape a sh:NodeShape ;
    sh:targetClass bp:Material ;
    sh:not [ sh:class bp:Equipment ] ;
    sh:message "A Material (batch/lot/pool) must not also be Equipment (a persisting vessel)." .

The division of labour is the point: the OWL axiom states intent for a DL reasoner; the SHACL shape is what actually catches the conflation in the network-free validator [4]. Belt and braces — and on the floor, the braces are what hold, because the runnable gate is what a quality unit actually runs against the day's data.

The QbD link: a process parameter that affects a quality attribute

Not every axiom guards the genealogy; one of the most valuable ones records development knowledge. The link a process-development team works hardest to establish — this critical process parameter affects that critical quality attribute — is, structurally, one more authored object property. bp:affectsQuality runs from a bp:ProcessParameter to a bp:QualityAttribute, and once declared, a fact that would otherwise live in a prose development report becomes a queryable edge:

# bioproc.ttl — the Quality-by-Design link as an authored relation.
bp:affectsQuality a owl:ObjectProperty ;
    rdfs:label "affects quality" ;
    rdfs:domain bp:ProcessParameter ; rdfs:range bp:QualityAttribute ;
    skos:definition "The Quality-by-Design link: a critical process parameter affects a critical quality attribute." .

Assert bp:FeedRate bp:affectsQuality bp:MonomerPct-CQA and an investigator chasing a low-monomer result can later ask the graph "which parameters affect monomer purity?" and get an answer rather than a reading assignment. The domain/range typing keeps the edge honest — only a parameter can affect, only an attribute can be affected — so the most prized knowledge in process development inherits the same machine-checkable discipline as the lineage spine.

Formalize: where release attributes are scoped, and why

One subtle axiom choice repays a close look because it is invisible until it bites: the scope of the release attributes. A batch carries a bp:derivedFrom edge to its parent, but the release attributes — bp:releaseStatus, bp:monomerPct, bp:hmwPct, bp:cexMainPct — are declared with their domain set to bp:Material, the superclass, not to bp:Batch. That width is deliberate. The lots that actually carry a release status and a SEC monomer result are not the bioreactor batches but the drug-substance and drug-product lots — DS-001 and the vialed DP-001 — which are also bp:Material. The drug substance DS-001 carries releaseStatus "PASS", monomerPct 98.611, hmwPct 1.287, cexMainPct 70.686; scoping these properties narrowly to bp:Batch would have wrongly typed every released lot as a batch, collapsing the very continuant distinction the disjointness guards protect. By scoping to bp:Material, asserting a release result types the subject as a material and lets the released lots inherit the attributes without anyone forcing them to be batches. The schema is wide on purpose, and the width is an axiom decision with downstream consequences for what the release gate can target.

Evaluation: the axioms earn the questions

validate.py parses bioproc.ttl + align.ttl + instances.ttl, applies the OWL-RL closure, runs the competency-question catalog, and SHACL-validates — and the closure is where the formalization shows its hand:

# Real output from validate.py (owlrl OWL-RL closure + SHACL over the running example).
[1] parsed 2120 triples (bioproc + align + instances)
[2] reasoned: 2120 -> 7137 triples after OWL-RL closure
      CQ-22  structural      PASS   transitive lineage + equipment-is-material inferred
      CQ-23  structural      PASS   Batch-as-process and Batch-as-bioreactor both caught

The jump from 2120 to 7137 triples is the closure doing structural work over the real campaign: the transitive derivedFrom manufactures the long-range lineage no one asserted — DS-001 reaches both the working bank WCB-CHO-001 and the research bank RCB-CHO-001 across the full eleven-material chain — and equipment is inferred a BFO material entity. That is CQ-22, passing, and it is the formal proof that the digital thread can trace any lot to its frozen vial. Both disjointness guards refuse their planted conflations (conforms False is SHACL's verdict, since OWL-RL does not act on owl:disjointWith): the "batch is the run" and "batch is the bioreactor" errors are both caught. That is CQ-23, passing. CQ-17 and CQ-18 are answered by the cell-bank gate and the passage-limit ASK: WCB-CHO-001 carries its four characterizations — identity, sterility, viral safety, genetic stability — and a passage count of 8, within the validated limit of 40. All four hold, and the one axiom we could not write is documented rather than faked.

The unsolved part: a consistent model can still misidentify a living root

Every axiom is a commitment a reasoner must honor, and that cuts both ways. A richly constrained ontology can become computationally expensive or step outside the decidable OWL 2 profile, where reasoning no longer terminates reliably [5] — the very risk the transitivity-profile limit above made concrete. The art is to axiomatize exactly enough to catch the errors that matter — for this graph, the genealogy-corrupting category errors and the cell-bank completeness gaps — and no more.

But the deeper limit is that a reasoner proves only that a model is consistent, never that it is correct. A derivedFrom whose direction is reversed, a disjointness forgotten so the "batch is the run" error slips through, a cardinality that should be "exactly one" left as "at least one" — all of these are perfectly consistent and perfectly wrong. And at the root of this particular graph the gap between consistent and correct turns biological. A cell line is alive: a population of cells that mutate and drift over generations, so the bank at passage 60 is not genetically identical to the bank at passage 5, and no owl:sameAs or restriction can answer whether the two are "the same entity." The axioms assume WCB-CHO-001 is WCB-CHO-001, a stable IRI over a moving population — a useful fiction bounded by characterization, not the crisp sameness the identifier implies. Worse, and historically real, is misidentification: cell lines have been confused and cross-contaminated across the life sciences for decades. For a manufacturing root node that is the worst possible error, because it is asserted with full confidence, it propagates to every descendant batch through derivedFrom, and no amount of downstream data integrity catches it — every downstream fact is correctly derived from a wrongly identified root. The logic checks coherence, not truth, which is why formalization stays a reviewed, governed human practice and not a generated artifact — and why the root of the graph rests ultimately on wet-lab authentication the ontology can record but never certify.

Why it matters

Axioms are the difference between a vocabulary that merely labels the campaign and one that checks and extends it. Transitivity makes the genealogy walkable from drug product to frozen vial; functional properties merge a duplicated provenance record so one cell line has one history; restrictions pin cell-bank completeness so an under-characterized bank cannot seed a batch; disjointness makes the genealogy-corrupting category errors loud. Get them right and the model defends its own integrity as it grows — every later lineage and impact query the digital thread runs is trustworthy by construction, including the one that scopes a recall when DP-004 comes back out of spec on HMW aggregate and the impact walk climbs to the shared cell bank. Get them wrong, or over-constrain, and you have either an expensive spreadsheet with IRIs or a model no reasoner can finish. The leverage of the whole approach lives in this chapter, because it lives at the root.

In the real world

You do not hand-write these axioms in a text editor; the de facto tool is Protégé, the free Stanford editor, where domain experts define classes and properties visually and run a DL reasoner to view inferences and catch contradictions before anything ships [4]. The transitivity-profile constraint is not academic trivia either — it is a documented OWL 2 DL rule that real ontologies hit the moment they make a part-of or derived-from relation both transitive and acyclic, and the standard, honest resolution is exactly the one here: keep the property transitive and enforce acyclicity outside the logic [2]. The cell-bank characterization restriction, likewise, mirrors a regulatory expectation — the RCB / MCB / WCB hierarchy and its characterization are an expectation of the guidance on cell substrates, not optional good practice — which is why every real CHO antibody program, working with a host whose genome is sequenced and public, maintains exactly this lineage and exactly these four classes of result [6].

Key terms

• Subclass / domain / range — the typing rules: a subclass inherits everything from its parent; domain and range infer the types of a property's ends, turning a loose derivedFrom edge into a typed one that the disjointness guards can police.
• Transitive property — an OWL relation (derivedFrom, contains, hasTemporalPart) where A→B and B→C imply A→C, making the eleven-deep genealogy and the packing containment inferable to any depth from a few stated edges.
• Functional property — createdBy, hasHostOrganism, hasClone: at most one value per subject (one transfection, one host species, one clone), so a reasoner merges a duplicate provenance record (owl:sameAs) instead of forking a cell line's history.
• Existential restriction — CellLine ⊑ ∃createdBy.Transfection: every engineered line must be the output of some transfection event, so a production line always has a defined genetic origin.
• Qualified cardinality restriction — WorkingCellBank ⊑ ≥1 hasCharacterization.CharacterizationResult: the open-world necessary condition that a bank carry characterization evidence, whose closed-world twin is the SHACL cell-bank gate.
• Disjointness — owl:disjointWith and owl:AllDisjointClasses: the material/equipment, continuant/occurrent, and cell-bank-tier guards that stop a multi-source load from fusing a batch with its run, its vessel, or a wrong tier.
• Transitivity-profile constraint — because derivedFrom is transitive (non-simple), OWL 2 DL forbids also typing it irreflexive/asymmetric; that genealogy points backward in time is a domain fact enforced by SHACL/convention, not an OWL one.
• Over-axiomatization — adding more constraints than the questions need, risking expensive or non-terminating reasoning; the discipline is to axiomatize exactly enough to catch the genealogy and completeness errors that matter, and stop.

Where this leads

The classes now have teeth: typed, transitive, functional, restricted, and guarded — the cell-bank root is constrained, the genealogy is walkable, and the one axiom OWL cannot hold is named. But every subject, predicate, and value written so far assumes a name means the same thing everywhere, and that a number like 98.611 never travels without its unit. The next chapter, Identifiers and Units: IRIs, QUDT, and the Typed Value, makes those guarantees concrete — the globally unique identifier that stops two systems' BATCH-2026-001 from colliding, and the unit-and-datatype discipline that stops 98.611 from ever meaning a fraction in one system and a percent in another, the exact ambiguity a release gate cannot afford.