Resource-bounded inference from inconsistent belief bases

1 Introduction

Few would dispute the fact that classical entailment is not suited to common-sense inference. One of its main drawbacks is its inability to deal with inconsistency. Indeed, any formula is a logical consequence of a contradiction. Such a trivialization of inference is often referred to as ex falso quodlibet sequitur and classical entailment is said to be explosive (i.e., not paraconsistent).

Many approaches have been proposed so far to address this issue. Some of them, like belief revision, aim at preventing inconsistencies from being generated; other approaches aim at removing inconsistencies once they appeared. Complementary to them, many approaches deal with inconsistencies. Among them are various paraconsistent logics, argumentative logics, belief merging and the so-called coherence-based approach 1 to inconsistency handling. Unfortunately, existing paraconsistent inference relations are typically intractable (see [Cayrol et al., 1998] [Nebel, 1998]).

In this paper, we show that trivialization in presence of inconsistency and intractability can be handled within a uniform framework. A family of paraconsistent resourcebounded inference relations is presented. Our starting point is the notion of CB A0 BF inference [Schaerf and Cadoli, 1995] and the coherence-based approach to inconsistency handling [Pinkas and Loui, 1992] [Benferhat et al., 1993]. In CB A0 BF logic, every propositional symbol is interpreted in a weak way, allowing it to be both true and false at the same time, except for the variables of a given set CB that are interpreted classically. Tractability is ensured by limiting the size of CB. Interestingly, CB A0BF entailment proves sufficient to handle some inconsistencies, those that are not reachable when classical inference is limited to the variables of CB. In order to handle the remaining inconsistencies while avoiding trivialization, we introduce a family of inference relations which are to CB A0 BF entailment what the inference relations of the standard coherence-based approach are to classical entailment. Specifically, consistency is restored by removing variables (from CB) instead of removing some explicit beliefs from the belief base. The computational complexity of these inference relations is identified, and some other properties are investigated. Among the strong features of our framework is the fact that tractability is ensured each time a computational bound CYCBCY is set. Moreover, binary connectives behave in a classical manner while it is not the case for many paraconsistent logics. Finally, our framework is general enough to encompass both CB A0 BF logic [Schaerf and Cadoli, 1995], the standard coherence-based approach to inconsistency handling [Pinkas and Loui, 1992] [Benferhat et al., 1993] and some systems for paraconsistent reasoning given in [Priest, 1991] [Besnard and Schaub, 1998] as specific cases.

1 In this approach, beliefs are represented by a belief base BU, i.e., a finite set of propositional formulas; some consistent subbases of BU that are preferred w.r.t. a given selection policy are first selected, then inference amounts to classical inference from some of them [Pinkas and Loui, 1992] [Benferhat et al., 1993].

2 Formal preliminaries

In the following, we consider a propositional language CA CB inductively defined from a finite set CB of propositional symbols, the boolean constants D8D6D9CT and CUCPD0D7CT and the connectives BM, CM, CN. For every formula AU from  CA  CB , CE CPD6B4AUB5 denotes the symbols of CB occurring in AU. As usual, every finite set of formulas is considered as the conjunctive formula whose conjuncts are the elements of the set.

Every formula AU from CA CB is interpreted in a classical way, unless stated otherwise. In order to avoid any ambiguity, we sometimes refer to BE-interpretations, BE-models, BE-consistent and BE-inconsistent formulas instead of the usual notions of (respectively) interpretations, models, consistent formulas and inconsistent formulas.

For the sake of simplicity, we assume that every formula AU of CA CB is in Negation Normal Form (NNF), i.e., only variables are in the scope of any occurrence of BM in AU. For instance, BMCP CN B4CQ CM BMCRB5 is in NNF while the (classically equivalent) formula BMB4CP CM BMB4CQ CM BMCRB5B5 is not. Nevertheless, this assumption could be given up easily (cf. Section 4.4).

We assume the reader familiar with the complexity classes P, A1 D4 BE CJB4D0D3CV D2B5CL, A1 D4 BE , and A5 D4 BE of the polynomial hierarchy (see [Papadimitriou, 1994] for details).

3 CB A0 BF inference

Our family of inference relations is based on CB A0 BF logic [Schaerf and Cadoli, 1995], a multivalued logic which can be viewed as a generalization of Levesque's logic of limited inference [Levesque, 1984]. In CB A0 BF logic, every propositional variable is interpreted in a weak way, allowing it to be both true and false at the same time, except for the variables of a given set CB.

