Equivalence in Abductive Logic

1 Introduction

Nowadays, abduction is used in many AI applications, including diagnosis, design, updates, and discovery. Abduction is an important paradigm for problem solving, and is incorporated in programming technologies, i.e., abductive logic programming (ALP) [12]. Automated abduction is also studied in the literature as an extension of deductive methods or a part of inductive systems, and its computational properties have also been studied [22; 2; 3; 4].

In this work, we are concerned with such computational issues on abductive reasoning. Despite being a problemsolving paradigm, ALP has a lot of issues which have not been fully understood yet. In particular, there are no concrete methods for (a) evaluation of abductive power in ALP, (b) measurement of efficiency in abductive reasoning, (c) semantically correct simplification and optimization, (d) debugging and verification in ALP, and (e) standardization in ALP. Since all these topics are important for any programming paradigm, the lack of them is a serious drawback of ALP. Then, it can be recognized that all the above issues are related to different notions of identification or equivalence in ALP. In particular,

Chiaki Sakama

Wakayama University Sakaedani, Wakayama 640-8510 Japan sakama@sys.wakayama-u.ac.jp

the item (c) is related to understanding the semantics of ALP with respect to modularity and contexts.

Abduction can be formalized in various logics [13]. Then, we can consider several notions of equivalence in several logics for abduction. In this paper, we will give two definitions of abductive equivalence in two logical frameworks for abduction. Two logics we consider here are first-order logic (FOL) and abductive logic programming (ALP). The first abductive equivalence, called explainable equivalence, requires that two abductive programs have the same explainability for any observation. Another one, explanatory equivalence, guarantees that any observation has exactly the same explanations in each abductive framework. Explanatory equivalence is stronger than explainable equivalence.

In this paper, we characterize these two notions of abductive equivalence in terms of other well-known concepts in AI and logic programming. In abduction in first-order logic, we will see that explainable equivalence can be verified by the notion of equivalence in default logic [18], which is defined for the families of extensions of two default theories. On the other hand, abductive equivalence in ALP is more complicated than in the case of FOL due to the nonmonotonicity in logic programs. In fact, equivalence between two abductive logic programs has little been discussed in the literature except that effects of partial deduction in ALP are analyzed in [20]. Here, we will see that explanatory equivalence in ALP can be characterized by the notion of (relative) strong equivalence [14; 10; 24].

The rest of this paper is organized as follows. Section 2 presents two definitions for abductive equivalence. Section 3 considers first-order logic as the representation language, while Section 4 considers nonmonotonic logic programming for ALP. Section 5 gives concluding remarks.

2 Abductive Equivalence

We start with the question as to when two abductive frameworks are equivalent. As far as the authors know, there is no answer for such a question in the literature of ALP. There are many parameters which should be considered important in defining equivalence notions in abductive frameworks. In the world, both background knowledge and observations are surely essential. In an agent who performs abduction, on the other hand, her abductive power must depend on her logic

(language, syntax, semantics) of background knowledge, observations and hypotheses. Moreover, the quality of abduction is relevant to other parameters such as axioms, inference procedures, logics of explanations, and criteria of best explanations. If we would take all such parameters into account, the task of defining the equivalence notion might become combinatorial and too complex.

In the following, we thus consider a rather simple framework for our problem while we try to hold the essence of equivalence notions as much as possible. First, logic, background knowledge and hypotheses are put as input parameters in each abductive framework. Secondly, a logic of explanations is taken into account in a definition, but its diversity is reflected in different notions of abductive equivalence.

The following definition of abductive frameworks is a standard one [13; 22; 2; 3]. As a notation, A6 CYBP  BY means that a formula BY is derived from a set A6 of formulas in a logic .

Definition 2.1 Let BU and be sets of formulas in some underlying logic . An abductive framework is defined as a triple B4BNBUBNB5, where BU is called background knowledge and each element of is called a candidate hypothesis.

Definition 2.2 Let B4BNBUBNB5 be an abductive framework, and  a formula in , and BX a formula belonging to . We define that BX is an explanation of an observation  in B4BN BUBN B5 if BU CJ BX CYBP   and BU CJ BX is consistent in . We say that  is explainable in B4BN BUBN B5 if it has an explanation in B4BN BUBN B5.

We now give two definitions for abductive equivalence. We assume that the underlying logic  is common when two abductive theories are compared.

