The Complexity of Nested Counterfactuals and Iterated Knowledge Base Revisions

1 Introduction

A counterfactual is a conditional statement "if p, then q," where the premise pis either known or expected to be false [Ginsberg, 1986], e.g. "If the electricity hadn't fai­ led, dinner would have been ready on time". This is cu­ stomarily written as 'p > q' to distinguish it from mate­ rial implication 'p =:} q', which is trivially true if pis false in the current context. The evaluation of a counterfac­ tual in a certain context, which is described by a know­ ledge base, can be done using the Ramsey Test, which roughly states that p > q is true if the minimal change to accept p requires accepting q. Counterfactual reasoning is nonmonotonic in the sense that by augmenting the knowledge base a previously valid counterfactual may become false . The relevance of counterfactual reasoning to a number of AI applications was first demonstrated in [Ginsberg, 1986], to which (and to [Gardenfors, 1988; Nebel, 1991; Grahne, 1991]) the reader is referred for a background.

In this paper we mainly deal with nested counterfac­ tuals, i.e., counterfactuals where the conclusion can be a counterfactual itself instead of a plain propositional Our study also includes allowing negation in nesting counterfactuals, i.e. statements like p > ...,( q > r ). This is motivated by natural relevance.

·This is a short version containing only proof sketches. An extended report containing full proofs and more results is in preparation.

Example 2: Imagine a two person game and that player one wants to know whether every possible choice for his next move ( ml) does not result in a forced win for player two, i.e. player two does not win regardless of his next move (...,(m2 > w2)). This question amounts to m1 > ...,(m2 > w2). 0

The alternative to nesting counterfactuals into the consequence is nesting into the premise, i.e. a nesting (p > q) > r. Intuitively, (p > q) > r means "Would r be true in the closest context where p > q is true" . Note this is different from "if p > q, then r", which is true if p > q is false . Nestings (p > q) > r are relevant to practice, as the following example shows.

Example 3: Imagine a system is error detecting if the occurrence of an error (e) is displayed (d) on some special device. The question whether a module m must occur in the system if its current state is changed to be error detecting amounts to (e >d) > m. 0

The complexity of evaluating a single counterfactual in the propositional case was studied in [Nebel, 1991 ; Eiter and Gottlob, 1992], where it was shown that this problem is Ilf -complete. In the present paper we study the complexity of checking nested counterfactuals over propositional knowledge bases. Our main results are summarized as follows. First, we show that deciding nested counterfactuals of the form Pl > (P2 > · · · (Pn > q) · · ·) is Ilf -complete. This is rather surprising and can be viewed as a positive result. It has an interesting conse­ quence for the two basic approaches to cope with iterated KB-revisions. The first incorporates each revision into the KB and needs in general exponential space and time, while the second stores the initial KB and the syntactic sequence [p1, P2 1 ··· , Pn) of revisions separately and ac­ counts for it in query answering. Our result guarantees that the second approach does not get substantially (i.e. exponentially) harder when the sequence of revisions in­ creases, which strongly favors this approach. Second, we show that things get more complicated (PSP ACE­ complete) if negated counterfactuals can appear in ne­ stings (see Example 2). Third, we consider nested coun­ terfactuals of type (p > q) > r, i.e. the nesting occurs in the premise, and show that checking validity of such formulas is Ilf -complete.

The rest of this paper is organized as follows . Sec­ tion 2 introduces concepts and reviews previous results. In Sections 3 and 4 investigate into the complexity of evaluating counterfactuals nested in the conclusion wi­ thout and with negation, respectively, while Section 5 deals with nesting in the premise. Section 6 gives some conclusions. Due to space limitations, we provide here for some results merely detailed proof sketches.

2 Definitions and previous results

