Defeasibility and Multi-Stratum Reasoning

A defeasible rule is one that can be overridden. The classical example, going back to Reiter’s A Logic for Default Reasoning (1980): birds fly; penguins are birds; penguins do not fly. The rule “birds fly” is not wrong — it is defeasible, defeated by the more-specific rule “penguins do not fly.” A reasoning system that cannot represent this kind of layered exception either over-asserts or under-asserts, and either failure mode shows up as soon as a real-world domain enters the picture.

Argon supports defeasibility natively, following Governatori et al.’s formalization in Defeasible Logic: Agency, Intention and Obligation (DEON 2004) and the broader Defeasible Logic Programming tradition (García & Simari, Defeasible logic programming, TPLP 2004). The three layers — strict rules, defeasible rules with a superiority relation, and the resulting stratified evaluation — give unambiguous semantics independent of evaluation order.

This chapter covers the three decorators that mark and order defeasible rules, the Governatori three-stratum compilation that gives them their semantics, and the diagnostics that surface when the defeasibility graph contradicts itself.

The mechanism lives in oxc::stratify. Defeasibility composes with the three-engine derive pipeline (Chapter 2.4), the project-level [defeat] configuration (later in this chapter), and the multi-head disjunction stratification covered below.

Strict versus defeasible

A rule with no decorator is strict: when the body fires, the head holds, full stop. No other rule can defeat it.

pub derive ResidentialLeaseHasOneTenant(l: ResidentialLease) :-
    l: ResidentialLease,
    count(t for t in l.tenant) == 1

A rule marked @[default] is defeasible: it fires when nothing more specific overrides it.

@[default]
pub derive standard_security_deposit_applies(l: Lease) :-
    l: Lease

The default says: every lease falls under the standard security-deposit regime. Unless something more specific says otherwise. (The actual deposit value is computed by a compute keyed off whichever regime the lease classifies under.)

@[override(rule)] — pointing at a specific defeater

Mark a rule as overriding another by name:

@[override(standard_security_deposit_applies)]
pub derive rent_controlled_security_deposit_applies(l: Lease) :-
    l: Lease,
    rent_controlled(l)

When the body of rent_controlled_security_deposit_applies fires, it defeats standard_security_deposit_applies for that lease. The engine treats the two rules as in a superiority relation: the override is more specific.

@[override(rule)] is the most-explicit form of defeasibility. The override target is named explicitly; the dependency is local; the resolver can build the superiority graph statically at compile time.

@[defeat(rule)] — defeasibility as an effect of the body

A different shape: a rule whose body asserts the defeat of another rule, without contributing a positive head of its own.

@[defeat(standard_security_deposit_applies)]
pub derive prohibit_standard_deposit_regime(l: Lease) :-
    l: Lease,
    deposit_prohibited_jurisdiction(l)

@[defeat(rule)] is for the cases where the body’s effect is “this other rule does not apply” rather than a positive consequence. The body fires; the named rule is defeated for the bindings that satisfied the body. The defeat is the rule’s contribution to reasoning.

A companion decorator @[chain(rule)] declares that a defeasible rule chains through another — the chain link’s body assumes the chained rule’s head and the resulting derivation carries both rules’ provenance into the why-tree. This is the canonical pattern for layered regulatory reasoning where one rule’s conclusion is another rule’s premise:

@[default]
pub derive eligible_for_subsidy(t: Tenant) :-
    t: Tenant,
    t.household_income < poverty_line

@[chain(eligible_for_subsidy)]
pub derive senior_subsidy_amount(t: Tenant) -> Money :-
    t: Tenant,
    t.age >= 65
    => t.household_income * 0.4

Variants: _catalog/decorator-chain/{minimal,composition-with-defeasibility,multi-chain-link,idiom}/ and _catalog/decorator-defeat/{minimal,composition-with-default,negative-bad-args}/. The manifest-defeat/cross-package/ workspace shows the project-level [defeat] order strategy resolving conflicts across packages.

Governatori three-stratum compilation

The semantics of a defeasible-rule program is given by a three-stratum compilation, after Governatori (and the broader defeasible-logic-programming tradition).