Definition 2.3 Two abductive frameworks B4BNBU BD BN BD B5 and B4BN BU BE BN BE B5 are explainably equivalent if, for any observation , there is an explanation of  in B4BNBU BD BN BD B5 iff there is an explanation of  in B4BN BU BE BN BE B5.

Explainable equivalence requires that two abductive frameworks have the same explainability for any observation. Explainable equivalence may reflect a situation that two programs have different knowledge to derive the same goals.

Definition 2.4 Two abductive frameworks B4BNBU BD BN BD B5 and B4BNBU BE BN BE B5 are explanatorily equivalent if, for any observation , BX is an explanation of  in B4BNBU BD BN BD B5 iff BX is an explanation of  in B4BN BU BE BN BE B5.

Explanatory equivalence assures that two abductive frameworks have the same explanation power for any observation. Explanatory equivalence is stronger than explainable equivalence as follows.

Proposition 2.1 If abductive frameworks B4BNBU BD BN BD B5 and B4BNBU BE BN BE B5 are explanatorily equivalent, then they are explainably equivalent.

For explanatory equivalence, we can assume that the hypotheses are common in two abductive frameworks in Definition 2.4, as the following property holds.

Proposition 2.2 If BT BD BP B4BNBU BD BN BD B5 andBT BE BP B4BNBU BE BN BE B5 are explanatorily equivalent, then BC BD BP BC BE , where BC CX BP CUCW BE CX CY BU CX CJ CUCWCV is consistent in CV for CX BP BDBN BE.

Proof. Assume that BC BD D2 BC BE BIBP BN. Then, for a formula B3 BE BC BD D2 BC BE , CUB3CV is an explanation of B3 in BT BD because BU BD CJ CUB3CV is consistent in . However, CUB3CV is not an explanation of B3 in BT BE . Hence, BT BD and BT BE are not explanatorily equivalent. BE

Note in Proposition 2.2 that any hypothesis CW in CX D2 BC CX cannot be added without violating the consistency of BU CX CJCUCWCV in . Thus, BC CX is the set of hypotheses that can be actually used in explanations of some formulas.

Example 2.1 Suppose the abductive frameworks BT BD BP B4FOLBN CUCPARD4CVBN CUCPBN CQCVB5 and BT BE BP B4FOLBN CUCQARD4CVBN CUCPBN CQCVB5. Then, BT BD and BT BE are explainably equivalent, but are not explanatorily equivalent. On the other hand, BT BF BP B4FOLBN CUCPARD4CVBN CUCQCVB5 and BT BG BP B4FOLBN CUCQARD4CVBN CUCQCVB5 are neither explainably equivalent nor explanatorily equivalent.

3 Abduction in First-order Logic

Abduction is used in many AI applications, and classical firstorder logic is most often used as the underlying logic for abduction [17; 13; 2; 22]. When the underlying logic  is FOL, the relation CYBP  becomes the usual entailment relation CYBP. In first-order abduction, explanations are usually defined as a set of ground instances from hypotheses [17]. That is, a set BX of ground instances of elements of is an explanation of  in B4FOLBN BUBN B5 if A6 CJ BX CYBP  and A6 CJ BX is consistent.

In the following, CCCWB4A6B5 denotes the set of logical consequences of a set A6 of first-order formulas. That is, CCCWB4A6B5 BP CUBY CY A6 CYBP BYCV. The next definition is originally given for default logic by Reiter [18].

Definition 3.1 [19; 17] Let BU and be sets of first-order formulas. An extension of BU with respect to is CCCWB4BU CJ CBB5 where CB is a maximal subset of ground instances of elements from such that BU CJ CB is consistent.

Using the notion of extensions, explainable equivalence can be characterized in first-order abduction.

Theorem 3.1 Two abductive frameworks B4FOLBN BU BD BN BD B5 and B4FOLBN BU BE BN BE B5 are explainably equivalent iff the extensions of BU BD with respect to BD coincide with the extensions of BU BE with respect to BE .

Proof. First, we claim that the union of the extensions of BU with respect to are exactly the set of formulas explainable in B4FOLBNBUBNB5. To see this, we can use a wellknown theorem [17; 22] that a formula  can be explained in B4FOLBNBUBNB5 iff there is a consistent extension CG of BU with respect to such that CG contains . Thus, the set of all explainable formulas are precisely those formulas contained in at least one extension of BU with respect to .