We assume that the reader knows about the basic con­ cepts of NP-completeness, the polynomial hierarchy, and PSPACE, rf. [Garey and Johnson, 1979]. Briefly, PSP ACE is the class of problems decidable in polynomial space, and the classes Llf, I::f, and II f of the polynomial hierarchy are defined as follows: Ll~ = I:~ = II~ = P and for k ~ 0, Llf+1 = pEf, Ef+1 = NPEf, IIf+1 = col:f+l . In particular, Llf = P, I::f = NP, and IIf = coNP. Clearly I::f ~ I::f U IIf ~ Llf+1 ~ Ef+1, but for k ~ 1 any equality is considered very unlikely similar as P = NP . The canonical PSPACE-complete problem is deciding the validity of a quantified Boolean formula (QBF) <II = Q1a1Q2a2 · · · QnanE, where each quantifier Q; E {3, 'v'} ranges over {true ,false} and E is a Boolean formula built on variables a1, .. . , an . Denote by QBFk,3 (resp. QBFk,v) the valid QBFs <II with j quan­ tifier alternations and Q1 = 3 (Q1 = 'v'), where <II has a "quantifier alternation" for Q1 and every i > 1 with Q; f Qi-1· Deciding if <II E QBFk ,3 (resp. <II E QBFk,v) is complete for Ef (IIf).

Let C be the language of propositional logic over some set of atoms. "T" and "..L" are constants for truth and falsity, respectively. We assume the usual convention on the binding of the logical connectives . A knowledge base is a finite subset of C. Knowledge bases are denoted by letters S, T, . . . , formulas from C by p, q, .. . , and atoms by a, b etc. A literal is an atom or the negation of an atom.

p > q denotes the counterfactual "If p, then q" . The formal semantics of p > q is as follows . Let

Then, p > q has value true over knowledge base S (in symbols, S F p > q) if for every T E F(p, S), T F q, and value false otherwise (S ~ p > q) .

F(p, S) had been earlier proposed as an operator for updating logical databases in [Fagin et a/., 1983], where the databases in F(p, S) are considered to be indepen­ dent possible outcomes of an update by p.

As shown in [Nebel, 1991; Eiter and Gottlob, 1992], evaluating a counterfactual is most likely much harder than any NP-complete problem.

Proposition 2.1 [Nebel, 1991; Eiter and Gottlob, 1992] Deciding whether S F p > q is IIf -complete.

The nested counterfactuals are the smallest formula set C that contains all counterfactuals p > q and satisfies the following properties:

1. if c E C and p E £,then p > c E C.
2. ifc E C, then ...,c E C.

We also write p 'j c for ...,(p > c) . The unique sequence s1,s2, ... ,sn = c such that s1 = p > q and s;, 2 ~ i ~ n, results from s;_1 by (1) or (2) is referred to as the structural sequence of c. Each s; is said to occur in c.

