The Boundary of Formalizability
How SatIR augments its formal representation for reasoning about clinical trials — compiling ontology-derived subsumption relations into constraints, and extending coverage beyond curated ontologies with embedding-based discovery.
The core mechanism: SatIR compiles subsumption relations directly into the SMT constraints themselves. On the patient side, concept-level, relation-level, qualifier-level, and causal subsumptions are encoded as additional constraints. On the trial side, qualifier-level subsumptions are injected into each trial's constraint set. Constraint solving is then performed over these augmented formulas rather than over raw extracted predicates alone.
The ontology provides four kinds of subsumption, each capturing a different axis of clinical reasoning:
A more specific patient concept can support a more general trial concept via SNOMED is-a relations. For positive facts, SatIR materializes ancestor facts while preserving time windows and qualifiers. For negation, a bounded set of negative descendants is materialized with caps and hop limits.
→ supports trial requiring Appendicitis (parent concept)
→ supports trial requiring Disorder of Appendix (grandparent)
Subsumption among clinical relations, implemented through curated rules. The grounded concept, qualifiers, and temporal context are preserved while the relation is generalized in a controlled way.
→ supports HasFindingOf(T2DM) (diagnosis is a finding)
HasSuspicionOf(Lymphoma)
→ supports HasFindingOf(Lymphoma) (suspicion is a finding)
→ supports HasDiagnosisOf(Lymphoma) (suspicion implies possible diagnosis)
Depends jointly on the relation and concept — cannot be reduced to concept or relation subsumption alone. Derived from SNOMED CT's formal concept definitions using typed attributes like Interprets, After, and Due to.
→ entails HasUndergone(Colonoscopy) (causal dependency)
HasFindingOf(Acute Kidney Injury)
→ entails Renal Function = Impaired (via Interprets + Has interpretation)
Temporal qualifiers are normalized to intervals. Any qualified predicate entails the corresponding unqualified one. For inclusion criteria, subsumption is defined by overlap; for exclusion, the exclusion window must strictly contain the patient fact window.
Chronic ⊑ ∅ (any qualifier subsumes no qualifier)
Patient side vs. trial side. On the patient side, SatIR compiles ⊑K, ⊑R, ⊑Q, and ⊑causal as additional constraints. On the trial side, ⊑Q is injected into each trial's constraint set. Constraint solving is then performed over these augmented formulas rather than over raw extracted predicates alone.