Definition 3.1 Let CB be a subset of CB.

• AF An CBA0BF-interpretation over CB is a mapping
  from the set  CB of all literals over CB to BU BP CUBCBN BDCV s.t. for every literal D0 of  CB , we never have
  B4D0B5 BP
  B4BMD0B5 BP BC, and we always have
  B4D0B5 BP BD A0
  B4BMD0B5 whenever the variable of D0 belongs to CB. D8D6D9CT is always interpreted as BD while CUCPD0D7CT is always interpreted as BC.
• AF An CBA0BF-interpretation
  is an CBA0BF-model of a NNF formula A6 iff the formula obtained by replacing in A6 every occurrence of BMD0 by CUCPD0D7CT (resp. D8D6D9CT) when
  B4BMD0B5 BP BC (resp. BD), then every occurrence of D0 by CUCPD0D7CT (resp. D8D6D9CT) when
  B4D0B5 BP BC (resp. BD) evaluates classically to BD.
• AF Let BU be a belief base (i.e., a conjunctively-interpreted finite set of formulas from CA CB ). Let AD be a formula from CA CB . AD is an CB A0 BF consequence of BU, noted BU CYBP BF CB AD, iff every CBA0BF-model of BU is an B4CBA0BF-) model of AD.

A formula is said to be CB A0 BF consistent when it has an CB A0 BF-model. A BF-interpretation (resp. BF-model) is just an BN A0 BF-interpretation (resp. BN A0 BF-model) and a formula is BF-consistent when it has a BF-model. Every formula from CA CB which does not contain any occurrence of CUCPD0D7CT is BF-consistent (the BF-interpretation
s.t.
B4D0B5 BP BD for every literal D0 of  CB is a BF-model of it).

As shown in [Schaerf and Cadoli, 1995], for every CB AI CB, the corresponding inference relation CYBP BF CB is an approximation of CYBP by below: if BU CYBP BF CB AD then BU CYBP AD.

Interestingly, the limited power of CB A0 BF inference enables some inconsistencies to be handled:

Example 3.1 Let BU BP CUB4BMCP CN CQB5BN CPBN B4BMCR CN CQB5BN B4BMCQ CN CSB5BN B4CR CM BMCSB5BN CTBN B4BMCT CN CUB5CV. BU is (BE-)inconsistent.

• AF Let CB BP CUCRBN CSBN CTCV. We have BU CYBP BF CB CP CM CR CM BMCS CM CQ CM BMCQ CMCT CM CU but BU BICYBP BF CB CS.
• AF Let CB BP CUCQBN CRBN CSBN CTCV. We have BU CYBP BF CB CUCPD0D7CT. Here, BU CYBP BF CB is explosive: any formula is an CB A0BF consequence of BU.

Tractability of CB A0 BF entailment is ensured by limiting the size of CB. To be more specific, the time complexity of CB A0 BF inference is in B4BE CYCBCY BMCYBUCYBMCYADCYB5 when BU is a CNF formula 2

2 Combining both Theorem A.3 from [Schaerf and Cadoli, 1995], Lemma 3.1 and Theorem 4.1 from [Cadoli and Schaerf, 1996], this

and AD is a clause [Schaerf and Cadoli, 1995]. Accordingly, the complexity of CB A0 BF inference depends essentially on the number of variables in CB.

4 Resource-bounded paraconsistent inference 4.1 Dealing with inconsistency

Adhering to CB A0BF entailment is a way to prevent some inconsistencies from being harmful, namely those which are derivable only if classical reasoning over some variables outside CB is performed. In the previous example with CB BP CUCRBN CSBN CTCV, while we have both BU CYBP BF CB CQ and BU CYBP BF CB BMCQ, we do not have BU CYBP BF CB CS.

However, restricting CB to an arbitrary subset of the variables occurring in BU is not sufficient to avoid trivialization in every situation (see the previous example). In order to deal with the remaining inconsistencies, we suggest to focus on some subsets CB BC of CB, those for which the corresponding inference relations are not explosive. The approach is similar to the standard coherence-based approach to inconsistency handling, except that the inference relation is weakened by removing variables from CB instead of removing explicit beliefs from BU. Formally, we first need a notion playing a role similar to the notion of consistent subbase in the standard coherence-based approach.