Example 4: The structural sequence of Pl > (P2 'j q) is P2 > q, P2 'j q, P 1 > (P2 'j q). 0

We now give a precise semantics to nested counterfac­ tuals. The truth value of a (possibly nested) c E Cover a knowledge-base S is recursively defined as follows . c has value true overS (in symbols, S F c)

• if c = p > c', c' E C, and T f= c', for every T E :F(p,S) .
• if c = -.c', c' E C, and c' has value false over S.

and has value false otherwise (S ~c) .

The knowledge bases that are relevant for s; from the structural sequence s1, s2, .. . , Sn of c are determined by S and the premises of Si+1, ... , Sn . We refer to these knowledge bases as the context of s;, which is formally defined as follows:

The following proposition is immediate from the defini­ tion.

Proposition 2.2 Let c = p > c', c' E C. Then, S f= c iff S' f= c' for every S' E Cn( c', c, S).

3 Right-nested counterfactuals

We start with the evaluation of nested counterfactuals where no negation occurs in the nesting. In the spi­ rit of [Rabin and Scott, 1959] (cf. also [Vardi, 1989; Kautz and Selman, 1991]), we describe a nondetermini­ stic algorithm for proving S ~ P1 > (P2 > · · · (Pn > q) · · ·):

NO-ALGORITHM RNCF(S,p1, ... ,pn, q) input: finite S ~ C, formulas PI, ... , Pn, q E C output: "no" iff S lot= P1 > (p2 > · · · (Pn > q) · · ·) begin WI :=S; Guess W2, ... , Wn+! ~ S U {PI , ... ,pn} such that W; ~ Wi-1 U {Pi-d and Pi-! E W;, for 2 ~ i ~ n + 1; for i = 2 to n + 1 do begin if (W; I= 1.) then stop; for each r E (Wi-1 - W;) do if (W; U { r} lot= 1.) then stop; end; if (Wn+l lot= q) then output "no"; end.

Proposition 3.1 RNCF(S,p1, ... ,pn,q) outputs "no" iff S ~ P 1 > (P2 > · · · (Pn > q) · · ·) ·

Proof. (Sketch) Let c1, ... , Cn be the structural se­ quence of c = P1 > (P2 > · · · (Pn > q) · · ·). Notice that c1 = Pn > q and c; = Pn-i+1 > Ci-1> 2::; i::; n.

One can show by induction on n that S f= c iff there exist W E Cn( c1, c, S) and W' E :F(Pn, W) such that W' ~ q. It follows from the definition of Cn that W is in the context of C1 iff there exist w1, w2, ... , Wn = w such that W; E Cn(cn-i+1· c, S), i.e Wi+1 E :F(p;, W;) fori< n. Now consider RNCF. It can be easily shown that the computation does not stop in the for-loop iff Wn+l E :F(pn, Wn), where Wn E Cn(c1, c, S). Thus RNCF correctly outputs "no". Conversely, RNCF out­ puts "no" in some computation if S ~ c. 0

Corollary 3.2 Given a knowledge base S and c = P1 > (P2 > · · · (Pn > q) · · ·), deciding if Sf= c is in Ilf.

From Proposition 2.1, we thus obtain the following. Theorem 3.3 Given a knowledge base S and c = P1 >

(P2 > · · · (Pn > q) · · ·) 1 deciding if S F= c is Ilf -complete.

This result applies to knowledge bases that may con­ tain arbitrary propositional formulas. In practice, know­ ledge bases are often sets of Horn clauses, i.e. disjunc­ tions of literals of which at most one is an atom. It is well-known that deciding S f= p is polynomial if p and every q E S are Horn clauses.

Theorem 3.4 Let S be a knowledge base and c = p1 > (P2 > · · · (Pn > q) · · ·) 1 where q and all Pi as well as all p E S are Horn clauses. Deciding if S f= c is coNP­ complete.

Proof. If pis a Horn clause, then every T E :F(p, S) is a set of Horn clauses. It follows that each classical infe­ rence test in RNCF can be done in polynomial time, and hence RN CF can be reformulated as an NP-algorithm. Consequently, deciding if S f= c is in coNP. Hardness for coNP follows for c = P1 > q from [Eiter and Gottlob, 1992, Theorem 8.5], even if p1 and q are literals. 0

We remark that [Fagin eta/., 1983] and [Nebel, 1991] consider a refinement of. the operator :F(p, S) by the in­ troduction of priorities. This does not only not increase the complexity (deciding s F= p > q is still in rrf)' but makes complexity decrease when Sis totally ordered (the problem is easily shown to be in ~f). Theorems 3.3 and 3.4 remain valid for the obvious generalization of priorities to nested counterfactuals. Moreover, if S is to­ tally ordered and all formulas are Horn, we obtain the optimistic result that evaluating a nested counterfactual over S is polynomial.

4 Right-nested counterfactuals with negation

We consider now evaluation of counterfactuals with ne­ gation in the nesting. It appears that negation has a dra­ stic effect on the complexity of evaluating nested coun­ terfactuals. Negating each counterfactual occurring in PI> (P2 > · · · (Pk > q) · · ·) leads to Ef+l-hardness if k is a constant and to PSPACE-hardness if k is not bounded. We show this in the sequel by a transformation of QBFs into nested counterfactuals. Let

41> = (Q1.!!.1)(Q2.!!.2) · · · (Qk+l.!!.k+I)E(.!!.1, · · · ,.!!.j), where Q1 = q1, Q; f. Qi-1, for i > 1 and where.!!.;

a;,1, ... , a;,n, is a group of n; ~ 1 variables and (Qi.!!.;) stands for Qiai,1 · · · Qiai,n;, 1 ::; i ::; k + 1.

Let c be a new variable, and let !!1 1 ··· , ~ be groups of new variables, where!!; = bi,, ... , bi,. . . Then, I

• Pi = ~ ¢. !!;], for 1 ::; i < k, where.!!.; ¢.!!; is short for 1\i=l ai,i ¢. b;,i.
• Pk = p(41>), and p(41>) is, depending on Qk+1· the following formula:

· q =-,c.

Define a knowledge base S(cf>) and a counterfactual c( 4>) = Ck ( 4>) as follows:

Note that for every 4>, S(cf>) and c(cf>) can be computed in polynomial time.

Intuitively, the c; ( 4>) 's represent the (possibly nega­ ted) subformulas of 4> on the quantified variable groups l!k-i+1, . . .· ~+1 where all remaining variables (i.e, those in g_1, ... , .!!k-i) are replaced in E with T or .l according to a truth value assignment . Every such assignment is encoded by a context knowledge base C of c;(cf>). The value of variable a; ,j is true if it occurs literally in C and otherwise false (in this case, b;,i is in C.) Testing if C F c;(cf>) implements a test if 4> is valid (or not) for the encoded truth assignment and quantification of l!k-i+1, . .. , .G.k+l with Qk-i+1, . .. , Qk+1 · Thus checking S I= ck(cf>), i.e. S F c(cf>), implements a test if the for­ mula 4> is valid.

Example 5 : Consider 4> = Vaaa2,13a2,2Va3 E,

4> is rewritten as (Vg1)(3g2)(V.!!J)E, where fh = a1, .!!2 = a2,1, a2,2, and .!!3 = a3. Applying the transformation (k + 1 = 3, Q1 = V) we get

q = -,c,

Verify that 4> is valid and that SF c(cf>). 0

Theorem 4.1 S(cf>) F c(cf>) if and only if4> is valid.

Before sketching a proof of this theorem, we note some useful lemmata.

Lemma 4.2 Fork+ 1 = 2 and Q1 = V, S(cf>) F c(<I>) iff 4> E QBF2,V.

Proof. (Sketch) Immediate from the proof of [Eiter and Gottlob, 1992, Lemma 6.2]. 0

Lemma 4.3 Let S and S' be knowledge bases such that S' ~ .l and no atom occurring in any p E S' occurs in any q E S or in c . Then, S F c iff S U S' F c, and for

each s; from the structural sequence s1 , .. . , Sk of c,

Proof. (Sketch) Can be shown by induction on k. 0

Lemma 4.4 LetS be a knowledge base and let s1, . .. , Sk be the structural sequence of c , and denote by c[c'] the counterfactual obtained if s 1 is replaced in c by the coun­ terfactual c'. If for all T E Cn(s1, c, S) it holds that T F s1 iffT F c', then SF c iff SF c[c'].

Proof. (Sketch) By induction on k (use Proposition 2.2) . 0

Proof sketch of Theorem 4.1 Proof by induction on the number k+1 of quantifier alternations of 4> .

(Basis) k + 1 = 2: By Lemma 4.2, it remains to consider 4> = (3g1)(Vg2)E. Since 4> = -,F' for 4>' = (Vg_1)(3g_2)-,£, 4> is valid iff S(cf>') ~ c(cf>'), which can be shown to be equivalent to S(cf>) F c(cf>).

(Induction). Consider k + 2, i.e. 4> = (Ql.!h) · · · ( QH2.!!H2)E has k + 2 quantifier alternations . There are two cases for Q1:

1. Q1 = V: In this case, 4> is valid iff for every truth assignment <P to g1, the formula <I>~ = (3g2) · · · (Qn+1.!!n+ 1 )E~ is valid, where E~ is obtained from 4> by replacing in E each occurrence of a1, by T if <P(a1.) = true and by .l otherwise, for all i . Applying the hypo­ thesis fork+ 1, <I>~ is valid iff SF c, where S = S(<I>~) and c = c(cf>~). Define

and let s1 = p(cf>~) > q be the first counterfactual in the structural sequence of c . It can be shown using Lemma 4.3 that s F c iff sus~ F c and that

It can be further shown that for every T E Cn(s1, c, S U S~), T F s1 iff T F p' > q. It follows from Lemma 4.4 that sus~ t= c (i .e., s t= c) iff sus~ t= c[p' > q] . Consequently, s F c iff S(cf>) us~ F c(p' > q]. Now observe that p' = p(cf>) and c[p' > q] = ck(cf>) . It follows that <I> is valid iff S(cf>) us~ F Ck(cf>) for every</!. Since ck+1(4>) = c(cf>) and

Proposition 2.2 implies that 4> is valid iff S(cf>) F c(cf>) .

2. Q1 = 3: Since <I> = -,cf>' for 4>' = (Vg1)(3g2) · · · (Q~+ 2 gk+2)-,£, using case 1.) it is not hard to show that the statement holds for k + 2. 0

We obtain the main results of this section.

Theorem 4.5 Let S be a knowledge base and c = P1 f (P2 f · · · (Pk f q) · · ·), for constant k ~ 1. Deciding if S F c is Ef+l-complete.

Proof. (Sketch) Membership in Ef.i-1 can be shown by induction on k. Fork= 1, this holds by Proposition 2.1; for k > 1, by the hypothesis a guess for W E :F(p1 , S) with W ~ p2 f (- · · (Pk f q) · · ·) can be verified in po­ lynomial time with a Ef oracle. Ef+1-hardness follows from Theorem 4.1. 0

Theorem 4.6 Given a knowledge base S and c E C, deciding if S f= c is PSPACE-complete. Hardness for PSPACE holds if c has form P1 "j> (P2 "f>· · · (Pn "f>q) · · ·).

Proof. It is straightforward to design a procedure for deciding Sf= c in polynomial space. PSPACE-hardness follows from Theorem 4.1. 0

Since evaluating nested counterfactuals is in PSPACE, it is straightforward that evaluating a formula built using the standard propositional connectives from propositio­ nal atoms and nested counterfactuals over a knowledge base is in PSPACE, too.

5 Left-nested counterfactuals

We consider in this section evaluation of counterfactuals nested in the premise, i.e. (p > q) > r. A formal seman­ tics for (p > q) > r using the "possible worlds approach" can be defined as follows. Define

Note that T f= p > q for every T E :F(p > q, S). Now define that (p > q) > r has overS value true (in symbols, S f= (p > q) > r) if T f= r for every T E :F(p > q, S) and has value false otherwise (S ~ (p > q) > r).

This definition can be extended to iterated nestings in the premise. Such statements are conceptually quite involved, however, and their relevance seems questiona­ ble; we do not know of an intuitive example. Future work will investigate into a semantics, though, which fo­ resees besides removal also addition of formulas to reach from the relevant knowledge base a "possible world" of a repeatedly left-nested counterfactual.

Consider the following nondeterministic algorithm, where CF(p, q, S) = true iff S f= p > q:

NO-ALGORITHM LNCF(S,p, q, r) input: finite S s; £, formulas p, q, r E £ output: "no" iff S ~ (p > q) > r begin Guess S' ~ S; if -.CF(S',p, q) or (S' I= r) then stop else for each T, S' C T s; S do if CF(T,p,q) then stop; output "no"; end.

Proposition 5.1 S ~ (p > q) > r iff LNCF outputs "no".

LNCF has exponential worst case runtime even mo­ dulo the CF calls and S' f= r. An improvement to po­ lynomial runtime seems hard to achieve. In particular, the exponential candidate space for T in the for-loop, which tests whether S' is closest to S such that p > q holds, can most likely not be reduced efficiently to a small subset (cf. Lemma 5.3). This may be explained by nonmonotony of counterfactuals.

It is easily seen that a proof for S' '1. :F(p > q, S) can be given nondeterministically in polynomial time with an oracle for classical and counterfactual inference. As a Ilf oracle is suitable for that, deciding if S' '1. :F(p > q, S) is in Ef. Clearly, a proof for S ~ (p > q) > r can be given nondeterministically in polynomial time with an oracle for S' '1. :F(p > q) and classical inference. Thus,

Theorem 5.2 Given S and (p > q) > r, deciding if S F= (p > q) > r is in II f.

Lemma 5.3 Let S' f= p > q for a S' ~ S. Given S' and p > q, deciding whether T f= p > q for any T, S' C T ~ S, is Ef -hard.

Proof. (Sketch) We transform deciding the validity of ~ = (3fh)(\ff!.2)(3Qa)E into this problem, where Q; = a;,l, ... ,a;,n,, i = 1,2,3. Let c be a new atom and It / I I 11_11 II d' e fh = al,l' · · · 'al,n1 ' !h - al,l' · · · 'al,n1 ' an !!.2 a~ , l, ... , a~,n, be groups of new atoms. Define

Notice that S', S, p and q are constructible in polyno­ mial time. It is not hard to see that S' f= p > q. Mo­ reover, it can be shown that there exists T, S' C T ~ S, such that T f= p > q iff ~ is valid. 0

Theorem 5.4 Deciding if S f= (p > q) > r from S and (p > q) > r is rrr -hard.

Proof. (Sketch) The proof is an extension of the trans­ formation in the proof of Lemma 5.3. Let

where S1 (resp. Pl, qi) is constructed asS (resp. p,q) in the proof of Lemma 5.3. It can be shown that Sf= (p > q) > r iff~ is valid. 0

Corollary 5.5 Deciding if Sf= (p > q) > r from S and (p > q) > r is rrr -complete.

6 Related work and conclusion

Complexity characterizations of evaluating counterfac­ tuals are given in [Winslett, 1990; Nebel, 1991; Grahne, 1991; Grahne and Mendelzon, 1991] . Grahne and Men­ delzon [Grahne and Mendelzon, 1991] considered sub­ junctive queries in a different framework, where the knowledge base is given by a set of models and updates are performed according to Winslett's method lWins­ lett, 1988] . In particular, [Grahne and Mendelzon, 1991, Corollary 4.2] implies that evaluating nested counterfac­ tuals under this update semantics is PSPACE-complete.

Our work contributes to the recent effort in giving a precise complexity characterization of nonmonotonic re­ asoning in the full propositional context, cf. [Niemela, 1991; Winslett, 1990; Nebel, 1991; Rutenburg, 1991; Eiter and Gottlob, 1992; Stillman, 1992] (see [Cadoli and Schaer£, 1992] for an overview), extending previ­ ous results for restricted contexts, e.g. [Kautz and Sel­ man, 1991; Stillman, 1990; Selman and Levesque, 1990; Cadoli and Lenzerini, 1990; Provan, 1990] . Such a cha­ racterization supports a better understanding of the computational relationships between various forms of nonmonotonic reasoning, e.g. efficient intertranslatabi­ lity. Furthermore, the precise complexity of a problem gives us a clue of its computational difficulty and may provide insight to sources of complexity. For counter­ factuals, these sources are classical inference (~ F= p) and the many knowledge bases that are possible af­ ter incorporating a change. Fortunately, a sequence of changes is not a source of complexity. Since IIf­ complete problems are most likely much harder than NP-complete problems, our results suggest that methods such as GSAT [Selman et al., 1992] for efficient handling of NP-complete problems are most likely not applicable to nested counterfactuals. However, GSAT can be fruit­ fully applied for proving S ~ PI > (P2 > · · · (Pn > q) · · ·) if all propositional formulas are Horn clauses.

Acknowledgments

The authors would like to thank two referees for their valuable comments.