Now, let BT BD BP B4FOLBNBU BD BN BD B5 and BT BE BP B4FOLBNBU BE BN BE B5 be two abductive frameworks. Suppose that the extensions of BU BD with respect to BD coincide with those of BU BE with respect to BE . By the above claim, the set of formulas explainable in BT BD is equal to the set of formulas explainable in BT BE . This means that BT BD and BT BE are explainably equivalent.

Conversely, assume that there is an extension CG BE of BU BE with respect to BE which is not an extension of BU BD with respect to BD . Let BY CG BE be a first-order formula which is logically equivalent to CG BE . Such a formula actually exists because CG BE BP CCCWB4BU BE CJ CBB5 holds for some maximally consistent subset CB of BE , and hence CG BE is logically equivalent to CE CUBEBU BE CU CM CE CVBECB CV. Since CG BE is consistent, BY CG BE is consistent too. Then, BY CG BE is explainable in BT BE because CB is an explanation of BY CG BE .

Now, if BY CG BE is not explainable in BT BD , then obviously BT BD and BT BE are not explainably equivalent. Hence, there is an explanation of BY CG BE in BT BD . Then, there is an extension CG BD of BU BD with respect to BD which contains BY CG BE . Since CG BE is not an extension ofBU BD with respect to BD , CG BD BIBPCG BE holds. Then, CG BE AQ CG BD . Let BY CG BD be a formula which is logically equivalent to CG BD . By the same argument as above, BY CG BD is explainable in BT BD . However, this BY CG BD cannot be explained in BT BE . This is because, if BY CG BD were explained in BT BE , there must be an extension CG BC BE of BU BE with respect to BE such that CG BE AQ CG BC BE , which is impossible because any extension is orthogonal to another extension in a default theory [18]. In any case, BT BD and BT BE are not explainably equivalent. BE

In [15], Reiter's default theories A1 BD BP B4BW BD BNBU BD B5 and A1 BE BP B4BW BE BNBU BE B5 are said to be equivalent if the extensions of A1 BD are the same as the extensions of A1 BE . When an abductive framework B4FOLBNBUBNB5 is given, we can associate a default theory A1 BP B4BWBNBUB5 where BW is the set of prerequisite-free normal defaults CU BMCS CS CY CS BE CV such that there is a one-to-one correspondence between the extensions of A1 and the extensions of BU with respect to [17].

Corollary 3.2 Two abductive frameworks B4FOLBNBU BD BN BD B5 and B4FOLBNBU BE BN BE B5 are explainably equivalent iff the default theories B4BW BD BNBU BD B5 and B4BW BE BNBU BE B5 are equivalent where BW CX BP CU BMCS CS CY CS BE CX CV for CX BP BDBN BE.

Example 3.1 Suppose two abductive frameworks, BT BD BP B4FOLBN BU BD BN BD B5 and BT BE BP B4FOLBN BU BE BN BE B5, where

BU BD BP CUCP AR D4BN CQ AR BMD4CVBN

BD BP CUCPBN CQBN CP AH CRBN CQ AH CSBN D4 AH D5CVBN

BU BE BP CUCR AR D5BN CS AR BMD5CVBN and

BE BP CUCRBN CSBN CP AH CRBN CQ AH CSBN D4 AH D5CVBM

Then, BT BD and BT BE are explainably equivalent. In fact, the two extensions of BU BD with respect to BD are CCCWB4BU BD CJ B4 BD D2 CUCQCVB5B5 BP CC CWB4CUCPBN BMCQBN CRBN BMCSBN D4BN D5CVB5 and CC CWB4BU BD CJB4 BD D2CUCPCVB5B5 BP CCCWB4CUBMCPBN CQBN BMCRBN CSBN BMD4BN BMD5CVB5, which are respectively equivalent to the two extensions of BU BE with respect to BE , CCCWB4BU BE CJ B4 BE D2 CUCSCVB5B5 and CCCWB4BU BE CJ B4 BE D2 CUCRCVB5B5.

It is interesting to see that we can transform any abductive framework to an explainably equivalent abductive framework whose background theory is empty. The next property is also derived by the representation theory for default logic [15].

Corollary 3.3 For any abductive framework B4FOLBNBUBNB5, there is an abductive framework B4FOLBN BNBN BC B5 which is explainably equivalent to B4FOLBNBUBNB5.