Definition 4.1 Let BU be a belief base. Let CB AI CB and CB BC AI CB s.t. BU BICYBP BF CB BC CUCPD0D7CT. A consistent subset CB BC of CB w.r.t. BU and CB BC is a subset of CB containing CB BC and s.t. BU BICYBP BF CB BC CUCPD0D7CT. CBB4BUBN CBBN CB BC B5 denotes the set of all consistent subsets of CB w.r.t. BU and CB BC .

In this definition, CB BC is a given set of variables which must be interpreted classically. In our framework, CB BC plays a role similar to the one played by integrity constraints. Requiring the existence of such a set CB BC (possibly empty) imposes that BU is BF-consistent (which is not a strong assumption).

In the following, we adhere to a skeptical approach (every preferred consistent subset is considered):

Definition 4.2 Let BU be a belief base and CB BC be a subset of CB s.t. BU BICYBP BF CB BC CUCPD0D7CT. Let  be a selection policy s.t. CB  B4BUBN CBBN CB BC B5 is a subset of CBB4BUBN CBBN CB BC B5 and let AD be a formula from CA CB . AD is a consequence of BU w.r.t.  and CB BC , noted BU CYAP BNCB BC CB AD, iff BKCB BC BE CB  B4BUBN CBBN CB BC B5, BU CYBP BF CB BC AD.

Now, we can define selection policies for consistent subsets that are similar to the ones defined for consistent subbases in the standard coherence-based approach [Pinkas and Loui, 1992] [Benferhat et al., 1993] [Benferhat et al., 1995].

Definition 4.3 Let BU be a belief base. Let CB BP B4CB BC BN BM BM BM BN CB CY B5 be a stratification 3 of a given subset of CB where CB BC is s.t. BU BICYBP BF CB BC CUCPD0D7CT.

• AF The set CB  B4BUBN CBBN CB BC B5 of all preferred consistent subsets of CB w.r.t. BU and CB BC for the possibilistic policy is the singleton CU CB D7A0BD CXBPBC CB CX CV, where D7 is either the smallest index (BD AK D7 AK CY) s.t. CB D7 CXBPBC CB CX is an inconsistent subset of CB w.r.t. BU and CB BC or CY B7 BD if CB is consistent w.r.t. BU.

result can be easily generalized to the case where BU is any NNF formula and AD is a CNF formula; in this situation, CB A0 BF inference can still be decided in time linear in the size of the belief base. 3 A stratification of CB is a totally ordered partition of it.

• AF The set CB  B4BUBN CBBN CB BC B5 of all preferred consistent subsets of CB w.r.t. BU and CB BC for the linear order policy is the singleton CU CB CY CXBPBC CB BC CX CV, where CB BC CX (CX BE BCBN BM BM BM BN CY) is defined by CB BC CX BP CB CX if CB CX CJ CB CXA0BD D0BPBC CB BC D0 is a consistent subset of CB w.r.t. BU and CB BC , BN otherwise.
• AF The set CB
   B4BUBN CBBN CB BC B5 of all preferred consistent subsets of CB w.r.t. BU and CB BC for the inclusion-preference policy is CUCB BC CY CB BC is a consistent subset of CB w.r.t. BU and CB BC and BKCB BCBC BIBP CB BC s.t. CB BCBC BE CBB4BUBN CBBN CB BC B5, BKCX BE BCBN BM BM BM BN CY B4B4BKD0 BO CXB4CB BC CK CB D0 BP CB BCBC CK CB D0 B5B5 B5 CB BC CK CB CX BIAQ CB BCBC CK CB CX B5CV.
• AF The set CB BX B4BUBN CBBN CB BC B5 of all preferred consistent subsets of CB w.r.t. BU and CB BC for the lexicographic policy is CUCB BC CY CB BC is a consistent subset of CB w.r.t. BU and CB BC and BKCB BCBC BIBP CB BC s.t. CB BCBC BE CBB4BUBN CBBN CB BC B5, BKCX BE BCBN BM BM BM BN CY B4B4BKD0 BO CXB4CYCB BC CK CB D0 CY BP CYCB BCBC CK CB D0 CYB5B5 B5 CYCB BC CK CB CX CY AL CYCB BCBC CK CB CX CYB5CV.

