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:

+Δq (strict proof), OR
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.

Symbol	Unicode	Name	Meaning
→	U+2192	Strict rule	Definite conclusion
⇒	U+21D2	Defeasible rule	Default conclusion
⇝	U+21DD	Defeater	Blocking rule
>	—	Priority	Rule ordering
+∂	—	Positively defeasible	Defeasibly proved
-∂	—	Negatively defeasible	Not defeasibly proved
+Δ	—	Positively definite	Strictly proved
∼	U+223C	Negation as failure	Not provable

Metatheory. Defeasible logic is decidable with linear complexity in theory size — more efficient than default logic. Sound and complete proof theory. Can represent default logic and logic programming (under appropriate translations). Coherent: no +∂q and +∂¬q simultaneously. Ambiguity propagating vs blocking variants exist.

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. Priority ordering must be given — no automatic derivation. Different variants (ambiguity propagating, blocking) give different answers. Less studied than default logic in academic literature. Defeaters are sometimes hard to understand. Team defeat strategies vary. No standard on handling loops or mutual defeat.