Proof. Put BC BP CUCWCMB3 CY CW BE CVCJCUB3CV, where B3 BP CE CUBEBU CU . Then, it holds for any  that, BU CJ BX CYBP  iff BX BC CYBP  where BX AI and BX BC BP CUCW CM B3 CY CW BE BXCV CJ CUB3CV AI BC . BE

An abductive framework B4BN BUBN B5 is called compatible if BU CJ is consistent. Explainable equivalence can be easily verified for compatible frameworks.

Corollary 3.4 Two compatible abductive frameworks B4FOLBN BU BD BN BD B5 and B4FOLBN BU BE BN BE B5 are explainably equivalent iff BU BD CJ BD AH BU BE CJ BE .

An abductive framework B4FOLBN BUBN B5 is called assumptionfree where  is the set of all literals in the underlying language. It is known that the complexity of finding explanations in assumption-free abductive frameworks is not harder than that in assumption-based frameworks [22; 4]. Explainable equivalence in the assumption-free case can also be simply characterized as follows.

Corollary 3.5 Two abductive frameworks B4FOLBNBU BD BN B5 and B4FOLBN BU BE BN B5 are explainably equivalent iff BU BD AH BU BE .

Proof. For an assumption-free abductive framework B4FOLBNBUBN B5, each extension of BU with respect to  is logically equivalent to a model of BU. Hence, explainable equivalence implies that the models of BU BD coincide with the models of BU BE , and vice versa. BE

For explanatory equivalence in first-order abduction, logical equivalence of background theories is necessary and sufficient.

Theorem 3.6 Two abductive frameworks B4FOLBNBU BD BNB5 and B4FOLBN BU BE BN B5 are explanatorily equivalent iff BU BD AH BU BE .

Proof. If BU BD AH BU BE , then for any BX and any , it holds that, BU BD CJBX CYBP  iff BU BE CJBX CYBP , and that, BU BD CJBX is consistent iff BU BE CJBX is consistent. Hence, B4FOLBN BU BD BN B5 and B4FOLBN BU BE BN B5 are explanatorily equivalent.

Conversely, suppose that B4FOLBNBU BD BNB5 and B4FOLBNBU BE BNB5 are explanatorily equivalent. Then, for any formula  and any BX from , it holds that BU BD CJ BX CYBP  iff BU BE CJ BX CYBP . Then, for any BX, we have CCCWB4BU BD CJBXB5 BP CCCWB4BU BE CJBXB5. That is, BU BD CJBX AH BU BE CJBX holds for any BX. This implies BU BD AH BU BE when BX BP BN. BE

The complexity of abductive equivalence in the propositional case can be given as follows.

Lemma 3.7 [1] Let A1 BP B4BWBNCFB5 be a prerequisite-free normal default theory. Then, a formula B3 is true in all extensions of A1 iff A1 BC BP B4BWBN CF CJ CUB3CVB5 and A1 are equivalent.

Theorem 3.8 Deciding explainable equivalence in propositional abduction is A5  BE -complete.

Proof. By Corollary 3.2 and Lemma 3.7, cautious reasoning in default logic can be transformed to explainable equivalence via equivalence of default theories. This transformation is obviously feasible in polynomial time. Because cautious reasoning from prerequisite-free normal default theories is A5  BE -complete [6], the decision problem of explainable equivalence is A5  BE -hard.

We now prove membership in A5  BE . Two abductive frameworks BT BD BP B4FOLBNBU BD BN BD B5 and BT BE BP B4FOLBNBU BE BN BE B5 are not explainably equivalent iff there is an extension of BU BD with respect to BD which is not an extension of BU BE with respect to BE . Given a subset CB AI BD as a guess, deciding if CG BP CCCWB4BU BD CJ CBB5 is an extension of BU BD with respect to BD can be checked by computing the "reduct" CB BC of BD by CG and then checking if BU BD CJ CB AH BU BD CJ CB BC . Here, computing the reduct requires satisfiability tests, and this computation as well as testing logical equivalence can be done in polynomial time with an NP-oracle. Once we know that CG is an extension of BU BD with respect to BD , we need to check if CG is not an extension of BU BE with respect to BE , which can also be done in the same way as the former test. Thus, we can construct a polynomial-time nondeterministic Turing machine with an NP-oracle to decide if BT BD and BT BE are not explainably equivalent. Hence, the original problem is the complement of this, and belongs to coNP NP BP A5  BE . BE

