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 $K$ be a set of propositional formulae, representing an agent's knowledge about the world. When a new formula $A$ is added to $K$, the problem of the possible inconsistency between $K$ and $A$ arises. The first step is to define the set of sets of formulae $W(K,A)$ in the following way:

$$\begin{array}{ll} W(K,A) = \{ K' & \multicolumn{1}{\vert l}{... ...bset }} \mbox{of $K \cup \{A\}$\ containing $A$} \} \end{array}$$

Any set of formulae $K' \in W(K,A)$ is a maximal choice of formulae in $K$ that are consistent with $A$ and, therefore, we may retain when incorporating $A$. 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: $K * A \doteq \{K' \mid K'\in W(K,A)\}$. Inference in the revised theory is defined as inference in each of the theories:

$$\begin{array}{rcl} K*A \vdash_{SBR} Q & \mbox{iff} & \mbox{ ... ...' \in W(K,A)$\ }, \mbox{ we have that } K' \vdash Q \end{array}$$

The model semantics is defined as:

$$\begin{array}{rcl} M \models_{SBR} K*A & \mbox{iff} & \mbox{... ... $K' \in W(K,A)$\ } \mbox{ such that } M \models K' \end{array}$$

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 $K$ that belong to all sets of $W(K,A)$. Thus, inference is defined as:

$$\begin{array}{rcl} K*A \vdash_{WIDTIO} Q & \mbox{iff} & \bigcap W(K,A) \vdash Q \end{array}$$

The model semantics of this formalism is defined as:

$$M \models_{WIDTIO} K*A \mbox{ ~~ iff ~~ } M \models \bigcap W(K,A)$$

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 $\parallel\!\leadsto$ P, thus WIDTIO is in model-P.

Theorem 17   [39, Theorem 5] The problem of model checking for Skeptical Belief Revision is $\parallel\!\leadsto$ 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 $\parallel\!\leadsto$ 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 $K*A$ into a propositional formula by computing the set $W(K,A)$ and then constructing their intersection. By construction their intersection has size less than or equal to the size of $K \cup A$. As a consequence, after preprocessing, deciding whether a formula $Q$ follows from $K*A$ 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 $\parallel\!\leadsto$$\Pi^p_{2}$-complete, thus Skeptical Belief Revision is thm-$\Pi^p_{2}$-complete.

Proof. Membership follows from the complexity results of Eiter and Gottlob [13], where they show that deciding whether $K*A \vdash_{SBR} Q$ is a $\Pi^p_2$-complete problem. Hardness follows easily from Theorem 17. In fact, $M \models_{SBR} K*A$ iff $K*A \not\vdash_{SBR} \neg form(M)$, where $form(M)$ is the formula that represents the model $M$. As a consequence, model checking can be reduced to the complement of inference. Thus inference is $\parallel\!\leadsto$$\Pi^p_{2}$-complete.