Next: Discussion Up: Applications Previous: Default Logic

Belief Revision

Many formalisms for belief revision have been proposed in the literature, here we focus on two of them: WIDTIO (When In Doubt Throw it Out) and SBR (Skeptical Belief Revision). Let be a set of propositional formulae, representing an agent's knowledge about the world. When a new formula is added to , the problem of the possible inconsistency between and arises. The first step is to define the set of sets of formulae in the following way:

Any set of formulae is a maximal choice of formulae in that are consistent with and, therefore, we may retain when incorporating . The definition of this set leads to two different revision operators: SBR and WIDTIO.

SBR
Skeptical Belief Revision [16,20]. The revised theory is defined as a set of theories: . Inference in the revised theory is defined as inference in each of the theories:

The model semantics is defined as:

WIDTIO
When In Doubt Throw It Out [51]. A simpler (but somewhat drastical) approach is the so-called WIDTIO, where we retain only the formulae of that belong to all sets of . Thus, inference is defined as:

The model semantics of this formalism is defined as:

The results on model compactness have been shown by Liberatore and Schaerf [39]. Here we recall them.

Theorem 16   [39, Theorem 11] The problem of model checking for WIDTIO is in P, thus WIDTIO is in model-P.

Theorem 17   [39, Theorem 5] The problem of model checking for Skeptical Belief Revision is coNP-complete, thus Skeptical Belief Revision is model-coNP-complete.

The results on theorem compactness are quite simple and we provide here the proofs.

Theorem 18   The problem of inference for WIDTIO is coNP-complete, thus WIDTIO is thm-coNP-complete.

Proof. Membership in the class thm-coNP immediately follows from the definition. In fact, we can rewrite into a propositional formula by computing the set and then constructing their intersection. By construction their intersection has size less than or equal to the size of . As a consequence, after preprocessing, deciding whether a formula follows from is a problem in coNP. Hardness follows from the obvious fact that PL can be reduced to WIDTIO and PL is thm-coNP-complete (see Theorem 3).

Theorem 19   The problem of inference for Skeptical Belief Revision is -complete, thus Skeptical Belief Revision is thm--complete.

Proof. Membership follows from the complexity results of Eiter and Gottlob [13], where they show that deciding whether is a -complete problem. Hardness follows easily from Theorem 17. In fact, iff , where is the formula that represents the model . As a consequence, model checking can be reduced to the complement of inference. Thus inference is -complete.

Next: Discussion Up: Applications Previous: Default Logic
Paolo Liberatore
2000-07-28