Theorem 3.9 The following decision problems in propositional abduction are coNP-complete.

1. Explainable equivalence of two compatible abductive frameworks.
2. Explainable equivalence of two assumption-free abductive frameworks.
3. Explanatory equivalence of two abductive frameworks.

Proof. By Corollaries 3.4 and 3.5 and Theorem 3.6, these problems can be solved by checking logical equivalence of two propositional theories, which is coNP-complete. BE

4 Abductive Logic Programming

Abductive logic programming (ALP) is another popular formalization of abduction in AI [12; 3]. Background knowledge in ALP is called a logic program, and the candidate hypotheses are given as literals called abducibles. The most significant difference between abduction in FOL and ALP is that ALP allows the nonmonotonic negation-as-failure operator D2D3D8 in background knowledge. In abduction, addition of hypotheses may invalidate explanations of some observations if the background theory is nonmonotonic.

Recall that a (logic) program is a set of rules of the form

where each  CX is a literal B4D2 AL D1 AL D0 AL CZ AL BCB5, and D2D3D8 is negation as failure (NAF). The symbol BN represents a disjunction. The left-hand side of the rule is the head, and the right-hand side is the body. A rule with variables stands for the set of its ground instances. In this paper, the semantics of a logic program is given by its answer sets [5; 9], while another semantics can be considered as well in ALP [12; 3]. Problem solving by representing knowledge as a logic program and then computing its answer sets is called answer set programming (ASP).

Definition 4.1 An abductive (logic) program is defined as a pair CWBNBTCX, where  is a logic program and BT is a set of literals called abducibles. Instead of using the notation B4ALPBN BNBTB5, we also use CWBNBTCX to represent an abductive framework whose underlying logic is ALP.

Definition 4.2 Let CWBNBTCX be an abductive program, and BZ a conjunction of ground literals called observations. A set BX AI BT is a (credulous) explanation of BZ in CWBNBTCX 1 if every ground literal in BZ is true in a consistent answer set of  CJBX.

1 Another, skeptical notion for explanations is defined as BX AI BT such that BZ is true in all consistent answer sets of  CJ BX.

Note that both abducibles and observations are restricted to ground literals in ALP. However, it is known for this framework that rules can be allowed in abducibles and that observations can contain NAF formulas as well as literals [8]. Definition 4.2 can also be represented in a different way as follows [8]. A belief set (with respect to BX) of an abductive program CWBNBTCX is a consistent answer set of a logic program  CJ BX where BX AI BT. Then, BX AI BT is an explanation of BZ if BZ is true in a belief set of CWBN BTCX with respect to BX.

Definition 4.3 Let BT BD BP CW BD BNBT BD CX and BT BE BP CW BE BNBT BE CX be abductive programs. BT BD and BT BE are explainably equivalent if, for any ground literal BZ, BZ is explainable in BT BD iff BZ is explainable in BT BE . BT BD and BT BE are explanatorily equivalent if, for any conjunction of ground literals BZ, BX is an explanation of BZ in BT BD iff BX is an explanation of BZ in BT BE .

Explainable equivalence in ALP guarantees the same explainability for any ground literal as a single observation, but it does not matter how each observation is explained. Hence, we do not have to care about whether multiple observations can be jointly explained by a common explanation. On the other hand, explanatory equivalence in ALP guarantees that, any conjunction (or set) of observations 2 has exactly the same credulous explanations. Hence, explanatory equivalence implies that any set of abducibles BX AI BT should explain the same set of observations in each abductive program.

We now show that explainable equivalence in ALP can be checked by comparing the belief sets of two abductive programs. Because there exist several methods to compute belief sets using ASP [21; 8; 9], checking explainable equivalence is also possible using such methods. In the following, we denote the set of all belief sets of CWBNBTCX as BUCBB4BNBTB5.

Theorem 4.1 Abductive programs CW BD BNBT BD CX and CW BE BNBT BE CX are explainably equivalent iff

