Default Logic

Origin. Raymond Reiter introduced default logic (1980). A formalization of non-monotonic reasoning: conclusions that hold "by default" and can be retracted when contradicting information arrives. Part of the broader study of non-monotonic logics (circumscription, autoepistemic logic). Models commonsense reasoning where we reason with incomplete information.

Models. Defeasible inference. "Birds typically fly" — conclude flying unless you know otherwise. Unlike classical logic, adding premises can retract conclusions. Defaults are rules that apply when their prerequisites are met and nothing contradicts their justification.

Formalism.

Default rule: α : β₁, ..., βₙ ───────────── γ

Meaning: If α is believed, and each βᵢ is consistent with beliefs, then conclude γ.

• α: prerequisite (what must be known)
• β₁, ..., βₙ: justifications (what must be consistent)
• γ: consequent (what to conclude)

Example: Bird(x) : Flies(x) ───────────────── Flies(x)

"If x is a bird, and it's consistent that x flies, conclude x flies."

Default theory: A pair (D, W) where:

• W: set of first-order formulas (facts)
• D: set of default rules

Extension: A set of beliefs E closed under:

1. Classical consequence of W
2. Application of defaults whose prerequisites are in E and justifications are consistent with E

A default theory may have zero, one, or multiple extensions.

Types of defaults:

• Normal default: α : β / β (justification = consequent)
• Semi-normal: α : β ∧ γ / γ
• Non-normal: more complex justifications

Closed-world assumption as default: : ¬P(x) ──────── ¬P(x)

"If P(x) is not provable, assume ¬P(x)."

Skeptical vs credulous reasoning:

• Skeptical: believe only what's in ALL extensions
• Credulous: believe what's in SOME extension

Symbols.

Metatheory. Reiter (1980) defined an extension of (D, W) as a fixed point of an operator Γ: E is an extension exactly when E = Γ(E), where Γ(S) is the smallest deductively closed superset of W containing γ for every default α : β₁, ..., βₙ / γ whose prerequisite α lies in Γ(S) and none of whose ¬βᵢ lies in S. The consistency test looks at the completed set S, which is why the definition is a fixed point rather than a derivation, and Reiter's quasi-inductive characterization as a union of stages is what makes extensions computable at all. He proved that every normal default theory has at least one extension and that normal theories are semi-monotonic: enlarging D never destroys an extension, since each extension of the smaller theory is contained in one of the larger. Non-normal theories may have none — {: p / ¬p} has no extension. Gottlob (1992) settled the propositional complexity: existence of an extension and credulous membership are both Σ₂ᵖ-complete, skeptical membership Π₂ᵖ-complete. Konolige (1988) embedded default logic in autoepistemic logic.

Applies to. Commonsense reasoning. Incomplete databases (closed-world reasoning). Legal reasoning (defeasible rules). Diagnosis (assume normal unless evidence of fault). Planning under incomplete information. Agent beliefs with uncertainty.

Limitations. A non-normal theory can have no extension, and then the skeptical relation degenerates: everything is vacuously in all extensions. Where several extensions exist the theory ranks none above another, so priorities must be supplied by a separate prioritized formalism rather than derived. Default logic is not cumulative — Makinson showed that adding to W a formula already belonging to every extension can change which extensions the theory has — so the consequence operation does not stabilize under its own outputs. Semi-monotonicity holds only for normal theories; with non-normal defaults a new default can eliminate an existing extension. The consistency test on justifications is applied to the completed extension, which makes the definition non-constructive, and in the first-order case that test is a satisfiability check, so extensions are not effectively computable. Defaults are rules, not formulas: they cannot be nested, negated or quantified over, and no deduction theorem holds.

© 2026 Lingenic LLC