These definitions assume that a stratification of the given set CB of variables is available. Such a stratification is the formal counterpart of the preferential information used to discriminate among consistent subsets.

Here is an example showing the variety of conclusions that can be drawn in our framework (if both a formula AD and its negation are consequences of BU, the truth of AD given BU must be considered as doubtful):

Example 4.1 Let BU BP CUB4BMCP CN CQB5BN CPBN B4BMCR CN CQB5BN B4BMCQ CN CSB5BN B4CR CM BMCSB5BN CTBN B4BMCT CN CU B5CV. With CB BP B4BNBN CUCPBN CQBN CRBN CSBN CTCVB5 or CB BP B4BNBN CUCPCVBN CUCQBN CRBN CSCVBN CUCTCVB5, CP, CR, BMCS and CT are consequences of BU (but their negations are not) whatever  among the four policies considered above. Moreover:

• AF With CB BP B4BNBN CUCPBN CQBN CRBN CSBN CTCVB5:
• w.r.t.  (or ), none of CQ, BMCQ, CU and BMCU are consequences of BU.
• w.r.t.
  , CU is a consequence of BU, but CQ and BMCQ are not.
• w.r.t. BX, CQ and CU are consequences of BU, but their negations are not.
• AF With CB BP B4BNBN CUCPCVBN CUCQBN CRBN CSCVBN CUCTCVB5:
• w.r.t. , CQ is a consequence of BU, but CU and BMCU are not.
• w.r.t. ,
   or BX, CQ and CU are consequences of BU, but their negations are not.

Clearly enough, in the case where BU BICYBP BF CB CUCPD0D7CT, all our inference relations BU CYAP BNCB BC CB coincides with BU CYBP BF CB . Accordingly, CB A0 BF inference can be recovered as a specific case in our framework in this situation.

The next proposition states that one of our basic objectives (avoiding trivialization) is always reached.

Proposition 4.1 None of the relations BU CYAP BNCB BC CB with  among , ,
, BX is explosive.

4.2 Instantiating our framework

There are many ways to define a stratified set CB from a stratified belief base (SBB) BU 4 . First, CB BC can be defined as the set of all variables from the certain beliefs (i.e., pieces of knowledge) of BU when available, provided that such a set is small enough and satisfies BU BICYBP BF CB BC CUCPD0D7CT. Otherwise, CB BC is defined as BN.

4 Upstream to our work are several techniques that aim at deriving a SBB from a "flat" belief base, see [Benferhat, 2000] for a survey.

Defining CB is known as a difficult problem in the general case [Schaerf and Cadoli, 1995]. Interestingly, when BU is a SBB, it is possible to exploit the given preferential information so as to define CB. A very natural way consists in considering in priority the variables of the most plausible beliefs until a preset bound CQ on the size of CB is reached. Formally, we consider the following set of variables CB CQ :

Definition 4.4 Let BU BP B4A1 BD BN BM BM BM BNA1 CZ B5 be a SBB. Let CQ be a positive integer. Let CB BC be a subset of CB s.t. BU BICYBP BF CB BC CUCPD0D7CT and CYCB BC CY AK CQ. The inference level 5 of BU given CQ and CB BC , noted CX CQ BU is the smallest CX (CX BE BCBMBMCZ A0 BD) s.t. CB CQ CX BP CB CQ CXB7BD , where the sequence B4CB CQ CX B5 is inductively defined by CB CQ BC BP CB BC and (BKCX BE BDBN BM BM BM BN CZA0BD) CB CQ CX BP CB CQ CXA0BD CJCE CPD6B4A1 CX B5 if CYCB CQ CXA0BD CJCE CPD6B4A1 CX B5CY AK CQ, CB CQ CX BP CB CQ CXA0BD otherwise. We define CB CQ as CB CQ CX CQ BU .

Finally, once both CB BC and a flat set CB are available, a stratification of CB can be easily derived from the given stratification of BU. Basically, once CB BC has been taken into account, it is reasonable to give more importance to the variables of CB that belong to the more plausible beliefs. Loosely speaking, we want to reason as much as classically as possible from the most plausible beliefs in order to take into account their, possibly conflicting, classical consequences: inconsistencies must not be ignored when supported by plausible beliefs.

