Toward Robust Legal Text Formalization into Defeasible Deontic Logic using LLMs is a rule-based non-monotonic formalism for representing legal norms and automating its evaluation. It combines defeasible logic — which models rules that hold by default but can be overridden by exceptions — with deontic logic, which provides the vocabulary of obligations, permissions, and prohibitions. Together, these make it well-suited to insurance law, where coverage obligations are established by grants, narrowed by exclusions, and partially restored by exceptions to those exclusions. This three-layer structure maps precisely onto DDL's core mechanism: defeasible rules ordered by a superiority relation, so that an exclusion defeats a grant, and an exception defeats the exclusion in turn.

The system described here uses DDL as the semantic backbone for automated coverage determination. A preprocessing pipeline converts structured policy clauses into typed, prioritised DDL rules. A forward pass then applies those rules to claim facts to produce a coverage decision together with a full, auditable reasoning trace. Both stages rely on prompting rather than training, making the approach directly deployable on any sufficiently capable language model.

What "governs" means — and why it is not the same as "relevant"

A common mistake in building these systems is equating governing with semantic similarity: the water exclusion is relevant to any water-related claim, so it governs. That is the wrong test.

In Defeasible Deontic Logic a clause governs a claim if and only if every one of its antecedent conditions is satisfied by the claim facts. This is applicability — a logical check, not a similarity score. A fire exclusion is semantically relevant to any property loss — it is an exclusion about physical perils — but it does not govern a water damage claim because "damage caused by fire" is simply false given the facts. A retrieval system based on embeddings would surface it; the applicability test correctly excludes it.

That one distinction — governs = all conditions satisfied, not semantically close — is the whole reason the preprocessing pipeline exists. Its job is to make each clause's conditions explicit enough to test.

Pre-Processing Insurance Conditions

┌──────────────────────────────────────┐
│ Section text │
│ with resolved definitions │
└──────────────────┬───────────────────┘
 │
 [LLM]
 │
 ▼
┌──────────────────────────────────────┐
│ Classify + extract │
│ List[ClauseExtraction] │
└──────────────────┬───────────────────┘
 │
 [rule-based]
 │
 ▼
┌──────────────────────────────────────┐
│ Assign priority per clause │
│ exception > exclusion > grant │
└──────────────────┬───────────────────┘
 │
 ▼
┌──────────────────────────────────────┐
│ List[ProcessedClause] │
│ type · antecedents · priority │
└──────────────────────────────────────┘

There are essentially two steps per section and one rule-based step.

Step 1 — Classify and extract (one LLM call per section)

The model receives a full policy section and returns all clauses it contains, each labelled with its DDL type and governing conditions.

You are formalizing all clauses in an insurance policy section.

Section path: {section_path}
Section text: {section_text}
Definitions used in this section: {resolved_definitions}

For each distinct normative unit (clause) in this section:
1. Assign a clause_id (e.g. "s3_c01", incrementing per clause)
2. Classify the clause type:
 - grant: establishes the insurer's obligation to cover a loss
 - exclusion: removes coverage for specific circumstances
 - exception: restores coverage that an exclusion removed
 - definition: fixes the meaning of a term
 - condition: a duty on the policyholder or insurer
3. List the antecedents — the conditions that must ALL hold for this
 clause to apply. Express each as a plain English statement,
 e.g. "the damage was caused by water".
4. State the conclusion: what follows when all antecedents hold.

Return a JSON array of clause extractions.

class ClauseExtraction(BaseModel):
 clause_id: str
 clause_type: Literal["grant", "exclusion", "exception", "definition", "condition"]
 antecedents: List[str] # e.g. ["damage was caused by water"]
 conclusion: str # e.g. "the insurer is not obliged to pay"

# The LLM returns:
List[ClauseExtraction]

Step 2 — Assign priority (rule-based, no LLM)

PRIORITY = {"exception": 3, "exclusion": 2, "grant": 1, "definition": 0, "condition": 0}

Stored clause unit (full index entry)

class ProcessedClause(BaseModel):
 clause_id: str
 clause_type: Literal["grant", "exclusion", "exception", "definition", "condition"]
 antecedents: List[str]
 conclusion: str
 priority: int # derived from PRIORITY lookup

Forward Pass — Deciding a Claim

┌──────────────────┐ ┌────────────────┐
│ Claim facts │ │ Clause index │
└────────┬─────────┘ └───────┬────────┘
 │ │
 └─────────────┬─────────────┘
 │
 [LLM]
 │
 ▼
┌──────────────────────────────────────────────┐
│ Applicability check │
│ do facts satisfy all antecedents? │
│ governs ≠ similar │
└─────────────────────┬────────────────────────┘
 │
 [applicable only]
 │
 ▼
┌──────────────────────────────────────────────┐
│ Contest │
│ applicable clauses that conflict │
└─────────────────────┬────────────────────────┘
 │
 [superiority]
 │
 ▼
┌──────────────────────────────────────────────┐
│ Priority resolution │
│ superior clause overrides the rest │
└─────────────────────┬────────────────────────┘
 │
 ▼
┌──────────────────────────────────────────────┐
│ Decision trace │
│ decision and which rule prevailed │
└──────────────────────────────────────────────┘

The applicability prompt (one call per candidate clause) makes the governing test explicit:

Claim facts:
{claim_facts}

Clause antecedents:
{antecedents}

For each antecedent, decide whether the claim facts satisfy it.
A clause governs this claim only when ALL antecedents are satisfied.

Return JSON: for each antecedent, {antecedent, satisfied: bool, reason}.
Then: governs: bool.

Decision trace — burst pipe example

Claim: "A pipe inside the kitchen wall burst suddenly. Water flooded and damaged the kitchen floor."

Step 1 — Applicability check

EXCL-07 is semantically relevant — it is an exclusion about a physical peril, the same category as EXCL-03. A naive retrieval system would surface it. The applicability check correctly excludes it: "damage caused by fire" is not satisfied by the facts. This is the governs/relevant distinction in action.

Step 2 — Contest (governing clauses with conflicting conclusions)

GRANT-01 → covered · EXCL-03 → not covered · EXCPT-03a → covered

Step 3 — Priority resolution

The trace is: GRANT-01 → overridden by EXCL-03 → overridden by EXCPT-03a → covered.

The core insight is that the applicability prompt is not asking whether a clause is about the same topic as the claim. It is asking whether all the conditions listed in the clause's antecedents are true given the specific claim facts. That shift — from topic similarity to condition satisfaction — is what Defeasible Deontic Logic formalises, and what separates a system that correctly identifies governing clauses from one that merely retrieves thematically related ones.