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.
The model semantics of this formalism is defined as:
The results on model compactness have been shown by Liberatore and Schaerf . Here we recall them.
The results on theorem compactness are quite simple and we provide here the proofs.
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).
Proof. Membership follows from the complexity results of Eiter and Gottlob , 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.