In: Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence (IJCAI-93), R. Bajcsy ed, Morgan Kaufman, 1993, pp. 526–531.

The Complexity of Nested Counterfactuals and Iterated Knowledge Base Revisions^{∗}

Thomas Eiter and Georg Gottlob

Christian Doppler Laboratory for Expert Systems

Technical University of Vienna Paniglgasse 16, A-1040 Wien, Austria

(eiter|gottlob)@vexpert.dbai.tuwien.ac.at

Abstract

We consider the computational complexity of evaluating nested counterfactuals over a propositional knowledge base. Counterfactual implication p > q models a statement “if p, then q,” where p is known or expected to be false, and is different from material implication p ⇒ q. A nested counterfactual is a counterfactual statement where the conclusion q is a (possibly negated) counterfactual. Statements of the form p_{1} > (p_{2} > ⋯ (p_{n} > q) ⋯) intuitively correspond to hypothetical queries involving a sequence of revisions. We show that evaluating such statements is Π_{2}^{P} -complete, and that this task becomes PSPACE-complete if negation is allowed in the nesting. We also consider nesting a counterfactual in the premise, i.e. (p > q) > r and show that evaluating such statements is most likely much harder than evaluating p > (q > r).

1 Introduction

A counterfactual is a conditional statement “if p, then q,” where the premise p is either known or expected to be false [Ginsberg, 1986], e.g. “If the electricity hadn’t failed, dinner would have been ready on time”. This is customarily written as ‘p > q’ to distinguish it from material implication ‘p ⇒ q’, which is trivially true if p is false in the current context. The evaluation of a counterfactual in a certain context, which is described by a knowledge 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 [Gärdenfors, 1988; Nebel, 1991; Grahne, 1991]) the reader is referred for a background.

In this paper we mainly deal with nested counterfactuals, i.e., counterfactuals where the conclusion can be a counterfactual itself instead of a plain propositional sentence. Nested counterfactuals are often used in reallife contexts and are an important principle of commonsense reasoning.

Example 1: The statement “If you would have bought a painting by Botticelli from John and you would notice it is a fake, you would still remain a client of John” corresponds to a nesting of counterfactuals of the form

buy botticelli from john > (fake > client of john).

The value of this counterfactual depends, of course, on the given knowledge base. It is intuitively clear that the counterfactual will evaluate to false on a large number of reasonable knowledge bases. According to Ramsey’s rule, the evaluation of this nested counterfactual over a given knowledge base T amounts to check whether

(T ∘ buy botticelli from john) ∘ fake) ⊧ client of john

for a suitable revision operator “∘”. This example also shows that nesting a counterfactual in the conclusion is different from strengthening the premise, i.e., (p > (q > r)) is different from p∧q > r. Indeed, the conjunction of buy botticelli from john and fake, is semantically inconsistent (because a Botticelli is not a fake), and therefore the sentence would be vacuously true for each knowledge base. □

More generally, a nested counterfactual of the form p_{1} > (p_{2} > … (… > (p_{n} > q)) …) is true over a knowledge base T iff T ∘ p_{1} ∘ p_{2} … ∘ p_{n} ⊧ q, i.e., iff T revised by p_{1}, revised by p_{2}, revised by p_{3} etc. implies q. For this reason, the complexity results we will derive for nested counterfactuals are equally relevant to the problem of inferencing after iterated knowledge base revisions.

The complexity of evaluating unnested counterfactuals over propositional knowledge bases, i.e. finite propositional theories, was considered in [Nebel, 1991; Grahne, 1991; Eiter and Gottlob, 1992]. In this paper, we deal with evaluating nested counterfactuals based on Ginsberg’s approach [Ginsberg, 1986] which uses the method by Fagin, Ullman and Vardi [Fagin et al., 1983] for incorporating changes to a knowledge base. Such statements intuitively correspond to hypothetical queries involving a sequence of revisions, and are naturally relevant to planning and reasoning about actions (cf. [Ginsberg and Smith, 1988; Winslett, 1988]), for instance.

∗This is a short version containing only proof sketches.

An extended report containing full proofs and more results is in preparation.

Our study also includes allowing negation in nesting counterfactuals, i.e. statements like p > ¬(q > r). This is motivated by natural relevance.