Definition 4.5 Let BU BP B4A1 BD BN BM BM BM BNA1 CZ B5 be a SBB, CB a subset of CB and CB BC a subset of CB. The stratification of CB induced by BU given CB BC is CB BP B4CB BC BN BM BM BM BN CB CZB7BD B5 s.t. CB CX BP B4CBCKCE CPD6B4A1 CX B5B5D2 CB CXA0BD D0BPBC CB D0 for every CX BE BDBMBMCZ, and CB CZB7BD BP CB D2 CB CZ D0BPBC CB D0 .

There are many other ways to derive a stratification of CB. For instance, in the situation where we are ready to give more credit to facts than to rules, we can take advantage of the notion of degree of definiteness 6 of a variable (as defined in [Besnard and Schaub, 1998]) to achieve this goal from a CNF belief base BU.

4.3 Logical properties and cautiousness

Some logical properties. As in the standard coherence-based approach, it is easy to give a preferential models semantics to each of our relations CYAP BNCB BC CB . Indeed, BU CYAP BNCB BC CB AD holds iff every preferred B4CB BC A0B5BF-model of BU w.r.t.  is a B4CB BC A0B5BFmodel of AD, where the preferred B4CB BC A0B5BF-models of BU w.r.t.  are exactly the CB BC A0 BF-models of BU with CB BC BE CB  B4BUBN CBBN CB BC B5. Thus, when CB BP B4BNBN CBB5, the preferred BF-models of BU w.r.t.
 are the BF-models of it encoding worlds that are "as normal as possible" (i.e., as close as possible to BE-interpretations).

5 At a first glance, the computation of the inference level of a belief base looks like the computation of the inconsistency level for possibilistic belief bases. However, the former is guided by computational motivations, only; especially, it is not the case that BU BICYBP BF CB CQ CUCPD0D7CT in the general case.

6 Roughly, every variable DC of CB occurring in BU can be associated with the size of one of the smallest clauses of BU containing DC; a stratification of CB is obtained by considering DC before DD whenever the score attached to DC is smaller than the score attached to DD.

Another strong point of our approach is that our inference relations exhibit a limited form of syntax-sensitivity. Indeed, the binary connectives CM and CN of our language behave in a classical manner: the set of CBA0BF models of AUCMAW (resp. AUCNAW) is the intersection (resp. union) of the set of CB A0 BF models of AU and the set of CBA0BF models of AW. As a consequence, given a stratification CB BP B4CB BC BN BM BM BM BN CB CY B5, every formula fromBU (and BU itself!) can be turned into a CNF formula without modifying the corresponding inference relations CYAP BNCB BC CB . The possibility of normalizing the belief base under CNF is particularly important for readibility reasons and the practical computing of the inference relations CYAP BNCB BC CB . Moreover, this valuable property is usually not satisfied by paraconsistent logics (e.g., the one given in [da Costa, 1974], the one given in [Lin, 1987], or the standard coherence-based approach). Contrastingly, like any paraconsistent inference relation, our relations do not satisfy left logical equivalence. For the same reason, they do not satisfy right weakening (since they satisfy reflexivity). Finally, unlike CB A0 BF inference [Schaerf and Cadoli, 1995] , they are not monotonic 7 (neither in CB nor in BU) in the general case.

Example 4.2 Let BU BP CUCPBN B4BMCP CN CQB5BN B4BMCP CN CRB5BN BMCRCV, BU BC BP CUCPBN B4BMCP CN CQB5BN B4BMCP CN CRB5BN BMCRBN BMCPCV, CB BP B4BNBN CUCPCVB5, and CB BC BP B4BNBN CUCPBN CRCVB5. We have BU CYAP
BNCB BC CB CQ but BU BC BI CYAP
BNCB BC CB CQ and BU BI CYAP
BNCB BC CB BC CQ. Similar counter-examples can be easily found for the other policies.

This is not very surprising: while monotonicity is a highly desirable property when BU is consistent, this is not the case otherwise. It is natural that the epistemic status of beliefs changes when more evidence is got through the incorporation of additional explicit beliefs or through an improvement of inferential capabilities. Specifically, increasing the computational effort can lead to discover inconsistencies that were hidden before.