Formally, let $\mathcal{R}={\mathcal{R}}_s\cup {\mathcal{R}}_d$ partition the rule set into strict rules ${\mathcal{R}}_s$ and defeasible rules ${\mathcal{R}}_d$, and let $>\subseteq {\mathcal{R}}_d\times {\mathcal{R}}_d$ be the superiority relation induced by the @[override] and @[defeat] annotations plus the configured [defeat] order strategies. The semantics of $(\mathcal{R},>)$ is the fixed-point of the three strata:

1. Stratum 1 — strict closure. ${\Delta }_1=T_{{\mathcal{R}}_s}^{\omega }(\varnothing )$, where $T_{{\mathcal{R}}_s}$ is the immediate-consequence operator over strict rules. These derivations are unconditional. Strict rules cannot be defeated; if a strict rule and a defeasible rule disagree on the same head, the strict rule wins by construction.
2. Stratum 2 — defeasible closure with superiority resolution. Starting from ${\Delta }_1$, add a defeasible derivation $r\in {\mathcal{R}}_d$ producing $\varphi$ from facts in ${\Delta }_1$ if and only if no rule $r^{\prime }>r$ produces $\neg \varphi$ from the same facts. Repeat to fixpoint ${\Delta }_2$. When two rules at incomparable priority disagree, the conflict is ambiguous (OE0401).
3. Stratum 3 — multi-head disjunction stratification. Multiple same-named defeasible rules form a Datalog disjunction: a fact holds if any of the rules fires. The disjunction’s contribution to the negation-as-failure layer is resolved by stratification, giving the final closure ${\Delta }_3$.

Each stratum reads from the completed state of the previous one. Stratum 2 cannot read its own in-progress state; that is what makes the compilation deterministic and the result independent of evaluation order.

The output is a triple $({\Delta }_1,{\Delta }_2,{\Delta }_3)$ together with, for each defeasible-rule application in ${\Delta }_2$, a record of which superiority-graph edge made the application win. Why-provenance traces back through the graph; a regulator can ask “which override produced this result?” and get a precise answer.

The superiority graph

The set of @[override] and @[defeat] annotations across a project induces a superiority graph: an edge A → B means rule A is more specific than rule B. The compiler:

• builds the graph from all annotations, across modules;
• checks for cycles (OE0403) — a cycle is an unrecoverable inconsistency in the modeller’s defeat-ordering;
• topologically sorts the graph to give Stratum 2 its priority order.

Cycle detection is binding. A cycle means two rules each claim to defeat the other; there is no consistent way to compute a fixed-point. The build fails.

OE0402 (“unreachable defeater”) fires when an @[override] or @[defeat] references a rule whose body could never fire under any interpretation — a static check that catches the kind of dead-code defeat-annotation that would otherwise pass silently.

Project-level [defeat] strategies

Some defeasibility orderings are systemic — not per-rule but per-project. Lex specialis (more specific wins), lex posterior (later wins), and lex superior (higher-status source wins) are the three classical orderings. Argon admits them as ordered project-level fallbacks:

[defeat]
order = ["explicit", "lex-specialis", "lex-posterior", "lex-superior"]

explicit is the per-rule annotations (@[override], @[defeat]). When two rules contradict and neither is explicitly annotated relative to the other, the engine consults the next strategy: lex specialis (the rule with the more-specific body wins). Then lex posterior (the rule defined later in source order wins). Then lex superior (the rule from the higher-priority package wins).

The four known strategies are explicit, lex-specialis, lex-posterior, lex-superior. Unknown strategies are OE1002. Empty order is allowed — it means “fall through to ambiguity diagnostics if no @[override] resolves.”

Mixed-strength rules and OE0207

A rule cannot be strict in some applications and defeasible in others. The compiler enforces this with OE0207 (“mixed-strength rules on same head”): if two rules with the same head differ in strength (one strict, one @[default]), the build fails. The fix is to make both defeasible or both strict — the modeller’s intent must be uniform.

This is a less-obvious constraint than it first appears. It catches the typical mistake of “I added an override but forgot to mark the original as defeasible,” which would otherwise silently produce contradictions.

Stratification and circular negation

NaF (negation as failure) interacts with defeasibility because both depend on a stratified evaluation order. A circular dependency through a NaF edge is OE0501 (“circular negation”); a program that cannot be stratified at all is OE0502 (“unstratifiable program”). Both are static checks; both fail the build.