Proof. Recall that BX AI BT is an explanation of a ground literal BZ iff BZ is true in a belief set of CWBNBTCX with respect to BX. Then, the set of all explainable literals are precisely those literals contained in some belief sets of CWBN BTCX with respect to some BX. Hence, the union of the belief sets of CWBN BTCX are exactly the set of literals explainable in CWBNBTCX. Therefore, two abductive programs are explainably equivalent iff the unions of the belief sets of two abductive programs coincide. BE

In some case of compatible problems, explanatory equivalence can be easily verified. Here, a logic program is definite if every its rule is NAF-free and has exactly one atom in the head and only atoms in the body. A definite program has a unique answer set that is equivalent to its least model. An abductive program CWBNBTCX is called definite if  is a definite logic program and BT is a set of atoms.

Corollary 4.2 Two definite abductive programs CW BD BNBT BD CX and CW BE BNBT BE CX are explainably equivalent if the least model of  BD CJ BT BD coincides with that of  BE CJ BT BE .

2 We assume that the set of observations includes the special atom BQ, which represents the empty conjunction of observations. Note that BQ is always true in any consistent set of ground literals.

Example 4.1 Given the common set of abducibles BT BP CUCPBN CQCV and three logic programs:

the three abductive programs CW CX BNBTCX (for CX BP BDBN BEBN BF) are all explainably equivalent, but none of them are explanatorily equivalent. In particular, the least model of  BD CJ BT is CUD4BN D5BN CPBN CQCV, which is identical to that of  BE CJ BT.  BF is not definite because of the third rule, but CW BF BNBTCX has three belief sets: CUD4CVBN CUD4BN D5BN CPCVBN CUD4BN CQCV, the union of which is equal to that of CW CX BN BTCX for CX BP BDBN BE.

Explanatory equivalence in ALP, on the other hand, requires a more semantical notion of logic programming. 3 For this purpose, we need to utilize the concept of equivalence in logic programming and ASP.

There are several notions for equivalence in logic programming, and weak equivalence and strong equivalence are most well known. We say that two programs are weakly equivalent if they simply agree with their answer sets. The notion of weak equivalence is similar to that of logical equivalence in FOL and other classical logics. Given two abductive programs CW BD BNBTCX and CW BE BNBTCX, however, weak equivalence of  BD and  BE is not a sufficient condition for explanatory equivalence of them, and is not even a sufficient condition for explainable equivalence. Weak equivalence is meaningful only when the abducibles are empty.

Proposition 4.3 Abductive programs CW BD BN BNCX and CW BE BN BNCX are explanatorily equivalent iff  BD and  BE are weakly equivalent.

On the other hand, strong equivalence [14] is a more context-sensitive notion for equivalence of logic programs. Two logic programs  BD and  BE are said to be strongly equivalent if for any additional logic program CA,  BD CJCA and  BE CJCA have the same answer sets. When we allow NAF in logic programs, weak equivalence is too fragile as a criterion. For example, CUD4 AW D2D3D8 CPCV and CUD4 AW CV are weakly equivalent with the same unique answer set CUD4CV, but adding CP to both results in the withdrawal of D4 in the former. Often, we can restrict the language for additional programs CA to some subset CA of the whole language of programs. Then, two programs  BD and  BE are said to be strongly equivalent with respect to CA if  BD CJCA and  BE CJCA have the same answer sets for any program CA AI CA [10]. The equivalence notion with such restriction is called relative strong equivalence [10; 24]. Using this notion, explanatory equivalence can be characterized as follows.

Theorem 4.4 Two abductive programs CW BD BNBTCX and CW BE BNBTCX are explanatorily equivalent iff  BD and  BE are strongly equivalent with respect to BT.

Proof. Suppose that CW BD BNBTCX and CW BE BNBTCX are explanatorily equivalent. Then, for any conjunction BZ of literals and any

3 Explanatory equivalence of CW BD BNBTCX and CW BE BNBTCX implies BUCBB4 BD BNBTB5 BP BUCBB4 BE BNBTB5, but the converse does not hold. For example, when  BD BP CUCP AW BN D4 AW CPCV,  BE BP CUCP AWD2D3D8 CPBN D4 AW CPCV and BT BP CUCPCV, BUCBB4 BD BN BTB5 BP BUCBB4 BE BN BTB5 BP CUCUCPBN D4CVCV. However, BN is an explanation of D4, CP and BQ in CW BD BN BTCX, but is not in CW BE BN BTCX.