Example 2: Imagine a two person game and that player one wants to know whether every possible choice for his next move (m_{1}) does not result in a forced win for player two, i.e. player two does not win regardless of his next move (¬(m_{2} > w_{2})). This question amounts to m_{1} > ¬(m_{2} > w_{2}). □

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. □

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 Π_{2}^{P} -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 p_{1} > (p_{2} > ⋯ (p_{n} > q) ⋯) is Π_{2}^{P} -complete. This is rather surprising and can be viewed as a positive result. It has an interesting consequence 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 [p_{1}, p_{2}, …, p_{n}] of revisions separately and accounts 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 increases, which strongly favors this approach. Second, we show that things get more complicated (PSPACEcomplete) if negated counterfactuals can appear in nestings (see Example 2). Third, we consider nested counterfactuals of type (p > q) > r, i.e. the nesting occurs in the premise, and show that checking validity of such formulas is Π_{4}^{P} -complete.

The rest of this paper is organized as follows. Section 2 introduces concepts and reviews previous results. In Sections 3 and 4 investigate into the complexity of evaluating counterfactuals nested in the conclusion without 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 concepts of NP-completeness, the polynomial hierarchy, and PSPACE, rf. [Garey and Johnson, 1979]. Briefly, PSPACE is the class of problems decidable in polynomial space, and the classes Δ_{k}^{P} , Σ_{k}^{P} , and Π_{k}^{P} of the polynomial hierarchy are defined as follows: Δ_{0}^{P} = Σ_{0}^{P} = Π_{0}^{P} = P and for k ≥ 0, Δ_{k+1}^{P} = P^{Σ_{k}^{P}} , Σ_{k+1}^{P} = NP^{Σ_{k}^{P}} , Π_{k+1}^{P} = coΣ_{k+1}^{P}. In particular, Δ_{1}^{P} = P, Σ_{1}^{P} = NP, and Π_{1}^{P} = coNP. Clearly Σ_{k}^{P} ⊆ Σ_{k}^{P} ∪ Π_{k}^{P} ⊆ Δ_{k+1}^{P} ⊆ Σ_{k+1}^{P}, 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) Φ = Q_{1}a_{1}Q_{2}a_{2} ⋯ Q_{n}a_{n}E, where each quantifier Q_{i} ∈ {∃, ∀} ranges over {true, false} and E is a Boolean formula built on variables a_{1}, …, a_{n}. Denote by QBF_{k,∃} (resp. QBF_{k,∀}) the valid QBFs Φ with j quantifier alternations and Q_{1} = ∃ (Q_{1} = ∀), where Φ has a “quantifier alternation” for Q_{1} and every i > 1 with Q_{i} ≠ Q_{i−1}. Deciding if Φ ∈ QBF_{k,∃} (resp. Φ ∈ QBF_{k,∀}) is complete for Σ_{k}^{P} (Π_{k}^{P}).

Let L be the language of propositional logic over some set of atoms. “⊤” and “⊥” 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 L. Knowledge bases are denoted by letters S, T, …, formulas from L 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 W (p, S) = {T ⊆ S : T |̸= ¬p, T ⊂ U ⊆ S ⇒ U ⊧ ¬p} be the “possible worlds for p” [Ginsberg, 1986], and let F(p, S) = {T ∪ {p} : T ∈ W (p, T)}. Then, p > q has value true over knowledge base S (in symbols, S ⊧ p > q) if for every T ∈ F(p, S), T ⊧ 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 al., 1983], where the databases in F(p, S) are considered to be independent 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 ⊧ p > q is Π_{2}^{P} -complete.

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

(1) if c ∈ C and p ∈ L, then p > c ∈ C.

(2) if c ∈ C, then ¬c ∈ C.

We also write p ≯ c for ¬(p > c). The unique sequence s_{1}, s_{2}, …, s_{n} = c such that s_{1} = p > q and s_{i}, 2 ≤ i ≤ n, results from s_{i−1} by (1) or (2) is referred to as the structural sequence of c. Each s_{i} is said to occur in c.

Example 4: The structural sequence of p_{1} > (p_{2} ≯ q) is p_{2} > q, p_{2} ≯ q, p_{1} > (p_{2} ≯ q). □

We now give a precise semantics to nested counterfactuals. The truth value of a (possibly nested) c ∈ C over a knowledge-base S is recursively defined as follows. c has value true over S (in symbols, S ⊧ c)

• if c = p > c′, c′ ∈ C, and T ⊧ c′, for every T ∈ F(p, S).

• if c = ¬c′, c′ ∈ C, and c′ has value false over S. and has value false otherwise (S |̸= c).

The knowledge bases that are relevant for s_{i} from the structural sequence s_{1}, s_{2}, …, s_{n} of c are determined by S and the premises of s_{i+1}, …, s_{n}. We refer to these knowledge bases as the context of s_{i}, which is formally defined as follows:

