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 is applicable to a propositional theory if and all theories are consistent. The application of this default to leads to the theory . An extension can be generated by applying the following algorithm: T = W /* current theory */ A = 0 /* set of defaults applied so far */ /* apply a sequence of defaults */ while there is a default d that is not in A and is applicable to T add the consequence of d to T add d to A /* final consistency check */ if for every default d in A T is consistent with all justifications of d then output T This algorithm is non-deterministic, as several defaults can alternatively be applied to a given theory . 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 is consistent with the background theory, the default can be applied, thus leading to the conclusion that is false. This result however undermines the assumption that has been made for applying the first default. Consequently, this theory has no extensions. In a normal default theory, all defaults are normal: each default has the form . A normal default theory is guaranteed to have at least one extension. Furthermore, the extensions of a normal default theory are mutually inconsistent, i.e., inconsistent with each other. 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: Skeptical a formula is entailed by a default theory if it is entailed by all its extensions; Credulous a formula is entailed by a default theory if it is entailed by at least one of its