Default logic

Default logic is a formalism for representing conclusions that are accepted in the absence of contrary information and withdrawn when such information becomes available. It belongs to the family of non-monotonic logics, in which adding premises can invalidate conclusions that previously followed from a knowledge base. This behavior distinguishes default consequence from classical entailment, where every consequence of a set of premises remains a consequence after further premises are added.

The formalism was introduced in its standard form by Raymond Reiter in 1980. During the 1979–1980 development of the framework, Reiter and You Watanabe analyzed the fixed-point construction used to define extensions, including the treatment of defaults whose justifications remain individually consistent but cannot be accepted jointly. The resulting semantics represented defeasible inference through sets of deductively closed beliefs rather than through a modification of the truth conditions of classical formulas.

Historical context

Research on default logic developed from attempts to formalize common-sense reasoning. Classical logic represents universally valid implications directly, but ordinary knowledge frequently has the weaker form that an implication applies unless an exception is established. The statement that birds normally fly, for example, does not assert that every bird flies. Encoding it as a material implication would incorrectly make flight a necessary property of every bird, while omitting it would prevent the intended conclusion in ordinary cases.

Several related formalisms emerged during the same period. John McCarthy formulated circumscription as a method for minimizing the extensions of selected predicates. Drew McDermott and Jon Doyle developed a modal approach to non-monotonic inference based on consistency and self-reference. Reiter’s formulation instead treated defaults as explicit inference rules and characterized acceptable belief sets through fixed points.

These approaches addressed a limitation of earlier systems based on procedural rules. A purely operational rule language can describe the order in which conclusions are generated, but its results may depend on the implementation’s rule-selection policy. Default logic separates the declarative content of a default theory from methods used to compute its consequences, although the theory itself can still possess several distinct extensions.

Syntax

A default theory is an ordered pair

[ \Delta=(W,D), ]

where (W) is a set of formulas in an underlying first-order logic, and (D) is a set of default rules. The formulas in (W) represent established information and are interpreted according to ordinary deductive consequence.

A default rule has the form

[ \frac{\alpha:\beta_1,\ldots,\beta_n}{\gamma}. ]

The formula (\alpha) is the prerequisite. Each formula (\beta_i) is a justification, while (\gamma) is the consequent. The intended reading is that (\gamma) may be accepted when (\alpha) has been derived and when none of the negations (\neg\beta_i) is included in the relevant set of beliefs.

The colon does not denote a classical connective. It separates the prerequisite from the conditions whose consistency permits application of the rule. A default therefore cannot in general be replaced by the material implication

[ \alpha\rightarrow\gamma, ]

because a material implication remains applicable even when evidence contradicting the default conclusion is present.

A default is called normal when its justification and consequent are identical:

[ \frac{\alpha:\beta}{\beta}. ]

Normal defaults express many familiar defeasible generalizations. The rule

[ \frac{\operatorname{Bird}(x):\operatorname{Flies}(x)} {\operatorname{Flies}(x)} ]

permits the conclusion that a known bird flies when assuming its flight is consistent with the completed belief set.

A prerequisite-free default has no substantive prerequisite and is written

[ \frac{:\beta}{\gamma}. ]

Such a rule represents a defeasible assumption that does not depend on a previously established antecedent. A semi-normal default places the consequent among the conditions represented in its justification, commonly through a rule of the form

[ \frac{\alpha:\beta\land\gamma}{\gamma}. ]

Defaults containing variables require an account of their applicable instances. In the standard first-order treatment, the semantic definition is stated for closed defaults, and open defaults are represented through their closed instances over the language of the theory.

Extension semantics

The central semantic concept is an extension, which represents a deductively complete set of beliefs that supports its own applications of default rules. For a proposed set of formulas (E), the operator (\Gamma_\Delta(E)) is defined as the smallest set satisfying three conditions. It contains every formula in (W), it is closed under classical consequence, and it contains (\gamma) whenever a default

[ \frac{\alpha:\beta_1,\ldots,\beta_n}{\gamma} ]

has (\alpha) in (\Gamma_\Delta(E)) while no formula (\neg\beta_i) belongs to (E).

A set (E) is an extension of (\Delta) precisely when

[ E=\Gamma_\Delta(E). ]

This definition separates the generation of conclusions from the consistency tests governing defaults. Prerequisites are evaluated against the set being generated, whereas justification failures are evaluated against the proposed extension as a whole. The apparent circularity is intentional: an extension must contain exactly the conclusions supported when that same extension determines which justifications remain consistent.

The definition also explains why default logic is non-monotonic. Suppose that (W) initially contains

[ \operatorname{Bird}(a), ]

and (D) contains the normal default concerning flight. An extension then contains (\operatorname{Flies}(a)). If the established information is enlarged by adding

[ \neg\operatorname{Flies}(a), ]

the consistency condition for the default fails, so the expanded theory does not retain the former default conclusion merely because it followed before the new premise was introduced.