Cn(s_{n}, c, S) = {S}, and for 2 ≤ i ≤ n,

Cn(s_{i−1}, c, S) = \{ \begin{matrix}⋃_{T ∈Cn(s_{i},c,S)} F(p, T) \\ if s_{i} = p > s_{i−1} \\ Cn(s_{i}, c, S)  if s_{i} = ¬s_{i−1} \end{matrix}

The following proposition is immediate from the definition. Proposition 2.2 Let c = p > c′, c′ ∈ C. Then, S ⊧ c iff S′ ⊧ c′ for every S′ ∈ 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 spirit of [Rabin and Scott, 1959] (cf. also [Vardi, 1989; Kautz and Selman, 1991]), we describe a nondeterministic algorithm for proving S |̸= p_{1} >(p_{2} >⋯ (p_{n} >q) ⋯):

ND-ALGORITHM RNCF(S, p_{1}, …, p_{n}, q)

input: finite S ⊆ L, formulas p_{1}, …, p_{n}, q ∈ L output: “no” iff S |̸= p_{1} >(p_{2} >⋯ (p_{n} >q) ⋯)

begin W_{1} := S; Guess W_{2}, …, W_{n+1} ⊆ S ∪ {p_{1}, …, p_{n}} such that W_{i} ⊆ W_{i−1} ∪ {p_{i−1}} and p_{i−1} ∈ W_{i}, for 2 ≤ i ≤ n + 1; for i = 2 to n + 1 do begin

if (W_{i} ⊧ ⊥) then stop; for each r ∈ (W_{i−1} − W_{i}) do

if (W_{i} ∪ {r} |̸= ⊥) then stop; end; if (W_{n+1} |̸= q) then output “no”; end.

Proposition 3.1 RNCF(S, p_{1}, …, p_{n}, q) outputs “no” iff S |̸= p_{1} >(p_{2} >⋯ (p_{n} >q) ⋯). Proof. (Sketch) Let c_{1}, …, c_{n} be the structural sequence of c = p_{1} > (p_{2} > ⋯ (p_{n} > q) ⋯). Notice that c_{1} = p_{n} > q and c_{i} = p_{n−i+1} > c_{i−1}, 2 ≤ i ≤ n.

One can show by induction on n that S ⊧ c iff there exist W ∈ Cn(c_{1}, c, S) and W′ ∈ F(p_{n}, W) such that W′ |̸= q. It follows from the definition of Cn that W is in the context of c_{1} iff there exist W_{1}, W_{2}, …, W_{n} = W such that W_{i} ∈ Cn(c_{n−i+1}, c, S), i.e W_{i+1} ∈ F(p_{i}, W_{i}) for i < n. Now consider RNCF. It can be easily shown that the computation does not stop in the for-loop iff W_{n+1} ∈ F(p_{n}, W_{n}), where W_{n} ∈ Cn(c_{1}, c, S). Thus RNCF correctly outputs “no”. Conversely, RNCF outputs “no” in some computation if S |̸= c. □

Corollary 3.2 Given a knowledge base S and c = p_{1} > (p_{2} >⋯ (p_{n} >q) ⋯), deciding if S ⊧ c is in Π_{2}^{P}.

From Proposition 2.1, we thus obtain the following. Theorem 3.3 Given a knowledge base S and c = p_{1} > (p_{2} >⋯ (p_{n} >q) ⋯), deciding if S ⊧ c is Π_{2}^{P} -complete.

This result applies to knowledge bases that may contain arbitrary propositional formulas. In practice, knowledge bases are often sets of Horn clauses, i.e. disjunctions of literals of which at most one is an atom. It is well-known that deciding S ⊧ p is polynomial if p and every q ∈ S are Horn clauses. Theorem 3.4 Let S be a knowledge base and c = p_{1} > (p_{2} > ⋯ (p_{n} > q) ⋯), where q and all p_{i} as well as all p ∈ S are Horn clauses. Deciding if S ⊧ c is coNPcomplete. Proof. If p is a Horn clause, then every T ∈ F(p, S) is a set of Horn clauses. It follows that each classical inference test in RNCF can be done in polynomial time, and hence RNCF can be reformulated as an NP-algorithm. Consequently, deciding if S ⊧ c is in coNP. Hardness for coNP follows for c = p_{1} > q from [Eiter and Gottlob, 1992, Theorem 8.5], even if p_{1} and q are literals. □

We remark that [Fagin et al., 1983] and [Nebel, 1991] consider a refinement of the operator F(p, S) by the introduction of priorities. This does not only not increase the complexity (deciding S ⊧ p > q is still in Π_{2}^{P}), but makes complexity decrease when S is totally ordered (the problem is easily shown to be in Δ_{2}^{P}). Theorems 3.3 and 3.4 remain valid for the obvious generalization of priorities to nested counterfactuals. Moreover, if S is totally 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 negation in the nesting. It appears that negation has a drastic effect on the complexity of evaluating nested counterfactuals. Negating each counterfactual occurring in p_{1} >(p_{2} >⋯ (p_{k} >q) ⋯) leads to Σ_{k+1}^{P}-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

Φ = (Q_{1}\underline{a}_{1})(Q_{2}\underline{a}_{2}) ⋯ (Q_{k+1}\underline{a}_{k+1})E(\underline{a}_{1}, …, \underline{a}_{j}), where Q_{1} = q_{1}, Q_{i} ≠ Q_{i−1}, for i > 1 and where \underline{a}_{i} = a_{i,1}, …, a_{i,n_{i}} is a group of n_{i} ≥ 1 variables and (Q_{i}\underline{a}_{i}) stands for Q_{i}a_{i,1} ⋯ Q_{i}a_{i,n_{i}}, 1 ≤ i ≤ k + 1.

Let c be a new variable, and let \underline{b}_{1}, …, \underline{b}_{k} be groups of new variables, where \underline{b}_{i} = b_{i_{1}}, …, b_{i_{n_{i}}}. Then,

• p_{i} = [\underline{a}_{i} ≢ \underline{b}_{i}], for 1 ≤ i < k, where \underline{a}_{i} ≢ \underline{b}_{i} is short for ⋀_{j=1}^{n_{i}} a_{i,j} ≢ b_{i,j}.

• p_{k} = p(Φ), and p(Φ) is, depending on Q_{k+1}, the following formula:

p(Φ) = ⋀_{i=1}^{k}[\underline{a}_{i} ≢ \underline{b}_{i}] ∧ (E(Φ) ∨ c) ∧ (c ⇒ \underline{a}_{k+1}),

where E(Φ) = ¬E if Q_{k+1} = ∀ and E(Φ) = E if Q_{k+1} = ∃, and c ⇒ \underline{a}_{k+1} stands for c ⇒ ⋀_{j} a_{k+1,j}.

• q = ¬c. Define a knowledge base S(Φ) and a counterfactual c(Φ) = c_{k}(Φ) as follows:

S(Φ) = \{\underline{a}_{1}, \underline{b}_{1}, …, \underline{a}_{k}, \underline{b}_{k}, ¬a_{k+1,1}, …, ¬a_{k+1,n_{k+1}}, ¬c\} For k ≥ i > 1,

c_{i}(Φ) = \{ \begin{matrix}p_{k−i} > c_{i−1}(Φ), & if Q_{k−i} = ∀ \\ p_{k−i} ≯ ¬c_{i−1}(Φ), & if Q_{k−i} = ∃ \end{matrix} ,

c_{1}(Φ) = \{ \begin{matrix}p_{k} ≯ q, & if Q_{k+1} = ∀ \\ p_{k} > q, & if Q_{k+1} = ∃ \end{matrix}

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

Intuitively, the c_{i}(Φ)’s represent the (possibly negated) subformulas of Φ on the quantified variable groups \underline{a}_{k−i+1}, …, \underline{a}_{k+1} where all remaining variables (i.e, those in \underline{a}_{1}, …, \underline{a}_{k−i}) are replaced in E with ⊤ or ⊥ according to a truth value assignment. Every such assignment is encoded by a context knowledge base C of c_{i}(Φ). The value of variable a_{i,j} is true if it occurs literally in C and otherwise false (in this case, b_{i,j} is in C.) Testing if C ⊧ c_{i}(Φ) implements a test if Φ is valid (or not) for the encoded truth assignment and quantification of \underline{a}_{k−i+1}, …, \underline{a}_{k+1} with Q_{k−i+1}, …, Q_{k+1}. Thus checking S ⊧ c_{k}(Φ), i.e. S ⊧ c(Φ), implements a test if the formula Φ is valid.

Example 5: Consider Φ = ∀a_{1}∃a_{2,1}∃a_{2,2}∀a_{3} E,

E = (a_{1} ∧ ¬a_{2,1} ⇒ a_{2,2} ∨ a_{3}).

Φ is rewritten as (∀\underline{a}_{1})(∃\underline{a}_{2})(∀\underline{a}_{3})E, where \underline{a}_{1} = a_{1}, \underline{a}_{2} = a_{2,1}, a_{2,2}, and \underline{a}_{3} = a_{3}. Applying the transformation (k + 1 = 3, Q_{1} = ∀) we get

S = {a_{1}, b_{1}, a_{2,1}, a_{2,2}, b_{2,1}, b_{2,2}, ¬a_{3}, ¬c},
p_{1} = a_{1} ≢ b_{1},
p_{2} = [a_{1} ≢ b_{1}] ∧ [a_{2,1} ≢ b_{2,1}] ∧ [a_{2,2} ≢ b_{2,2}] ∧

(¬E ∨ c) ∧ (c ⇒ a_{3}),

q = ¬c,
c_{1}(Φ) = p_{2} ≯ q,  c_{2}(Φ) = p_{1} > (p_{2} ≯ q).

Verify that Φ is valid and that S ⊧ c(Φ). □

Theorem 4.1 S(Φ) ⊧ c(Φ) if and only if Φ is valid.

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

Lemma 4.2 For k + 1 = 2 and Q_{1} = ∀, S(Φ) ⊧ c(Φ) iff Φ ∈ QBF_{2,∀}.

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

Lemma 4.3 Let S and S′ be knowledge bases such that S′ |̸= ⊥ and no atom occurring in any p ∈ S′ occurs in any q ∈ S or in c. Then, S ⊧ c iff S ∪ S′ ⊧ c, and for each s_{i} from the structural sequence s_{1}, …, s_{k} of c,

T ∈ Cn(s_{i}, c, S) ⇔ T ∪ S′ ∈ Cn(s_{i}, c, S ∪ S′).

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

Lemma 4.4 Let S be a knowledge base and let s_{1}, …, s_{k} be the structural sequence of c, and denote by c[c′] the counterfactual obtained if s_{1} is replaced in c by the counterfactual c′. If for all T ∈ Cn(s_{1}, c, S) it holds that T ⊧ s_{1} iff T ⊧ c′, then S ⊧ c iff S ⊧ c[c′].

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

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

(Basis) k + 1 = 2: By Lemma 4.2, it remains to consider Φ = (∃\underline{a}_{1})(∀\underline{a}_{2})E. Since Φ ≡ ¬F′ for Φ′ = (∀\underline{a}_{1})(∃\underline{a}_{2})¬E, Φ is valid iff S(Φ′) |̸= c(Φ′), which can be shown to be equivalent to S(Φ) ⊧ c(Φ).

(Induction). Consider k + 2, i.e. Φ = (Q_{1}\underline{a}_{1}) ⋯ (Q_{k+2}\underline{a}_{k+2})E has k + 2 quantifier alternations. There are two cases for Q_{1}:

1. Q_{1} = ∀: In this case, Φ is valid iff for every truth assignment ϕ to \underline{a}_{1}, the formula Φ_{ϕ} = (∃\underline{a}_{2}) ⋯ (Q_{n+1}\underline{a}_{n+1})E_{ϕ} is valid, where E_{ϕ} is obtained from Φ by replacing in E each occurrence of a_{1_{i}} by ⊤ if ϕ(a_{1_{i}}) = true and by ⊥ otherwise, for all i. Applying the hypothesis for k + 1, Φ_{ϕ} is valid iff S ⊧ c, where S = S(Φ_{ϕ}) and c = c(Φ_{ϕ}). Define

S_{ϕ} = {a_{1,j} : ϕ(a_{1,j}) = true, 1 ≤ j ≤ n_{1}} ∪

\{b_{1,j} : ϕ(a_{1,j}) = false, 1 ≤ j ≤ n_{1}\} ∪ \{\underline{a}_{1} ≢ \underline{b}_{1}\},

p′ = [\underline{a}_{1} ≢ \underline{b}_{1}] ∧ ⋯ ∧ [\underline{a}_{k+1} ≢ \underline{b}_{k+1}] ∧
(E(Φ) ∨ c) ∧ (c ⇒ \underline{a}_{k+2}),

and let s_{1} = p(Φ_{ϕ}) > q be the first counterfactual in the structural sequence of c. It can be shown using Lemma 4.3 that S ⊧ c iff S ∪ S_{ϕ} ⊧ c and that

T ∈ Cn(s_{1}, c, S) ⇔ T ∪ S_{ϕ} ∈ Cn(s_{1}, c, S ∪ S_{ϕ}).

It can be further shown that for every T ∈ Cn(s_{1}, c, S ∪ S_{ϕ}), T ⊧ s_{1} iff T ⊧ p′ > q. It follows from Lemma 4.4 that S ∪ S_{ϕ} ⊧ c (i.e., S ⊧ c) iff S ∪ S_{ϕ} ⊧ c[p′ > q]. Consequently, S ⊧ c iff S(Φ) ∪ S_{ϕ} ⊧ c[p′ > q]. Now observe that p′ = p(Φ) and c[p′ > q] = c_{k}(Φ). It follows that Φ is valid iff S(Φ) ∪ S_{ϕ} ⊧ c_{k}(Φ) for every ϕ. Since c_{k+1}(Φ) = c(Φ) and

Cn(c_{k}(Φ), c(Φ), S(Φ)) = \{S ∪S_{ϕ} : ϕ a truth ass. to \underline{a}_{1}\},

Proposition 2.2 implies that Φ is valid iff S(Φ) ⊧ c(Φ).

2. Q_{1} = ∃: Since Φ ≡ ¬Φ′ for Φ′ = (∀\underline{a}_{1})(∃\underline{a}_{2}) ⋯ (Q′_{k+2}\underline{a}_{k+2})¬E, using case 1.) it is not hard to show that the statement holds for k + 2. □

We obtain the main results of this section.

Theorem 4.5 Let S be a knowledge base and c = p_{1} ≯ (p_{2} ≯ ⋯ (p_{k} ≯ q) ⋯), for constant k ≥ 1. Deciding if S ⊧ c is Σ_{k+1}^{P}-complete.

Proof. (Sketch) Membership in Σ_{k+1}^{P} can be shown by induction on k. For k = 1, this holds by Proposition 2.1; for k > 1, by the hypothesis a guess for W ∈ F(p_{1}, S) with W |̸= p_{2} ≯ (⋯ (p_{k} ≯ q) ⋯) can be verified in polynomial time with a Σ_{k}^{P} oracle. Σ_{k+1}^{P}-hardness follows from Theorem 4.1. □

Theorem 4.6 Given a knowledge base S and c ∈ C, deciding if S ⊧ c is PSPACE-complete. Hardness for PSPACE holds if c has form p_{1} ≯(p_{2} ≯⋯ (p_{n} ≯q) ⋯).

Proof. It is straightforward to design a procedure for deciding S ⊧ c in polynomial space. PSPACE-hardness follows from Theorem 4.1. □

Since evaluating nested counterfactuals is in PSPACE, it is straightforward that evaluating a formula built using the standard propositional connectives from propositional 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 semantics for (p > q) > r using the “possible worlds approach” can be defined as follows. Define

F(p > q, S) = {T ⊆ S : T |̸= p ≯ q,

T ⊂ U ⊆ S ⇒ U ⊧ p ≯ q}.

Note that T ⊧ p > q for every T ∈ F(p > q, S). Now define that (p > q) > r has over S value true (in symbols, S ⊧ (p > q) > r) if T ⊧ r for every T ∈ 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 questionable; we do not know of an intuitive example. Future work will investigate into a semantics, though, which foresees 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 ⊧ p > q:

ND-ALGORITHM LNCF(S, p, q, r) input: finite S ⊆ L, formulas p, q, r ∈ L output: “no” iff S |̸= (p > q) > r

begin Guess S′ ⊆ S; if ¬CF(S′, p, q) or (S′ ⊧ r) then stop else

for each T, S′ ⊂ T ⊆ 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 modulo the CF calls and S′ ⊧ r. An improvement to polynomial 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′ ∉ F(p > q, S) can be given nondeterministically in polynomial time with an oracle for classical and counterfactual inference. As a Π_{2}^{P} oracle is suitable for that, deciding if S′ ∉ F(p > q, S) is in Σ_{3}^{P}. Clearly, a proof for S |̸= (p > q) > r can be given nondeterministically in polynomial time with an oracle for S′ ∉ F(p > q) and classical inference. Thus, Theorem 5.2 Given S and (p>q)>r, deciding if S ⊧ (p>q)>r is in Π_{4}^{P}. Lemma 5.3 Let S′ ⊧ p > q for a S′ ⊆ S. Given S′ and p > q, deciding whether T ⊧ p > q for any T, S′ ⊂ T ⊆ S, is Σ_{3}^{P} -hard. Proof. (Sketch) We transform deciding the validity of Φ = (∃\underline{a}_{1})(∀\underline{a}_{2})(∃\underline{a}_{3})E into this problem, where \underline{a}_{i} = a_{i,1}, …, a_{i,n_{i}}, i = 1, 2, 3. Let c be a new atom and let \underline{a}′_{1} = a′_{1,1}, …, a′_{1,n_{1}}, \underline{a}′′_{1} = a′′_{1,1}, …, a′′_{1,n_{1}}, and \underline{a}′_{2} = a′_{2,1}, …, a′_{2,n_{2}} be groups of new atoms. Define

S′ = \{\underline{a}_{2}, \underline{a}′_{2}, c\},
S = \{\underline{a}_{1}, \underline{a}′_{1}, \underline{a}_{2}, \underline{a}′_{2}, c\},
p = [ c ∧ ⋀_{i=1}^{n_{1}}(¬a_{1,i} ∧ ¬a′_{1,i} ∧ a′′_{1,i}) ] ∨

[ ⋀_{i=1}^{n_{1}}[(a_{1,i} ∧ a′_{1,i} ⇒ ¬c) ∧ (a_{1,i} ∨ a′_{1,i} ⇒ a′′_{1,i})] ∧

⋀_{i=1}^{n_{2}}(a_{2,i} ≢ a′_{2,i}) ∧ (c ⇒ E) ] ,
q = c ∧ ⋀_{i=1}^{n_{1}}a′′_{1,i}.

Notice that S′, S, p and q are constructible in polynomial time. It is not hard to see that S′ ⊧ p > q. Moreover, it can be shown that there exists T, S′ ⊂ T ⊆ S, such that T ⊧ p > q iff Φ is valid. □

Theorem 5.4 Deciding if S ⊧ (p > q) > r from S and (p>q)>r is Π_{4}^{P} -hard. Proof. (Sketch) The proof is an extension of the transformation in the proof of Lemma 5.3. Let

Φ = (∀\underline{b}^{∗})(∃\underline{a}_{1})(∀\underline{a}_{2})(∃\underline{a}_{3})E,

\underline{b}^{∗} = b_{1}, …, b_{n_{b}}, and let \underline{b} = b_{1}, …, b_{2n_{b}}, \underline{b}′ = b′_{1}, …, b′_{2n_{b}}, \underline{b}′′ = b′′_{1}, …, b′′_{2n_{b}} using new atoms. Define

S = S_{1} ∪ \{\underline{b}, \underline{b}′\},
p = ⋀_{i=1}^{2n_{b}}[(b_{i} ∧ b′_{i} ⇒ ¬c) ∧ (b_{i} ∨ b′_{i} ⇒ b′′_{i})] ∧ p_{1},
q = ⋀_{i=1}^{2n_{b}} b′′_{i} ∧ ⋀_{i=1}^{n_{b}}(b_{i} ≡ b_{n_{b}+i}) ∧ q_{1},
r = ⋀_{j=1}^{n_{2}}(a_{2,j} ∧ a′_{2,j}) ∧ c ⇒ ⋁_{i=1}^{n_{1}}(a_{1,i} ∨ a′_{1,i}),

where S_{1} (resp. p_{1}, q_{1}) is constructed as S (resp. p, q) in the proof of Lemma 5.3. It can be shown that S ⊧ (p > q) > r iff Φ is valid. □

Corollary 5.5 Deciding if S ⊧ (p > q) > r from S and (p > q) > r is Π_{4}^{P} -complete.

6 Related work and conclusion

Complexity characterizations of evaluating counterfactuals are given in [Winslett, 1990; Nebel, 1991; Grahne, 1991; Grahne and Mendelzon, 1991]. Grahne and Mendelzon [Grahne and Mendelzon, 1991] considered subjunctive 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 [Winslett, 1988]. In particular, [Grahne and Mendelzon, 1991, Corollary 4.2] implies that evaluating nested counterfactuals under this update semantics is PSPACE-complete.

Our work contributes to the recent effort in giving a precise complexity characterization of nonmonotonic reasoning in the full propositional context, cf. [Niemelä, 1991; Winslett, 1990; Nebel, 1991; Rutenburg, 1991; Eiter and Gottlob, 1992; Stillman, 1992] (see [Cadoli and Schaerf, 1992] for an overview), extending previous results for restricted contexts, e.g. [Kautz and Selman, 1991; Stillman, 1990; Selman and Levesque, 1990; Cadoli and Lenzerini, 1990; Provan, 1990]. Such a characterization supports a better understanding of the computational relationships between various forms of nonmonotonic reasoning, e.g. efficient intertranslatability. Furthermore, the precise complexity of a problem gives us a clue of its computational difficulty and may provide insight to sources of complexity. For counterfactuals, these sources are classical inference (S ⊧ p) and the many knowledge bases that are possible after incorporating a change. Fortunately, a sequence of changes is not a source of complexity. Since Π_{2}^{P} - 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 fruitfully applied for proving S |̸= p_{1} > (p_{2} > ⋯ (p_{n} > q) ⋯) if all propositional formulas are Horn clauses.

Acknowledgments

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

References

[Cadoli and Lenzerini, 1990] Marco Cadoli and Maurizio Lenzerini. The Complexity of Closed World Reasoning and Circumscription. In Proceedings AAAI-90, pages 550–555, 1990.

[Cadoli and Schaerf, 1992] M. Cadoli and M. Schaerf. A Survey on Complexity Results for Non-monotonic Logics. Technical report, Dipartimento di Informatica e Sistemistica, Università di Roma “La Sapienza”, 1992. Journal of Logic Programming, to appear.

[Eiter and Gottlob, 1992] Thomas Eiter and Georg Gottlob. On the Complexity of Propositional Knowledge Base Revision, Updates, and Counterfactuals. Artificial Intelligence, 57(2–3):227–270, 1992.

[Fagin et al., 1983] R. Fagin, J. D. Ullman, and M. Y. Vardi. On the Semantics of Updates in Databases. In Proceedings PODS-83, pages 352–365, 1983.

[Gärdenfors, 1988] P. Gärdenfors. Knowledge in Flux. Bradford Books, MIT Press, 1988.

[Garey and Johnson, 1979] Michael Garey and David S. Johnson. Computers and Intractability – A Guide to the Theory of NP-Completeness. W. H. Freeman, New York, 1979.

[Ginsberg and Smith, 1988] Matthew L. Ginsberg and David E. Smith. Reasoning About Action I: A Possible Worlds Approach. Artificial Intelligence, 35:165–195, 1988.

[Ginsberg, 1986] Matthew L. Ginsberg. Counterfactuals. Artificial Intelligence, 30:35–79, 1986.

[Grahne and Mendelzon, 1991] Gösta Grahne and Alberto O. Mendelzon. Updates and Subjunctive Queries. Technical Report KRR-TR-91-4, University of Toronto, CS Dept., July 1991. Information and Computation, to appear.

[Grahne, 1991] Gösta Grahne. Updates and Counterfactuals. In Proceedings KR-91, pages 269–276, 1991.

[Kautz and Selman, 1991] H. Kautz and B. Selman. Hard Problems for Simple Default Logics. Artificial Intelligence, 49:243–279, 1991.

[Nebel, 1991] Bernhard Nebel. Belief Revision and Default Reasoning: Syntax-Based Approaches. In Proceedings KR-91, pages 417–428, 1991.

[Niemelä, 1991] I. Niemelä. Towards Automatic Reasoning. In Proc. Europ. Workshop on Logics in AI, Amsterdam, September 1990, LNCS 478. Springer, 1991.

[Provan, 1990] Gregory Provan. The Computational Complexity of Multiple-Context Truth Maintenance Systems. In Proceedings ECAI-90, pages 522–527, 1990.

[Rabin and Scott, 1959] M.O. Rabin and D. Scott. Finite Automata and Their Decision Problem. IBM J. of Research and Development, 3:114–125, 1959.

[Rutenburg, 1991] V. Rutenburg. Complexity Classification in Truth Maintenance Systems. In Proceedings STACS-91, pages 373–383, 1991.

[Selman and Levesque, 1990] Bart Selman and Hector J. Levesque. Abductive and Default Reasoning: A Computational Core. In Proceedings AAAI-90, pages 343–348, July 1990.

[Selman et al., 1992] B. Selman, H. Levesque, and D. Mitchell. A New Method for Solving Hard Satisfiability Problems. In Proceedings AAAI-92, pages 440–446, 1992.

[Stillman, 1990] J. Stillman. It’s Not My Default: The Complexity of Membership Problems in Restricted Propositional Default Logic. In Proceedings AAAI-90, pages 571–579, 1990.

[Stillman, 1992] J. Stillman. The Complexity of Propositional Default Logic. In Proceedings AAAI-92, pages 794–799, 1992.

[Vardi, 1989] M. Vardi. On the Complexity of Epistemic Reasoning. In Proceedings Fourth Annual Symposium on Logic in Computer Science LICS-89, pages 243– 252. IEEE Computer Science Press, 1989.

[Winslett, 1988] Marianne Winslett. Reasoning About Action Using a Possible Models Approach. In Proceedings AAAI-88, pages 89–93, 1988.

[Winslett, 1990] Marianne Winslett. Updating Logical Databases. Cambridge University Press, 1990.