Cautiousness. In the spectrum of inference relations in our framework, one extreme bound corresponds to the case CB BP BN, while at the other extreme bound, we have CB BP CB. None of these two extreme cases can be considered as a "reasonable" inference relation for common-sense reasoning. On the one hand, the latter case corresponds to an ideal agent, with unlimited inferential capabilities: CYBP BF CB coincides with CYBP. Accordingly, if BU is BE-consistent, all our inference relations BU CYAP BNCB BC CB coincide with BU CYBP (admittedly, this contrasts with many paraconsistent inference relations). On the other hand, the former case corresponds to an agent with very limited reasoning capabilities. Indeed, if CB BP BN, all our inference relations correspond to Levesque's BF-entailment [Levesque, 1984]. This inference relation is tractable and avoids trivialization (as long as BU does not contain any occurrence of CUCPD0D7CT). However, with this inference relation, disjunctive syllogism can never be applied: it is not possible to conclude CQ from CP CM B4BMCP CN CQB5. This suggests that cautiousness must be taken into account as an important criterion in the choice of a relation.

7 Nevertheless, we have a "stratumwise" monotonicity property: for  BE CUBN BN
BN BXCV, for every CX BE BCBN BM BM BM BN CY A0 BD, if BU CYAP BNCB BC B4CB BC BNBMBMBMBNCB CX B5 AD, then BU CYAP BNCB BC B4CB BC BNBMBMBMBNCB CXB7BD B5 AD. This property is helpful to check whether BU CYAP BNCB BC CB AD in an incremental fashion.

In the case where CB is a consistent subset, all our inference relations coincide with CYBP BF CB , so they are just as cautious as CYBP BF CB , and the size of CB can be viewed as a degree of cautiousness. In the remaining case, our inference relations are more cautious relations than CYBP BF CB but this is what is expected since trivialization must be avoided. In this situation, our inference relations do not coincide in the general case, and results similar to the corresponding ones in the standard coherence-based approach can be obtained; especially, the less cautious inference relations correspond to the  and BX policies.

Proposition 4.2

• AF CYAP BNCB BC CB is more cautious than CYAP BNCB BC CB and CYAP
  BNCB BC CB , but the converse does not always hold.
• AF CYAP
  BNCB BC CB is more cautious than CYAP BXBNCB BC CB but the converse does not always hold.
• AF CYAP BNCB BC CB cannot be compared with CYAP
  BNCB BC CB and CYAP BXBNCB BC CB w.r.t. cautiousness in the general case.

4.4 A general framework

Our framework is quite general. As evoked previously, it includes CB A0 BF inference as a specific case. As a consequence, it also includes the inference relation CO  of the three-valued logic  8 [Priest, 1989] with CUBDBN BD BE CV as designated truth values, defined by:

Definition 4.6

• AF An  -interpretation
  over CB is a mapping from CB to CCCABXBX BP CUBCBN BD BE BN BDCV.
• AF The semantics of a formula in an -interpretation
  is defined inductively by:
• 
  B4D8D6D9CTB5 BP BD and
  B4CUCPD0D7CTB5 BP BC;
• 
  B4BMAUB5 BP BDA0
  B4AUB5;
• 
  B4AU CMAWB5 BPD1CXD2B4
  B4AUB5BN
  B4AWB5B5;
• 
  B4AU CNAWB5 BPD1CPDCB4
  B4AUB5BN
  B4AWB5B5.
• AF
  is an -model of A6 iff
  B4A6B5 BQ BC.
• AF A6 CO  AD holds iff every -model of A6 is an (-)model of AD.

Indeed, it is not very difficult to prove that CO  coincides with CYBP BF BN . More interestingly, let AK be the preference ordering over -interpretations defined by
AK - iff CUDC BE CB CY
B4DCB5 BP BD BE CV AI CUDC BE CB CY -B4DCB5 BP BD BE CV; then, the relation CO  D1 defined by A6 CO  D1 AD iff every minimal - model of A6 w.r.t. AK is an ( -)model of AD, can be recovered as a specific case of our CYAP
BNCB BC CB relation:

Proposition 4.3 Let A6 and AD be two formulas from CA CB . We have A6 CO  D1 AD iff CUA6CV CYAP
BNBN CB AD.

Our work is also closely related to the approach to paraconsistent reasoning given in [Besnard and Schaub, 1998]. In this work, every formula A6 of CA CB is associated to a default theory CWA6 A6 BN BW CB CX where:

8  is also known as- BF , see [Epstein, 1990].

