Insurance

The scene

A claim arrives. First-pass adjudication is exactly the decision regulators and courts have been looking at: when it is automated opaquely, the record is not good. One Medicare Advantage tool faced litigation over an alleged "known 90% error rate"; ProPublica found another payer batch-denied 300,000 claims in two months at roughly 1.2 seconds per claim; a 2026 Senate and OIG inquiry followed (research/scenarios/ruled-out.md). CMS-0057-F now requires FHIR prior-authorization APIs, and the Da Vinci CRD/DTR/PAS guides define the wire.

None of that argues against automation. It argues against automation that cannot say why. The Horismos version of this decision produces, for every determination, a proof tree that names the exact clause it rests on — which is what makes a denial appealable and an approval auditable.

The overlay

# Gallery overlay: first-pass adjudication of a health-insurance claim.
# Illustrative business rules — every denial carries a proof tree that names
# the exact clause, which is what makes it appealable.

@prefix :      <https://example.org/claims#> .
@prefix horis: <https://w3id.org/horismos#> .
@prefix rdf:   <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix rdfs:  <http://www.w3.org/2000/01/rdf-schema#> .
@prefix xsd:   <http://www.w3.org/2001/XMLSchema#> .

## Domain (doc 02)

:Claim a rdfs:Class ;
    rdfs:label "Claim" .

:policyActiveOnServiceDate a rdf:Property ;
    rdfs:domain :Claim ; rdfs:range xsd:boolean ;
    horis:cardinality "1" .

:serviceCovered a rdf:Property ;
    rdfs:domain :Claim ; rdfs:range xsd:boolean ;
    horis:cardinality "1" .

:priorAuthRequired a rdf:Property ;
    rdfs:domain :Claim ; rdfs:range xsd:boolean ;
    horis:cardinality "0..1" .

:priorAuthOnFile a rdf:Property ;
    rdfs:domain :Claim ; rdfs:range xsd:boolean ;
    horis:cardinality "0..1" .

:billedAmount a rdf:Property ;
    rdfs:domain :Claim ; rdfs:range xsd:decimal ;
    horis:unit "USD" ;
    horis:min 0 ;
    horis:cardinality "0..1" .

:Network a rdfs:Class ;
    horis:oneOf ( :InNetwork :OutOfNetwork ) .

:network a rdf:Property ;
    rdfs:domain :Claim ; rdfs:range :Network ;
    horis:cardinality "0..1" .

:Adjudication a rdfs:Class ;
    horis:oneOf ( :Approved :Pended :Denied ) .

:adjudication a rdf:Property ;
    rdfs:domain :Claim ; rdfs:range :Adjudication ;
    horis:cardinality "0..1" ;
    horis:assignedBy horis:RulesOnly .   # no model, adjuster script, or API caller sets this

## Rules (doc 04)

:denyInactivePolicy a horis:Rule ;
    horis:priority 100 ;
    horis:when [
        horis:subject :Claim ; horis:property :policyActiveOnServiceDate ; horis:is false
    ] ;
    horis:then [ horis:property :adjudication ; horis:value :Denied ] ;
    horis:explain "Policy was not active on the date of service" .

:denyNonCoveredService a horis:Rule ;
    horis:priority 90 ;
    horis:when [
        horis:subject :Claim ; horis:property :serviceCovered ; horis:is false
    ] ;
    horis:then [ horis:property :adjudication ; horis:value :Denied ] ;
    horis:explain "Service is excluded from the plan's covered benefits" .

:pendMissingPriorAuth a horis:Rule ;
    horis:priority 80 ;
    horis:when [
        horis:all (
            [ horis:subject :Claim ; horis:property :policyActiveOnServiceDate ; horis:is true ]
            [ horis:subject :Claim ; horis:property :serviceCovered ; horis:is true ]
            [ horis:subject :Claim ; horis:property :priorAuthRequired ; horis:is true ]
            [ horis:subject :Claim ; horis:property :priorAuthOnFile ; horis:is false ]
        )
    ] ;
    horis:then [ horis:property :adjudication ; horis:value :Pended ] ;
    horis:explain "Prior authorization is required and none is on file — pend for documentation, do not deny" .

:pendHighDollar a horis:Rule ;
    horis:priority 70 ;
    horis:when [ horis:all (
            [ horis:subject :Claim ; horis:property :policyActiveOnServiceDate ; horis:is true ]
            [ horis:subject :Claim ; horis:property :serviceCovered ; horis:is true ]
            [ horis:subject :Claim ; horis:property :billedAmount ; horis:exceeds 10000 ]
    ) ] ;
    horis:then [ horis:property :adjudication ; horis:value :Pended ] ;
    horis:explain "Billed amount exceeds the auto-adjudication ceiling — human review" .