Extensions are not arbitrary models of a collection of formulas. They are fixed points determined by the interaction between classical closure and defeasible rules. A theory can have one extension, several extensions, or no extension. The last two cases express structural properties of the formal theory rather than uncertainty about which rules were written into it.

Conflicting defaults

Multiple extensions arise when incompatible defaults can each support a stable interpretation. A standard example uses an individual who is both a Quaker and a Republican, together with one default associating Quakers with pacifism and another associating Republicans with non-pacifism. The background theory is

[ W={\operatorname{Quaker}(n),\operatorname{Republican}(n)}, ]

and the defaults are

[ \frac{\operatorname{Quaker}(x):\operatorname{Pacifist}(x)} {\operatorname{Pacifist}(x)} ]

and

[ \frac{\operatorname{Republican}(x):\neg\operatorname{Pacifist}(x)} {\neg\operatorname{Pacifist}(x)}. ]

One extension contains (\operatorname{Pacifist}(n)), which blocks the justification of the second default. Another contains (\neg\operatorname{Pacifist}(n)), which blocks the justification of the first. Neither extension is selected merely by the syntactic order in which the defaults are displayed.

This phenomenon distinguishes conflicts between defaults from inconsistencies in the background theory. When (W) is classically inconsistent, its deductive closure contains every formula under ordinary explosive consequence. By contrast, incompatible defaults can yield several individually consistent extensions without making the established premises inconsistent.

Priority information is not part of Reiter’s basic semantics. A system in which one default overrides another because it is more specific, more recent, or explicitly ranked requires an extension such as prioritized default logic. Specificity can sometimes be encoded within prerequisites and justifications, but the unextended formalism does not derive a general priority ordering from the linguistic interpretation of its predicates.

Skeptical and credulous consequence

When a default theory has several extensions, consequence can be defined by quantifying over them. A formula is a skeptical consequence when it belongs to every extension. It is a credulous consequence when it belongs to at least one extension.

For the conflicting-default theory above, the facts that the individual is a Quaker and a Republican are skeptical consequences because they occur in the background theory and therefore in every extension. Pacifism is only a credulous consequence, as is its negation, because each occurs in one extension but not the other.

These relations capture different interpretations of defeasible acceptance. Skeptical consequence retains only conclusions invariant across all stable resolutions of the defaults. Credulous consequence records conclusions supported by at least one stable resolution, without combining incompatible extensions into a single belief set.

The distinction also affects computational analysis. Determining whether a formula occurs in some extension and determining whether it occurs in every extension involve different quantifier structures over candidate fixed points. For propositional default theories, central reasoning tasks occupy levels of the polynomial hierarchy above ordinary propositional satisfiability, and the exact classification depends on the permitted form of defaults and the selected consequence relation.

Relation to logic programming

Default logic has a close formal relationship with logic programming under negation as failure. A logic-programming rule such as

[ p \leftarrow q,\ \operatorname{not}\ r ]

can be associated with a default whose prerequisite requires (q) and whose justification requires consistency with (\neg r). The correspondence becomes especially direct for restricted propositional theories and for programs interpreted under stable model semantics.

The two frameworks nevertheless organize their syntax differently. Logic programs use rule bodies containing positive and default-negated literals, whereas default logic explicitly distinguishes prerequisites from justifications. Stable models are sets of atoms or literals determined by a program reduct, while extensions are deductively closed theories determined through the operator (\Gamma_\Delta).

Autoepistemic logic provides another closely related representation. Its modal operator expresses what an idealized reasoner believes, allowing defaults to be translated into formulas whose applicability depends on the absence of a belief in contrary information. Under suitable translations, stable expansions of autoepistemic theories correspond to extensions of associated default theories, although direct translations can preserve different properties depending on the syntactic fragment.

Representation and limitations

Default logic represents exceptions by preventing the application of a rule rather than by assigning a reduced numerical probability to its conclusion. It therefore differs from Bayesian inference, where uncertainty is represented quantitatively and evidence changes probability distributions. A default justification records consistency with a belief set, not the frequency of a property or the probability that a conclusion is true.

The formalism also differs from defeasible logic, which commonly provides explicit rule types and a proof theory for resolving conflicts. Reiter default logic gives conflicts semantic expression through extensions and does not include an intrinsic superiority relation among rules.

The extension mechanism makes the global organization of a theory significant. A default can be locally applicable with respect to established facts but fail to occur in an extension because its justification conflicts with conclusions generated elsewhere in that same extension. Consequently, default applicability is not reducible to a one-pass test against the original background theory.

The existence of theories without extensions follows from this self-referential structure. Such a theory demands a set of beliefs whose assumed contents invalidate the rules needed to generate those contents, while excluding them can reactivate the same rules. Normal default theories avoid part of this behavior: every closed normal default theory has at least one extension, provided the underlying classical assumptions satisfy the standard consistency conditions.