• AF A6 A6 is a formula in the language CA CB A6 where CB A6 BP CUDC B7 CY DC BE CBCV CJ CUDC A0 CY DC BE CBCV; A6 A6 is obtained by replacing in A6 every occurrence of a positive literal DC by the positive literal DC B7 and every occurrence of a negative literal BMDC by the positive literal DC A0 .
• AF BW CB BP CUÆ DC CY DC BE CBCV is a set of default rules

Among the inference relations that can be defined from CWA6 A6 BNBW CB CX is skeptical signed inference; a formula AD of CA CB is a skeptical signed consequence of A6, noted A6 CO A6 D7 AD iff AD A6 belongs to every extension of CWA6 A6 BN BW  CB CX.

Interestingly, the relation CO A6 D7 can be recovered as a specific case of our CYAP
BNCB BC CB relation.

Proposition 4.4 Let A6 and AD be two formulas from CA CB . We have A6 CO A6 D7 AD iff CUA6CV CYAP
BNBN CB AD.

Finally, our approach encompasses as well the skeptical inference relations CYAO  of the standard coherence-based approach 9 as defined in [Pinkas and Loui, 1992] [Benferhat et al., 1993] [Benferhat et al., 1995].

Proposition 4.5 Let BU BP B4A1 BD BN BM BM BM BN A1 CZ B5 be a SBB. We associate to BU in polynomial time the belief base

BU D2CTDB BP CUD2CTDB CXBNCY BN BMD2CTDB CXBNCY CN AU CXBNCY CY AU CXBNCY BE A1 CX CV and the stratification CB BP

B4CE CPD6B4BUB5BN CUD2CTDB BDBNCY CY AU BDBNCY BE A1 BD CVBN BM BM BM BN CUD2CTDB CZBNCY CY AU CZBNCY BE A1 CZ CVB5 where all the D2CTDB CXBNCY are new variables (not occurring in BU). For every selection policy  among , ,
, BX and every formula AD not containing a new variable, we have BU CYAO  AD iff BU D2CTDB CYAP BNCE CPD6B4BUB5 CB AD.

Focusing on variables instead of beliefs gives less syntaxsensitivity and some flexibility that is hardly achieved by the standard coherence-based approach. For instance, let us assume that BU gathers beliefs stemming from two different sources of information. The first source states CP CM CQ while the second source states BMCP CM BMCQ. The two sources are equally reliable; however, the first source is more reliable to what concerns CQ while the second source is more reliable to what concerns CP. With  BE CU
BN BXCV, the standard coherencebased approach gives B4CUCP CM CQBN BMCP CM BMCQCVB5 CYAO  CP CN BMCQ, but the expected conclusion is just the negation of CP CN BMCQ! Indexing variables with sources, we can express in our framework that CQ from source 1. is more reliable than CP from source 1. and the opposite holds when source 2. is considered. Indeed, with BU BP CUB4BMCP BD CN CPB5 CM B4BMCP CN CP BD B5 CM B4BMCP BE CN CPB5 CM B4BMCP CN CP BE B5 CM B4BMCQ BD CN CQB5CMB4BMCQCNCQ BD B5CMB4BMCQ BE CNCQB5CMB4BMCQCNCQ BE B5CMCP BD CMCQ BD CMBMCP BE CMBMCQ BE CV,  BE CUBN BN
BNBXCV, and CB BP B4CUCPBN CQCVBN CUCQ BD BN CP BE CVBN CUCP BD BN CQ BE CVB5, we have BU CYAP BNCB BC CB BMCPCMCQ and we do not haveBU CYAP BNCB BC CB CPCNBMCQ.

4.5 Dealing with intractability

Despite the generality of our framework, our inference relations are just as hard as the corresponding ones in the standard coherence-based approach when the size of CB is not bounded.

9 A converse polynomial encoding based on A6 transformation exists as well; we omit it here due to space limitations.

Definition 4.7 For every selection policy , CLAUSE CYAP BNCB BC CB is the following decision problem:

• AF Input: A belief base BU, a subset CB of CB, a subset CB BC of CB s.t. BU BICYBP BF CB BC CUCPD0D7CT and a CNF formula AD.
• AF Query: Does BU CYAP BNCB BC CB AD hold ?

LITERAL CYAP BNCB BC CB is the restriction of this problem to the case where AD is a conjunction of literals.

Proposition 4.6 The complexity of CLAUSE CYAP BNCB BC CB and LITERAL CYAP BNCB BC CB is reported in Table 1.