:approveClean a horis:Rule ;
    horis:priority 10 ;
    horis:when [
        horis:all (
            [ horis:subject :Claim ; horis:property :policyActiveOnServiceDate ; horis:is true ]
            [ horis:subject :Claim ; horis:property :serviceCovered ; horis:is true ]
            [ horis:subject :Claim ; horis:property :billedAmount ; horis:atMost 10000 ]
            [ horis:any (
                [ horis:subject :Claim ; horis:property :priorAuthRequired ; horis:is false ]
                [ horis:subject :Claim ; horis:property :priorAuthOnFile ; horis:is true ]
            ) ]
        )
    ] ;
    horis:then [ horis:property :adjudication ; horis:value :Approved ] ;
    horis:explain "Active policy, covered service, within ceiling, authorization satisfied" .

# PRP-005 completeness-cover:start
# Two regions had no adjudication until PRP-005's completeness check named them.
# Both are missing data rather than a settled outcome, and this rule set already
# says what to do with missing data — :pendMissingPriorAuth pends for documentation
# rather than denying. Auto-denying a claim because a field was never populated is
# exactly the failure this overlay exists to argue against.
#
# A claim with no amount *and* a missing required authorization stays with
# :pendMissingPriorAuth, which already pends it; the guard below keeps this rule off
# that region so the proof names the authorization, not the amount.
:amountNotRecordedPends a horis:Rule ;
    horis:priority 60 ;
    horis:when [ horis:all (
        [ horis:subject :Claim ; horis:property :policyActiveOnServiceDate ; horis:is true ]
        [ horis:subject :Claim ; horis:property :serviceCovered ; horis:is true ]
        [ horis:subject :Claim ; horis:property :billedAmount ; horis:isEmpty true ]
        [ horis:any (
            [ horis:subject :Claim ; horis:property :priorAuthRequired ; horis:isNot true ]
            [ horis:subject :Claim ; horis:property :priorAuthOnFile ; horis:isNot false ]
        ) ]
    ) ] ;
    horis:then [ horis:property :adjudication ; horis:value :Pended ] ;
    horis:explain "No billed amount on the claim — it cannot be tested against the auto-adjudication ceiling, so it pends" .

# :approveClean needs `priorAuthRequired is false` or `priorAuthOnFile is true`, and
# :pendMissingPriorAuth needs both recorded; a condition over an unassigned property
# is false (doc 02), so a claim that never recorded the requirement matched neither.
:priorAuthStatusUnknownPends a horis:Rule ;
    horis:priority 60 ;
    horis:when [ horis:all (
        [ horis:subject :Claim ; horis:property :policyActiveOnServiceDate ; horis:is true ]
        [ horis:subject :Claim ; horis:property :serviceCovered ; horis:is true ]
        [ horis:subject :Claim ; horis:property :billedAmount ; horis:atMost 10000 ]
        [ horis:subject :Claim ; horis:property :priorAuthRequired ; horis:isNot false ]
        [ horis:subject :Claim ; horis:property :priorAuthOnFile ; horis:isNot true ]
        [ horis:any (
            [ horis:subject :Claim ; horis:property :priorAuthRequired ; horis:isEmpty true ]
            [ horis:subject :Claim ; horis:property :priorAuthOnFile ; horis:isEmpty true ]
        ) ]
    ) ] ;
    horis:then [ horis:property :adjudication ; horis:value :Pended ] ;
    horis:explain "Whether prior authorization is required, or whether it is on file, was never recorded — pend for documentation, do not deny" .
# PRP-005 completeness-cover:end

Two design choices are the whole point. A missing prior authorization pends the claim for documentation rather than denying it (pendMissingPriorAuth outranks approveClean and never concludes :Denied), and an amount over the auto-adjudication ceiling goes to a human. The rules encode the policy you would defend in front of a regulator, and nothing else can set :adjudication.

The decision, with proof

from horismos import HorismosValidationError, Ontology, World

onto = Ontology.load("examples/gallery/claims-adjudication.ttl")
world = World(onto)

def adjudicate(subject: str, **facts: object) -> None:
    ref = world.assert_(":Claim", subject=subject, **facts)
    proof = world.explain(ref, ":adjudication")
    print(proof.render() if proof else f"{subject}: no determination")

adjudicate(":clm-1001", policy_active_on_service_date=True, service_covered=True,
           prior_auth_required=False, billed_amount=1840.00, network=":InNetwork")
adjudicate(":clm-1002", policy_active_on_service_date=True, service_covered=True,
           prior_auth_required=True, prior_auth_on_file=False, billed_amount=3200)
adjudicate(":clm-1003", policy_active_on_service_date=False, service_covered=True,
           prior_auth_required=False, billed_amount=120)

