Default logic is a non-monotonic logic proposed by Raymond Reiter to formalize reasoning with default assumptions.
Contents
- Syntax of default logic
- Examples
- Restrictions
- Semantics of default logic
- Entailment
- Alternative default inference rules
- Variants of default logic
- Translations
- Complexity
- Implementations
- References
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. A classical example is: “birds typically fly”. This rule can be expressed in standard logic either by “all birds fly”, which is inconsistent with the fact that penguins do not fly, or by “all birds that are not penguins and not ostriches and ... fly”, which requires all exceptions to the rule to be specified. Default logic aims at formalizing inference rules like this one without explicitly mentioning all their exceptions.
Syntax of default logic
A default theory is a pair
According to this default, if we believe that Prerequisite is true, and each of
The logical formulae in W and all formulae in a default were originally assumed to be first-order logic formulae, but they can potentially be formulae in an arbitrary formal logic. The case in which they are formulae in propositional logic is one of the most studied.
Examples
The default rule “birds typically fly” is formalized by the following default:
This rule means that, if X is a bird, and it can be assumed that it flies, then we can conclude that it flies. A background theory containing some facts about birds is the following one:
According to this default rule, a condor flies because the precondition Bird(Condor) is true and the justification Flies(Condor) is not inconsistent with what is currently known. On the contrary, Bird(Penguin) does not allow concluding Flies(Penguin): even if the precondition of the default Bird(Penguin) is true, the justification Flies(Penguin) is inconsistent with what is known. 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. Deriving the antecedents of an inference rule from the consequences is a form of explanation of the consequences, and is the aim of abductive reasoning.
A common default assumption is that what is not known to be true is believed to be false. This is known as the Closed World Assumption, and is formalized in default logic using a default like the following one for every fact F.
For example, the computer language Prolog uses a sort of default assumption when dealing with negation: if a negative atom cannot be proved to be true, then it is assumed to be false. Note, however, that Prolog uses the so-called negation as failure: when the interpreter has to evaluate the atom
Restrictions
A default is categorical or prerequisite-free if it has no prerequisite (or, equivalently, its prerequisite is tautological). A default is normal if it has a single justification that is equivalent to its conclusion. A default is supernormal if it is both categorical and normal. A default is seminormal if all its justifications entail its conclusion. A default theory is called categorical, normal, supernormal, or seminormal if all defaults it contains are categorical, normal, supernormal, or seminormal, respectively.
Semantics of default logic
A default rule can be applied to a theory if its precondition is entailed by the theory and its justifications are all consistent with the theory. The application of a default rule leads to the addition of its consequence to the theory. Other default rules may then be applied to the resulting theory. When the theory is such that no other default can be applied, the theory is called an extension of the default theory. The default rules may be applied in different order, and this may lead to different extensions. The Nixon diamond example is a default theory with two extensions:
Since Nixon is both a Republican and a Quaker, both defaults can be applied. However, applying the first default leads to the conclusion that Nixon is not a pacifist, which makes the second default not applicable. In the same way, applying the second default we obtain that Nixon is a pacifist, thus making the first default not applicable. This particular default theory has therefore two extensions, one in which Pacifist(Nixon) is true, and one in which Pacifist(Nixon) is false.
The original semantics of default logic was based on the fixed point of a function. The following is an equivalent algorithmic definition. If a default contains formulae with free variables, it is considered to represent the set of all defaults obtained by giving a value to all these variables. A default
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. As a result, two extensions are generated: one in which Nixon is a pacifist and one in which Nixon is not a pacifist.
The final check of consistency of the justifications of all defaults that have been applied implies that some theories do not have any extensions. In particular, this happens whenever this check fails for every possible sequence of applicable defaults. The following default theory has no extension:
Since
In a normal default theory, all defaults are normal: each default has the form
Entailment
A default theory can have zero, one, or more extensions. 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. Consequently, neither Pacifist(Nixon) nor ¬Pacifist(Nixon) are skeptically entailed, while both of them are credulously entailed. As this example shows, the credulous consequences of a default theory may be inconsistent with each other.
Alternative default inference rules
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.
Variants of default logic
The following variants of default logic differ from the original one on both syntax and semantics.
Translations
Default theories can be translated into theories in other logics and vice versa. The following conditions on translations have been considered:
Translations are typically required to be faithful or at least consequence-preserving, while the conditions of modularity and same alphabet are sometimes ignored.
The translatability between propositional default logic and the following logics have been studied:
Translations exist or not depending on which conditions are imposed. Translations from propositional default logic to classical propositional logic cannot always generate a polynomially sized propositional theory, unless the polynomial hierarchy collapses. Translations to autoepistemic logic exists or not depending on whether modularity or the use of the same alphabet is required.
Complexity
The computational complexity of the following problems about default logic is known:
Implementations
Three systems implementing default logics are DeReS, XRay and GADeL