** 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*