Interestingly, limiting the size of CB is sufficient to ensure tractability. The next proposition shows that our second objective is reached in this case:

Proposition 4.7 The complexity of CLAUSE CYAP BNCB BC CB from a belief base BU given a stratification CB BP B4CB BC BN BM BM BM BN CB CY B5 of a bounded set of propositional variables is in P.

The main reason is that when CYCBCY AK CQ, there is only BE CQ subsets of CB, which is a constant when CQ is a constant. Accordingly, the naive algorithm consisting in generating CB  B4BUBN CBBN CB BC B5 by filtering out the preferred consistent elements of BE CB , and testing for every of the resulting elements CB BC whether or not BU CYBP CB BC AD holds runs in time B4BE BECQ BMCYBUCYBMCYADCYB5, hence in B4CYBUCYBMCYADCYB5 for a constant CQ, for every BU and a CNF query AD.

Of course, this is a "trick" in some sense but we can hardly do better: unless P = NP, there is no tractable inference relation that is general enough to include CYBP as a specific case. In addition, we argue that focusing on BU CYBP BF CB as a tractable approximation of BU CYBP in order to design a paraconsistent inference relation is not so bad, especially when compared with other possible choices. Indeed, let BU CO be a tractable approximation by below of BU CYBP upon which we want to build a tractable paraconsistent inference relation. Requiring that such a tractable paraconsistent relation coincides with BU CO whenever BU CO is not explosive and is obtained by weakening BU CO through the removal of some beliefs of BU otherwise limits the spectrum of interesting relations CO. For instance, considering the restriction BU CO D9D2CXD8 of BU CYBP where only unitrefutation derivable consequences of BU are considered would lead to a complex semantics with respect to which CM and CN do not behave classically [Crawford and Etherington, 1998]; considering the restriction BU D3D6D2 CYBP of BU CYBP where BU D3D6D2 is the subset of Horn clauses of BU would not lead to a tractable relation [Cayrol et al., 1998] [Nebel, 1998].

5 Other related work

A close look at the AI literature shows that both trivialization and intractability can be handled by considering infraclassical inference relations, i.e., approximations by below of BU CYBP.

What is quite surprising is the fact that the two issues have usually not been addressed together.

On the one hand, the proof theory of any paraconsistent logic limits the set of admissible proofs to a strict subset (i.e., an approximation by below) of the classical proofs in the objective of avoiding trivialization. In the standard coherencebased approach, the focus is laid on some preferred consistent subbases of BU, which can be considered as approximations of BU by below. Preferred subbases can also be defined by splitting the belief base BU into several micro-theories characterized by their sets of variables, and selected in a dynamic way by looking at the variables occurring in the queries [Chopra and Parikh, 1999]. Unfortunately, for all these approaches, the corresponding inference relations are typically at least as hard as classical inference in the general case.

On the other hand, many approximation techniques have been developed so far to deal with the intractability issue (e.g., [Levesque, 1984] [Crawford and Kuipers, 1989] [Schaerf and Cadoli, 1995] [Selman and Kautz, 1996] [Dalal, 1996] [Crawford and Etherington, 1998]); in such approaches, the inference relation or the knowledge base itself are approximated into computationally easier one(s). However, the trivialization issue is typically not addressed. For instance, the inference relation defined in [Selman and Kautz, 1996] is always explosive when BU is inconsistent, while the ones given in [Schaerf and Cadoli, 1995] [Crawford and Etherington, 1998] are explosive in the general case when BU is inconsistent.

6 Conclusion

The main contribution of this paper is a family of resourcebounded paraconsistent inference relations. In contrast to many approaches to inconsistency handling, the computational issue is very central in our framework. Especially, the computational resources can be tuned to give rise to realistic, computationally viable, inference relations. Nevertheless, our framework is general enough to encompass CB A0 BF logic, the standard coherence-based approach to inconsistency handling, and some other systems for paraconsistent reasoning as specific cases.

Several additional families of inference relations could be defined in our framework. Analyzing their computational and logical properties is a topic for further research.

Acknowledgements

Many thanks to the reviewers for their helpful comments, and to the R´egion Nord / Pas-de-Calais and the IUT de Lens for their support. Nad`ege Porquet is granted by the R´egion Nord / Pas-de-Calais.