Jump to content

Default logic: Difference between revisions

From Wikipedia, the free encyclopedia
Content deleted Content added
rewritten introductive paragraph with a classical example
syntax of default logic
Line 5: Line 5:


==Syntax of Default Logic==
==Syntax of Default Logic==
A default theory consists of a pair <math>\langle D, W \rangle</math>, where <math>W</math> is a set of logical formulae, called ''the background theory'', and <math>D</math> is a set of default inference rules called ''default rules'', each one of the form:
A default theory is a pair <math>\langle D, W \rangle</math>. <math>W</math> is a set of logical formulae, called ''the background theory'', that formalize the facts that are known for sure. <math>D</math> is a set of default inference rules called ''default rules'', each one of the form:


: <math>\frac{Prerequisite : Justification_1, ..., Justification_n}{Conclusion}</math>
: <math>\frac{Prerequisite : Justification_1, ..., Justification_n}{Conclusion}</math>


This default rule expresses that if we know that <math>Prerequisite</math> is true, and each of <math>Justification_i</math> is consistent with our current knowledge, then <math>Conclusion</math> is true.
Such a default rule formalize the fact that, if we know that <math>Prerequisite</math> is true, and each of <math>Justification_i</math> is consistent with our current knowledge, then <math>Conclusion</math> is true.


The logical formulae in <math>W</math>, and all formulae in a default were originally assumed to be in [[first-order logic]], but 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.
The logical formulae in <math>W</math>, and all formulae in a default were originally assumed to be in [[first-order logic]], but 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===
==Some Default Theories==
The example of birds can be formalized using the following first-order default:
The default rule &ldquo;birds typically fly&rdquo; is formalized by the following first-order default:


:<math>D = \left\{ \frac{Bird(X) : Flies(X)}{Flies(X)} \right\} </math>
:<math>D = \left\{ \frac{Bird(X) : Flies(X)}{Flies(X)} \right\}</math>


This default has a single justification, which is equal to its conclusion; this is not always the case. The background theory contains facts that are known. In the case of birds, a background theory might be the following one:
This rule means that, if <math>X</math> 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:


:<math>W = \{ Bird(Condor), Bird(Penguin), \neg Flies(Penguin), Flies(Airplane) \}</math>.
:<math>W = \{ Bird(Condor), Bird(Penguin), \neg Flies(Penguin), Flies(Eagle)) \}</math>.


The default rule allows concluding that a condor flies because the precondition of the default <math>Bird(Condor)</math> is true and its justification <math>Flies(Condor)</math> is not inconsistent with what is currently known.
The default rule allows concluding that a condor flies because the precondition of the default <math>Bird(Condor)</math> is true and its justification <math>Flies(Condor)</math> is not inconsistent with what is currently known.

On the contrary, <math>Bird(Penguin)</math> does not allow concluding <math>Flies(Penguin)</math>. Indeed, even if the precondition of the default <math>Bird(Penguin)</math> is true, the default rule cannot be applied because its justification <math>Flies(Penguin)</math> is inconsistent with what is known.
On the contrary, <math>Bird(Penguin)</math> does not allow concluding <math>Flies(Penguin)</math>. Indeed, even if the precondition of the default <math>Bird(Penguin)</math> is true, the default rule cannot be applied because its justification <math>Flies(Penguin)</math> is inconsistent with what is known.
From this background theory and this default, <math>Bird(Eagle)</math> cannot be concluded because the default rule only allows deriving
<math>Flies(X)</math> from <math>Bird(X)</math>, but not vice versa. Deriving the antecedents from the consequences is a form of explanation of the consequences, and is the aim of [[Abductive reasoning]].


A common default inference is that something that 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 <math>X</math>.
As in standard logic we cannot say anything about whether or not an airplane is a bird because we have no inference rules available to do that, default or otherwise.

The computer language [[Prolog]] uses a sort of default assumption when leading with negatation: if a negative atom cannot be proved to be true, then it is assumed to be false. This assumption is similar to the following default rule:


: <math>D = \left\{ \frac{ : {\neg}X}{{\neg}X} \right\} </math>
: <math>\frac{:{\neg}X}{{\neg}X}</math>


For example, the computer language [[Prolog]] uses a sort of default assumption when leading with negatation: 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 <math>\neg X</math>, it tries to prove that <math>X</math> is true, and conclude that <math>\neg X</math> is true if it fails. In default logic, instead, a default having <math>\neg X</math> as a justification can only be applied if <math>\neg X</math> is consistent with the current knowledge.
Note, however, that [[Prolog]] uses the so-called [[negation as failure]]: when the interpreter has to evaluate the atom <math>\neg X</math>, it tries to prove that <math>X</math> is true, and conclude that <math>\neg X</math> is true if it fails. In default logic, instead, a default having <math>\neg X</math> as a justification can only be applied if <math>\neg X</math> is consistent with the current knowledge.



Revision as of 17:34, 30 July 2005

Default logic is a non-monotonic logic proposed by Ray Reiter to formalize the human reasoning with default assumptions.

In default logic, one 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 humans often do inference using facts that are true only in the majority of cases, but not always. A classical example of a fact that cannot be easily expressed in standard logic is that “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 default rule to be specified. Default logic aims at formalizing inference rules like this one without explicitely mention every exception to them.

Syntax of Default Logic

A default theory is a pair . is a set of logical formulae, called the background theory, that formalize the facts that are known for sure. is a set of default inference rules called default rules, each one of the form:

Such a default rule formalize the fact that, if we know that is true, and each of is consistent with our current knowledge, then is true.

The logical formulae in , and all formulae in a default were originally assumed to be in first-order logic, but 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 first-order default:

This rule means that, if 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:

.

The default rule allows concluding that a condor flies because the precondition of the default is true and its justification is not inconsistent with what is currently known. On the contrary, does not allow concluding . Indeed, even if the precondition of the default is true, the default rule cannot be applied because its justification is inconsistent with what is known. From this background theory and this default, cannot be concluded because the default rule only allows deriving from , but not vice versa. Deriving the antecedents from the consequences is a form of explanation of the consequences, and is the aim of Abductive reasoning.

A common default inference is that something that 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 .

For example, the computer language Prolog uses a sort of default assumption when leading with negatation: 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 , it tries to prove that is true, and conclude that is true if it fails. In default logic, instead, a default having as a justification can only be applied if is consistent with the current knowledge.

Semantics

Semantics of default logic is defined in terms of extensions. Each extension represents the result of applying a number of default rules from the initial background theory until no other default rule can be applied. Default rules may be applied in different order, and this may lead to different extensions. The Nixon diamond example shows an example of 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 is true, and one in which is false.

In general, a default theory may have zero, one, or more extensions. The following is a default theory with no extensions:

Since is consistent with the background theory, the default can be applied, thus leading to the conclusion that is false. This result undermines the assumption that has been made for applying the first default. In default logic, according to the original semantics by Ray Reiter, the above default theory has no extensions.

Several other semantics for default logics have been defined. In some of them, every default theory has at least an extension.

Restrictions

A default with no prerequisite is called categorical. A default with a single justification that is equivalent to the conclusion is called normal. If every justification entails the conclusion the default is called semi-normal.

A default theory in which all defaults are normal is guaranteed to have at least one extensions. Furthermore, different extensions of the same default theory are mutually inconsistent, i.e., two extensions of the same normal theory are inconsistent with each other.

References