Default logic can express facts like “by default, something is true”; by contrast, standard logic can only express that something is true or that something is false.
This is a problem because reasoning often involves facts that are true in the majority of cases but not always.
Default logic aims at formalizing inference rules like this one without explicitly mentioning all their exceptions.
W is a set of logical formulas, called the background theory, that formalize the facts that are known for sure.
is consistent with our current beliefs, we are led to believe that Conclusion is true.
From this background theory and this default, Bird(Bee) cannot be concluded because the default rule only allows deriving Flies(X) from Bird(X), but not vice versa.
A common default assumption is that what is not known to be true is believed to be false.
Note, however, that Prolog uses the so-called negation as failure: when the interpreter has to evaluate the atom
A default is normal if it has a single justification that is equivalent to its conclusion.
A default theory is called categorical, normal, supernormal, or seminormal if all defaults it contains are categorical, normal, supernormal, or seminormal, respectively.
The application of a default rule leads to the addition of its consequence to the theory.
The original semantics of default logic was based on the fixed point of a function.
An extension can be generated by applying the following algorithm: This algorithm is non-deterministic, as several defaults can alternatively be applied to a given theory T. In the Nixon diamond example, the application of the first default leads to a theory to which the second default cannot be applied and vice versa.
The final check of consistency of the justifications of all defaults that have been applied implies that some theories do not have any extensions.
is consistent with the background theory, the default can be applied, thus leading to the conclusion that
This result however undermines the assumption that has been made for applying the first default.
Entailment of a formula from a default theory can be defined in two ways: Thus, the Nixon diamond example theory has two extensions, one in which Nixon is a pacifist and one in which he is not a pacifist.
As this example shows, the credulous consequences of a default theory may be inconsistent with each other.
The following alternative inference rules for default logic are all based on the same syntax as the original system.
The justified and constrained versions of the inference rule assign at least an extension to every default theory.
The following variants of default logic differ from the original one on both syntax and semantics.
Translations to autoepistemic logic exist or not depending on whether modularity or the use of the same alphabet is required.
The computational complexity of the following problems about default logic is known: Four systems implementing default logics are DeReS[permanent dead link], XRay, GADeL Archived 2007-04-06 at the Wayback Machine, and Catala.