The standard pattern that triggers OE0501:

pub derive A(x) :- not B(x)        // can A even be evaluated?
pub derive B(x) :- not A(x)        // ... we'd need to know B

The two rules cycle through a NaF edge. The compiler refuses to compile until the modeller breaks the cycle, typically by inserting a strict rule that grounds one of the predicates.

Multi-head disjunction

Multiple same-named @[default] derive rules form a disjunction: a fact holds if any of the rules fires. The pattern is canonical for genuine disjunctive reasoning where the head is the same predicate but the supporting bodies are independent:

@[default]
pub derive eligible_for_review(l: Lease) :-
    l: Lease,
    l.monthly_rent >= rent_review_threshold

@[default]
pub derive eligible_for_review(l: Lease) :-
    l: Lease,
    rent_controlled(l)

@[default]
pub derive eligible_for_review(l: Lease) :-
    l: Lease,
    l.tenant.is_senior

A lease is eligible for review if any one of the three conditions holds; the why-provenance tags whichever rule fired so a consumer can ask “which branch matched?” and get a precise answer. Mixing strict and defeasible rules under the same head is OE0207 for the same reason single-head mixed-strength is rejected.

Refinement-type interaction

The refinement-type fragment (Chapter 2.6) interacts with defeasibility through the three-valued semantics. A refinement-type predicate where { ... } is decided per $K3$ (Kleene’s strong three-valued logic) with the Pietz-Rivieccio “Exactly True” designation: only IS admits membership, CAN does not. When a defeasible rule conditions on the refinement-type narrowing, the rule fires only if the narrowing is IS — the narrowing itself can be defeated by an override rule that asserts the converse. The corner cases are rare; the semantics is well-defined when they do come up.

Worked example — regulatory-regime classification

The lease tutorial does not yet exercise defeasibility, but the pattern is straightforward to add. Imagine rules.ar extended with:

@[default]
pub derive lease_governance_standard(l: Lease) :-
    l: Lease

@[override(lease_governance_standard)]
pub derive lease_governance_rent_controlled(l: Lease) :-
    l: Lease,
    rent_controlled(l)

@[override(lease_governance_rent_controlled)]
pub derive lease_governance_senior_rent_controlled(l: Lease) :-
    l: Lease,
    rent_controlled(l),
    l.tenant.is_senior

Three classification rules, each more specific than the last. The superiority graph is a chain: senior_rent_controlled → rent_controlled → standard. For a senior tenant in a rent-controlled lease, all three bodies fire; the engine applies them in topological order; lease_governance_senior_rent_controlled wins; the lease classifies under the senior-rent-controlled regime.

For a non-senior tenant in a rent-controlled lease, only the first two bodies fire; lease_governance_rent_controlled wins; the lease classifies under the rent-controlled regime.

For a market-rate lease, only the first body fires; lease_governance_standard wins; the lease classifies under the standard regime.

A separate compute keyed off the regime predicate produces the actual security-deposit cap, monthly-rent ceiling, or whatever the regime determines. Defeasibility classifies; the compute calculates. The why-provenance for each classification tags which override won, giving the regulator a precise audit trail.

Diagnostics worth knowing

ox explain <code> prints the long-form explanation and the canonical fix.

Why a stratified semantics

A naïve “first-rule-wins” or “most-recent-rule-wins” approach to defeasibility is brittle: rule order in source becomes load-bearing, refactors silently change behavior, and the result depends on evaluation order. The Governatori three-stratum compilation gives unambiguous semantics that is independent of evaluation order — multiple paths through the strata produce the same result, by construction.

This is what makes the defeasibility layer composable. A package can ship rules with their own @[override] annotations; a downstream package can add more rules, more annotations, even override rules from the upstream package; the resulting superiority graph is the union; the semantics stays well-defined; and the compiler tells you when the union has a cycle or an ambiguity.

What’s next

Chapter 5.3 covers the tier ladder; defeasibility’s stratification interacts with tier classification (NaF can lift a rule up the ladder). Chapter 5.4 covers standpoints; defeasibility orderings differ between standpoints, and the same rule pair can have different superiority outcomes depending on which standpoint the query runs against. Chapter 5.1 covers the meta-property calculus that powers Tier-0 reasoning — a substrate the defeasibility layer reads but does not modify.