A logic for default reasoning

Inside the paper

The problem

Ordinary deduction does not easily express everyday assumptions that hold unless an exception is known. For instance, knowing that an individual is a bird does not prove that it is not among the exceptions to flight.

The idea

Reiter gives default rules a formal interpretation in which a conclusion can depend on the consistency of an assumption with a set of beliefs. The resulting extensions represent possible sets of conclusions supported by the facts and defaults.

How it works

• A default rule specifies a prerequisite, one or more assumptions that must remain consistent, and a conclusion.
• A default theory combines ordinary facts with a set of such rules, including rules that represent typical cases or closed-world assumptions.
• An extension is defined by a fixed-point construction: its conclusions are generated using defaults whose justifications are consistent with that same extension.
• New information can change which defaults apply, and different extensions can represent alternative sets of conclusions.

What it showed

The paper develops the semantics and proof theory of default logic and studies properties of classes of default theories. Its examples include ordinary exceptions, database assumptions and the persistence of facts through changes in the world.

Read it for

Start with the examples in Section 1.1, especially the bird example, before reading the definition of an extension in Section 2. The later theorems and proof procedures reward a second pass; follow the examples first if the notation is unfamiliar.

Written in our own words from the paper itself. A draft the editors have not yet reviewed.