:adjudication = :Approved   via approveClean — "Active policy, covered service, within ceiling, authorization satisfied"
  ├─ policyActiveOnServiceDate true is true   (asserted by the api)
  ├─ serviceCovered true is true   (asserted by the api)
  ├─ billedAmount 1840 atMost 10000   (asserted by the api)
  └─ any of:
     ├─ priorAuthRequired false is false   (asserted by the api)
     └─ priorAuthOnFile is true   (not held)

:adjudication = :Pended   via pendMissingPriorAuth — "Prior authorization is required and none is on file — pend for documentation, do not deny"
  ├─ policyActiveOnServiceDate true is true   (asserted by the api)
  ├─ serviceCovered true is true   (asserted by the api)
  ├─ priorAuthRequired true is true   (asserted by the api)
  └─ priorAuthOnFile false is false   (asserted by the api)

:adjudication = :Denied   via denyInactivePolicy — "Policy was not active on the date of service"
  └─ policyActiveOnServiceDate false is false   (asserted by the api)

The denial is one line long and names the one fact it rests on. An appeal disputes that fact, not a black box.

The authorization arrives for the pended claim. The determination changes in the transaction that recorded the document — no batch job, no stale "pended" status left behind — and the proof now shows the other branch of the disjunction held:

adjudicate(":clm-1002", prior_auth_on_file=True)

:adjudication = :Approved   via approveClean — "Active policy, covered service, within ceiling, authorization satisfied"
  ├─ policyActiveOnServiceDate true is true   (asserted by the api)
  ├─ serviceCovered true is true   (asserted by the api)
  ├─ billedAmount 3200 atMost 10000   (asserted by the api)
  └─ any of:
     ├─ priorAuthRequired is false   (not held)
     └─ priorAuthOnFile true is true   (asserted by the api)

High-dollar claims go to a person, and no adjuster script, model, or API caller can write the determination directly:

adjudicate(":clm-1004", policy_active_on_service_date=True, service_covered=True,
           prior_auth_required=True, prior_auth_on_file=True, billed_amount=48000)
try:
    world.assert_(":Claim", subject=":clm-1005", policy_active_on_service_date=True,
                  service_covered=True, adjudication=":Approved")
except HorismosValidationError as e:
    print(f"[{e.constraint}] {e}")

:adjudication = :Pended   via pendHighDollar — "Billed amount exceeds the auto-adjudication ceiling — human review"
  ├─ policyActiveOnServiceDate true is true   (asserted by the api)
  ├─ serviceCovered true is true   (asserted by the api)
  └─ billedAmount 48000 exceeds 10000   (asserted by the api)

[provenance_refused] adjudication may only be assigned by rules (horis:assignedBy horis:RulesOnly); assertion came from the api

Why verification matters here

This is the rule set where completeness is a compliance property: is there any claim this policy neither approves, pends, nor denies? There was. The check answered over the declared input space and rendered each gap as a sentence — a claim with no billedAmount recorded, which could be tested against neither approveClean's ceiling nor pendHighDollar's floor; and a claim where priorAuthRequired was never populated, which satisfied neither branch of approveClean's authorization test nor pendMissingPriorAuth's. Both now resolve to :Pended, which is the outcome this rule set already reached for missing documentation: pendMissingPriorAuth says pend for documentation, do not deny. Auto-denying a claim because a field was never populated is precisely the failure this overlay exists to argue against, and completeness is what turns that principle into something a check can enforce. Conflict-freedom is equally load-bearing — pendMissingPriorAuth and pendHighDollar can both match one claim and agree, so neither is a conflict; denyNonCoveredService and approveClean must never both match, and the check proves it rather than trusting the author. It did name four real overlaps, each a deny rule against a pend rule, all resolved by priority and now guarded explicitly. Dead-rule detection catches a ceiling that horis:min makes unreachable. The assumption manifest records which benefit-plan version and which code-system edition the closure assumed, so an auditor never has to infer scope from silence.

What verification does not claim: that the plan document was transcribed correctly into these rules, that the eligibility feed was complete, or that the clinical criteria behind serviceCovered are sound. Those are outside the closure and are stated as such.

Status and honest edges

• Runs today with structured input. Hydrating claims from a FHIR Claim/Coverage bundle with source versions in the proof, and returning a ClaimResponse or a CDS Hooks card conditionally, is PRP-008 territory.
• The research wiki deliberately deprioritizes prior authorization as a first Horismos deployment because of the harm record above — a maturity and liability judgment, not a technical one. The mechanism shown here is what a trustworthy deployment would need; when to deploy it is a human decision.
• Thresholds and rules are illustrative. A real plan has hundreds of clauses; the shape does not change.