BX AI BT, it holds that, BX is an explanation of BZ in CW BD BNBTCX iff BX is an explanation of BZ in CW BE BNBTCX. The latter equivalence then implies that, for any BZ and any BX, we have that, BZ is true in a belief set of CW BD BNBTCX with respect to BX iff BZ is true in a belief set of CW BE BNBTCX with respect to BX. Then, for any BZ and any BX, BZ is true in an answer set of  BD CJ BX iff BZ is true in an answer set of  BE CJ BX. That is, for any BX and any set CB of literals, CB is an answer set of  BD CJ BX iff CB is an answer set of  BE CJBX. Hence,  BD and  BE are strongly equivalent with respect to BT. The converse direction can also be proved by tracing the above proof backward. BE

Example 4.2 Given the common set of abducibles BT BP CUCPBN CQCV, consider three programs

Then, the three abductive programs CW CX BNBTCX (for CX BP BDBN BEBN BF) are explainably equivalent. Although CW BD BNBTCX is explanatorily equivalent to CW BE BNBTCX, it is not to CW BF BNBTCX [20]. In fact,  BD and  BE are strongly equivalent with respect to BT, while  BD and  BF are not because the addition of CP derives D4 in  BD but this is not the case in  BF . This example shows that unfold/fold transformation [23] does not preserve explanatory equivalence in ALP [20] even when  BD and  BE are definite.

The complexity results of abductive equivalence in ALP are given as follows.

Theorem 4.5 Deciding explainable equivalence in propositional ALP is in A1  BF .

Proof. Explanation-finding, i.e., deciding if each literal has an explanation in an ALP, is a A6  BE -complete problem [3]. To decide explainable equivalence, we need to check if explainability agrees in two abductive frameworks for each literal. Thus we can construct a polynomial-time deterministic Turing machine with an oracle for the explanation-finding problem in order to decide explainable equivalence. Hence, the problem is in  A6  BE BPA1  BF . BE

Theorem 4.6 Deciding explainable equivalence in propositional ALP is A5  BE -hard.

Proof. The problem contains the case that the abducibles are empty. In this case, explainable equivalence and explanatory equivalence coincide. Then, by Proposition 4.3, the problem reduces to deciding weak equivalence of two logic programs, which is known to be A5  BE -complete [16]. BE

Corollary 4.7 Explainable equivalence of two definite abductive programs can be decided in polynomial time.

Theorem 4.8 Deciding explanatory equivalence in propositional ALP is A5  BE -complete.

Proof. From a set BT of literals, we construct a logic program

where Æ D0 is a new atom which is uniquely associated with D0. Then, it can be shown that,  BD and  BE are strongly equivalent with respect to BT iff  BC BD BP  BD CJAMB4BTB5 and  BC BE BP  BE CJAMB4BTB5 are weakly equivalent. By Theorem 4.4, explanatory equivalence of CW BD BNBTCX and CW BE BNBTCX reduces to weak equivalence of  BC BD and  BC BE , which is A5  BE -complete [16]. BE

5 Conclusion

We have introduced the notion of abductive equivalence in this paper. We have considered two definitions of abductive equivalence in two logics. Two important differences between FOL and ALP as the underlying logics are that (1) explainability is considered for all formulas in FOL while only literals are considered as observations in ALP, and that (2) nonmonotonicity by NAF appears in ALP while this is not the case in FOL. Intuitively, the restriction of observations to literals in ALP gives more chances for two abductive programs to be equivalent, but the existence of nonmonotonicity in ALP makes comparison of abductive programs more complicated. In each case, we can observe that explanatory equivalence is not computationally harder than explainable equivalence.

• In [11], the notion of abductive equivalence in this paper is further applied to extended abduction [7], where hypotheses can not only be added to a program but also be removed from the program to explain an observation. In extended abduction, explanatory equivalence can be characterized by the notion of update equivalence [10].

We have observed that logical equivalence of background theories in FOL or weak equivalence of logic programs does not simply imply abductive equivalence except for some very simple cases. That is why we need to characterize abductive equivalence in terms of other known concepts in classical or nonmonotonic logics. Having such characterizations in this paper, the next target is to develop transformation techniques which preserve abductive equivalence. In another future work, we can consider other underlying logics for background theories, hypotheses and observations as well as the criteria of best explanations for abductive equivalence.

Acknowledgment

We thank Kazuhisa Makino for his valuable comments.