Defeasible Logic

Origin. Donald Nute developed defeasible logic (1980s-1994). Practical non-monotonic reasoning with explicit rules and priorities. Designed for efficient computation unlike some other non-monotonic logics. Used in legal reasoning, business rules, and agent systems. Related to but distinct from default logic and argumentation.

Models. Rules that can be defeated by stronger rules. Three rule types: strict (always apply), defeasible (normally apply), defeaters (block conclusions). Priorities among rules resolve conflicts. A conclusion is defeasibly proved if supported by undefeated argument chains.

Formalism.

Rule types:

• Strict rules: A₁, ..., Aₙ → B (if premises, then certainly B)
• Defeasible rules: A₁, ..., Aₙ ⇒ B (if premises, then presumably B)
• Defeaters: A₁, ..., Aₙ ⇝ B (if premises, might block ¬B, but don't prove B)

Defeasible theory: D = (F, R, >) where:

• F: facts (initial truths)
• R: set of rules (strict, defeasible, defeaters)

• : priority ordering on rules

Proof theory: +∂q: q is defeasibly provable -∂q: q is not defeasibly provable +Δq: q is strictly provable -Δq: q is not strictly provable

Proof conditions for +∂q:

1. +Δq (strict proof), OR
2. All of:
   • ∃ applicable rule r for q (premises proved)
   • ¬-Δ¬q (¬q not strictly proved)
   • Every applicable rule s for ¬q is either:
     • Defeated by a stronger rule for q, OR
     • Has a blocked premise

Team defeat: An argument for ¬q is countered if a superior rule concludes q.

Example:

r1: bird(X) ⇒ flies(X)
r2: penguin(X) ⇒ ¬flies(X)
r3: penguin(X) → bird(X)
r2 > r1
bird(tweety)
penguin(opus)

Result: +∂flies(tweety), +∂¬flies(opus)

Symbols.

Metatheory. A defeasible theory D = (F, R, >) determines its conclusions uniquely: the four tags +Δ, -Δ, +∂, -∂ are fixed by a mutual recursion over the rules, so there are no extensions to choose among and the formalism is skeptical by construction rather than by a further selection principle. Billington established the structural properties: the logic is consistent, and it is coherent, in that +∂q and +∂¬q are never both derivable unless the strict rules together with the facts are already inconsistent. Maher (2001) proved that propositional defeasible logic has linear complexity — the full set of conclusions of a theory is computable in time linear in its size — which separates it sharply from default logic, where existence of an extension is Σ₂ᵖ-complete, and from circumscription. Antoniou, Billington, Governatori and Maher (2001) proved representation results: defeaters and the superiority relation are each eliminable, since every defeasible theory has a conclusion-equivalent theory without them at the cost of new propositions, so both are conveniences rather than sources of expressive power. Ambiguity-blocking and ambiguity-propagating defeasible logic are distinct consequence relations, not two presentations of one.

Applies to. Legal reasoning (regulations with exceptions). Business rules (policies with overrides). Agent deliberation. Regulatory compliance. Contracts. Expert systems with exceptions. RuleML and industry standards.

Limitations. Rule heads are literals, so disjunctive conclusions cannot be stated at all, and the language has no quantifiers: variables in rules are schematic, and a predicate theory must be grounded before the proof theory applies, which costs exponentially in the number of variables and confines Maher's linear bound to the propositional case. The superiority relation is an input, required acyclic, and nothing in the logic derives or justifies it. Being skeptical by construction, the logic cannot represent genuinely alternative positions: it yields one determinate set of tagged conclusions, never a family of extensions, so there is no credulous reading to fall back on. Defeaters block without supporting, so their effect cannot be chained into further conclusions. Ambiguity blocking versus propagating, and team defeat versus individual defeat, change what is provable, and the formalism offers no criterion for choosing between them.

© 2026 Lingenic LLC