Circumscribing Inconsistency

1 Introduction

The capability of reasoning in the presence of inconsistencies constitutes a major challenge for any intelligent system. This is because in practical settings it is common to have contradic­ tory information. In fact, despite its many appealing features for knowledge representation and reasoning, classical logic falls in the same trap: A single contradiction may wreck an entire reasoning system, since it may allow for deriving any proposition. This comportment is due to the fact that a contra­ diction denies any classical two-valued model, since a propo­ sition must be either true or false. We thus aim at providing a formal reasoning system satisfying the principle of para­ consistency: {a, -.a} If f3 for some a, {3. In other words, given a contradictory set of premises, this should not necessar­ ily lead to concluding all formulas. We address this problem from a semantic point of view. We want to counterbalance the effect of contradictions by providing a third truth-value that accounts for contradictory propositions. As already put for­ ward by [Priest, 1979], this provides us with inconsistency­ tolerating three-valued models. However, this approach turns out to be rather weak in that it invalidates certain classical in­ ferences, even if there is no contradiction. Intuitively, this is because there are too many three-valued models, in particu­ lar those assigning the inconsistency-tolerating truth-value to propositions that are unaffected by contradictions.

*Previously at LERIA, Universite d' Angers, France.

Torsten H. Schaub* Institut ftir Informatik Universitat Potsdam, Postfach 60 15 53 D-14415 Potsdam

Our idea is to focus on those three-valued models that are as similar as possible to two-valued models of the knowledge base. In this way, we somehow hand over the model selec­ tion process to the knowledge base by preferring those mod­ els that assign true to as many items of the knowledge base as possible. As a result, our approach reduces nicely to classical reasoning in the absence of inconsistency. (For the reader fa­ miliar with the work of [Priest, 1989] we note that ours is dif­ ferent from preferring three-valued models having the highest number of classical truth-values, which amounts to approx­ imating two-valued interpretations while somehow discard­ ing the underlying knowledge base.) The syntactic counter­ part of our preferential reasoning process is furnished by an axiom schema, similar to the ones found in circumscription [McCarthy, 1980]. Another salient feature of our approach is driven by the desire to preserve existing proofs even though they may lead to contradictory conclusions. This is because proofs provide evidence for derived conclusions. We accom­ plish this by introducing an implication connective that re­ duces (inside the knowledge base) to classical implication in the absence of inconsistency, while its resulting inferences are conserved under inconsistency.

The paper is organized as follows. Section 2 lays the se­ mantic foundations of our approach; it presents a novel three­ valued logic comprising two special connectives: The afore­ mentioned implication and a truth-value-indicating connec­ tive (used for later axiomatization of the model selection pro­ cess). To a turn, we define our paraconsistent inference rela­ tion by means of a preference relation over the set of models obtained in this logic. Section 3 presents the syntactic coun­ terpart by proposing a corresponding formal proof system. We present an axiomatization of the underlying three-valued logic and we furnish a circumscription axiom providing syntactic means for reasoning from preferred inconsistency-toleratin~ models.

2 Modeltheory

This section presents our semantic approach to reasoning frorr possibly inconsistent knowledge bases expressed in a propo· sitionallanguage. We use 1- for classical entailment wrt two valued interpretations and Cnf- for classical deductive clo sure. For dealing with inconsistencies we rely on an extende(

propositional language:

Definition 2.1 Given a set P of propositional symbols let £ be the set of all formulas generated from P using connectives T, .l , -, , V, A, -+,++, Q, :::;.

The last two connectives serve as truth-value indicators. That is, Qa means that a is true and a :::; {3 signifies that the truth value of a is less than that of {3. This order is proper to this connective and is no intrinsic feature of the rest of the logic. We define T as Qa -+ a and .l by -, T . Also, we define a ++ {3 as (a -+ {3) /1. ({3 -+ a). In fact, :::; is also a defined connective (using Q), whose discussion is deferred to Section 3.

Definition 2.2 An interpretation is a function

v:P-t{t,j,o} extendingto v : £-t{t , j , o} according to the truth tables below.

A model of a formula a is an interpretation that assigns either t oro to a.

Modelhood extends to sets of formulas in the standard way. Observe that /1. and V are de Morgan duals. Also, note that the truth-value of a -+ {3 differs from that of -,a V {3 only in the case of v = {a : o, {3 : !} resulting in v( a -+ {3) = f and v( -,a V {3) = o. This difference is prompted by the fact that t and o indicate modelhood, which motivates the assignment of the same truth-values to a-+ {3 no matter whether we have a : t or a : o. This has actually to do with the difference between modus ponens (MP) and disjunctive syllogism (DS):

The latter yields B from A /1. -,A /1. -,B because A V B follows from A. The overall inference seems wrong because in the presence of A /1. -,A, A V B is satisfied (by A : o) with no need for B to be t . This is why we center our approach upon modus ponens.

We then obtain the following consequence relation:

Definition 2.3 Let r be a set of formulas and 'Y a formula. We definer If- 'Y iff each model ofr is a model of "f.

The reader is warned that replacement of equivalents fails: Let 'Y[¢1, ... , cf>k] be the formula obtained from 7[1/J1, ... , 1/Jk] by replacing all occurrences of 1/J1, ... , 1/Jk by c/>1, ... , cf>k. Then,

Letting a be A -+ -,-,A, {3 be B -+ -,-,B, and 'Y be -,'ljJ shows the failure of replacement of equivalents: If- (A -+ -,-,A) ++ (B-+ -,-,B) but l,)l. -,(A -+ -,-,A) ++ -,(B -+ -,-,B).

We now turn to the key definition of our approach:

Definition 2.4 Let v and v' be two interpretations and r a set of formulas. We define

Observe that -<r is a strict partial order on interpretations. Hence, we can speak of minimal models for a set of formu­ las r. This leads us to the following paraconsistent inference relation:

Definition 2.5 Let r be a set of formulas and 'Y a formula. We definer llf- 'Y iff each -<r-minimal model ofr is a model of 'Y·

Definition 2.4 and 2.5 show that we focus on models of r that assign t (instead of o) to a maximal subset of r. Since o accounts for inconsistency all this amounts to minimizing in­ consistency. In fact, both aforementioned inference relations are paraconsistent: {A, -,A} l,ll B and {A, -,A} l}f- B.

Since we aim at modeling reasoning from knowledge bases expressed in a propositional language, we impose the follow­ ing restriction: As modus ponens is a fairly uncontroversial reasoning mode, we take it as a basis for our approach. In par­ ticular, premises are required to be in conditional form prone to application of modus ponens:

Definition 2.6 Let P be a set of propositional symbols and £ ..... the set of all expressions of the form

where LiE {a, -,a I a E P} fori= l..n andO:::; m < n.

We refer to expressions in £ ..... as clauses. For m = 0, such clauses reduce to £ 1 V . . . V Ln. As a whole,£ ..... is generated from P using connectives-,, V, 11., -+.

Consider the set of formulas

We obtain r llf- -,A. In fact, -,A is concluded for the reason that, if A were true then there would be a contradiction about B. So, when it really is the case that there is a contradiction about B, the reason for -,A to be concluded no longer applies. That is, we have ru {A} l}f--,A and ru {A} llf- All. B /1. -,B. Observe that this example violates unrestricted monotonicity (the relative theories must be both consistent or both inconsis­ tent; cf. Theorem 2.2). This comportment can be verified in Table 1. An entry like o/2 in column r means that interpretation v, given in the first two rows, assigns o to (the conjunction of) r, while lh E r I v(1) = o}l = 2. Such a number is however just an indication and should not be confused with the actual ordering relation on models which is based on set inclusion! A preferred model is indicated by boldface type­ setting.

For a complement, take a look at clause set

We haver' U {A} \,If- ·B 1\ B. We only haver' U {A} 1\f­ BV·B. This illustrates the difference between an implication, like A -+ B and a disjunction, like ·A V B. Unlike the latter, connective-+ allows us to construct a proof for B 1\ ·B from r U {A}. Compare this with the case of all contrapositives:

This yields r" U {A} \If- A 1\ ·A 1\ ·B 1\ B.

The previous examples have illustrated that whenever there are two-valued models, they are the only relevant minimal models. That is, in case of a 3-valued model v assigning t, we find also all 2-valued models obtained by substituting o in v by t and f , respectively. Hence, such 3-valued models are irrelevant. See columns r , r', r" in Table 1. In fact, we have the following result showing that our mechanism amounts to classical (two-valued) logic, whenever we deal with a classi­ cally consistent theory.

Theorem 2.1 Let r be a classically consistent set of clauses and 1 a formula whose connectives are among ·, 1\ , V. Then,

This result does not extend to the underlying inference relation If- . A counterexample is simply r as in (1) and 1 be­ ing ·A. Also, this theorem does not extend to conclusions containing -+, eg. \,If- ( ·A V B) -+ (A -+ B) although (·A VB) -+ (A-+ B) is a classical tautology. Theorem 2.1 is neither expected to carry over to the case where r is incon­ sistent.

A salient property of our approach is that it is monotonic on inconsistent premises:

Theorem 2.2 For sets of clauses r and~. we have

whenever r \If- a 1\ ·a and 'vT' ~ r. r' \,If- a 1\ ·a.

We now need a few definitions on restricted alphabets:

For an alphabet P x, let .Cx denote the language generated from P x using ·, V, 1\, -+, ++. Then, we have the following result showing that truthful parts of the knowledge base are closed under classical logic:

Theorem 2.3 For all sets of clauses r and ~ such that ~ = {a 1 r llf- qa}, we have

Moreover, we can show that truthful parts are never polluted by contradictions:

Theorem 2.4 Let r = r 1 U r 2 be a clause set such that P1 n P2 = 0 where Pi is the set of propositional symbols occurring in r i. We have for each a E .C1.

whenever r \If- Qr for each 1 E r 1·

As illustrated below, the last theorem extends in some cases to non-disjoint parts, as witnessed by r 1' r~ ' q- below.

For further illustration, consider first the set of clauses

Indeed ro has a single two-valued model {A : / , B : t , C : t} (apart from 9 three-valued ones assigning 0 to ro). The former is clearly the only minimal model of r o. We thus have

Adding A to r 0 yields inconsistent theory r~ = {A, ·A, B, ( ·B V C)} having only three-valued models left. In fact, all former models of ro with A : f do now falsify r~. All remaining models of r 0 assign thus o to r~ and A, the ac­ tual heart of the contradiction. Among the resulting models, we have a single minimal model, {A : o, B : t , C : t}, giving r~ \If- A 1\ ·A 1\ B 1\ C by "applying" disjunctive syllogism to the consistent part of r~.

Next, consider the set of clauses

This theory induces the truth-values given in Table 2. Among

the three models of r 1 , there is only one minimal one: {A : o, B : t}. As a consequence, we obtain

For those familiar with [Priest, 1989], we note that this ap­ proach has {A : o, B : !} as a second preferred model, which denies conclusion B. See Section 4 for details. The example illustrates further the aforementioned extendibility of Theo­ rem 2.4: Despite the inconsistency of A, we derive B from the consistent premises A and ·A V B.

Actually, things do not necessarily change by orienting the above disjunctions as implications:

r( and q- have the same minimal model as r 1; thus offer­ ing the same conclusions. However, while q- has the same models as r 1 , interpretation {A : o, B : !} falsifies f(.

Adding clause A v ...,B to Theory r 1 yields

r~ has two minimal models, both of which were models of f 1, yet only one of them was r 1 -preferred. We thus get

illustrating that inferences by disjunctive syllogism are notal­ ways preserved.

For a complement, consider rule sets

From these, we obtain after consulting Table 2:

The derivability of B and -,B illustrates the role of connec­ tive -+ as proof-provider: All proofs obtained from clauses by modus ponens are set in stone. This general property is reflected by the validity of II- (a 1\ (a -+ /3)) -+ /3.

3 Prooftheory

This section presents a formal proof system for our approach to circumscribing inconsistency. In analogy to the semantics, we first axiomatize II- and then we account for minimization by providing a syntactic axiom schema, so that the resulting system axiomatizes Ill-. ·

The axiomatization of II- consists of modus ponens as infer­ ence rule and the following axiom schemas:

• a -+ a V /3, a -+ f3 V a (3)

• a .H ...,...,a (7)
• -,(a V /3) +-+ -,a 1\ ....,13 (8)
• -,(a 1\ /3) +-+ -,a V ...,13 (9)

• qa-+ qqa (15)

• -,qa +-+ q-,qa (17)
• q(a 1\ /3) +-+ qa 1\ q/3 (18)
• q(a V /3) +-+ qa V Q/3 (19)

• -,a -+ q(a -+ /3) (21)

As can be shown, this proof system is sound and complete for 11-. We write')' E Cn11-(f) to indicate that -y can be derived from r by the above proof system.

Semantically, the move from II- to Ill- amounts to minimiz­ ing the set of premises with truth-value o. That is, we prefer models that assign truth-value o to a minimal set of premises. We can turn this idea into the syntax by using a connective indicating that a formula has a truth value which is less than the one of another formula. As anticipated in Section 2, such a connective can be defined as follows:

This induces the following truth table corresponding to the poset of truth-values on the right hand side.

I\

f

With this connective, we are now ready to express the follow­ ing circumscription schema providing a syntactic account for preferring -<r-minimal models. For readability, we identify in the next definition clause set { ')'1, ... , 'Yn} with /\~= 1 'Yi·

Definition 3.1 Let r = {1'1, . .. , 'Yn} be a finite set of formu­ las over alphabet P1 , ... , Pk (abbreviated P) so that 'Yi = -yi[P] and r = r[P]. We define the three-valued paraconsis­ tent circumscription schema Circ3 P(f) as

Importantly, combining Circ3 P(f) with the proof system for II- captures the desired paraconsistent inference relation Ill- :

Theorem 3.1 Let r be a set of clauses. Then, we have

o

For illustration, let us return to our initial example

We consider the following instance of CircsP(f) where ¢A = . ..l and ¢ B = B:

From r, we obtain the right hand side (RHS) of CircsP(f), that is, (A -t B ::; ..l -t B) and (A -t ·B ::; ..l -t ·B) after establishing the LHS by means of theorem (a 1\ ((3 ::; T)) -t ((3 ::; a). By applying transitivity of ::; to RHS and (..l -t B) ::; T and (..l -t ·B) ::; T, we then get (A -t B) ::; T and (A -t ·B) ::; T . So, we get (·A ::; T) V ( ( ·B 1\ B) ::; T) yielding ·A ::; T, hence ·A. Notably, it is the circumscription schema that reduces the three-valued consequence relation !If- to its classical two-valued counterpart f- ( cf. Theorem 2.1 ).

For further illustration, consider r U {A} along with the instance of Circ3 P (r U {A}) obtained by taking ¢A = T and ¢ B = B 1\ ·B. We obtain A ::; T and so A using theorem (a 1\ ('y ::; (3)) -t ('y ::; (a -t (3)). Of course, not every !If­ conclusion necessitates the circumscription schema in order to be derived. For instance, B and ·B are directly derived by modus ponens from r u {A}.

4 Related work

There are a number of proposals addressing inconsistent in­ formation. At first, there is the wide range of paraconsistent logics [Priest et al., 1989]. As opposed to our approach, such logics usually fail to identify with classical logic when the set of premises is consistent. There are also many approaches dealing with classical reasoning from consistent subsets. In a broader sense, this includes also belief revision and truth maintenance systems. A comparative study of the aforemen­ tioned approaches in general is given in [Besnard, 1991].

A system, at first sight closely related to ours, is LP m [Priest, 1989]; it was conceived to overcome the failure of disjunctive syllogism in LP [Priest, 1979]. LP amounts to the 3-valued logic obtained by restricting If- to connectives ·, V and 1\ and defining a -t (3 as ·a V (3. In LPm model­ hood is then limited to models containing a minimal number of propositional variables being assigned o. As our approach, this allows for drawing "all classical inferences except where inconsistency makes them doubtful anyway" [Priest, 1989]. There are two major differences though: First, the aforemen­ tioned restriction of modelhood focuses on models as close as possible to 2-valued interpretations, while the one in our approach aims at models next to 2-valued models of the con­ sidered formula. The effects of making the formula select its preferred models can be seen by looking at r 1: While LP m yields two preferred models {A : o, B : t} and {A : o, B : !}

from which one obtains AI\ ·A, r 1 makes our approach prefer the former over the latter, thus yielding B as additional con­ clusion. Second, we have introduced implication as a primi­ tive connective rather than a defined one. As a consequence, a modus ponens inference, like deriving B from A and A -t B, is preserved no matter what other premises are given; this fails in LPm. Note that we get distinct truth-tables (and so different conclusions) for r~ and its variants r~=~, ... , while LPm does not differentiate these variations. A resolution-based system close to LP yet with a stronger disjunction is described in [Lin, 1987].

A whole variety of approaches uses lattices for dealing with inconsistency, eg. [Arieli and Avron, 1994; Belnap, 1977; Sandewall, 1985]. For instance, [Arieli and Avron, 1994; 1996] describes a system based on 4-valued logic that allows for constraining "the most consistent" models in the meta­ level by a user-given set of propositions taking classical truth­ values only. [Carnielli et al., 1991] proposes a translation­ based approach to reasoning in the presence of contradictions that translates a logic into a family of other logics, eg. classical logic into 3-valued logics.

The difference between our approach and "reasoning from maximal consistent subsets · of the premises" is that we still pay attention to one objection motivating relevant logics [An­ derson and Belnap, 1975] and that is applying disjunctive syl­ logism to contradictory premises. However, we do not go as far as sanctioning any classical inference not using inconsis­ tent subformulas. That is, we still follow the principle of rel­ evant logics that an inference rule is a priori applicable to any premise. This is in contrast with the idea of restricted access logic [Gabbay and Hunter, 1993], where all classical inference rules are admitted with some special application conditions.

Among others, logic programming with inconsistencies was addressed in [Blair and Subrahmanian, 1988; 1989]. [Wagner, 1991] describes a procedural framework for han­ dling contradictions that relies on the notions of "support" and "acceptance". The former avenue of research is further devel­ oped in [Grant and Subrahmanian, 1995], where it is shown how the approach of [Blair and Subrahmanian, 1988] can be extended by classical inferences, like reasoning by cases. In­ tuitively, the corresponding entailment relations amount to logic programming in a 3-valued (and 4-valued, respectively) logic. The major difference to our approach is that compared to classical entailment, these approaches are sound but not complete (even when the set of premises is consistent). As with other approaches, this is because they aim at paraconsis­ tent reasoning in a logic programming setting that does not necessarily coincide with classical logic.

Our approach is clearly semantical in contrast to many other proposals to paraconsistency: (i) the idea of "forget­ ting" literals [Kifer and Lozinskii, 1989; Besnard and Schaub, 1996]; (ii) the idea of stratified theories [Benferhat et al., 1993]; (iii) the idea of reliability relation [Roos, 1992], (iv) and more generally the idea of reasoning from consistent subsets of the premises. In contrast to [Turner, 1990], where the baseline is to analyze propositions (so as to resolve paradoxes about truth, for instance), we simply apply a system of truth­ values so that we can have non-trivial inconsistent premises. Moreover, our approach is purely deductive, as opposed to argumentation-based frameworks, like [Wagner, 1991; Elvang and Hunter, 1995]. An unusual approach to reasoning from in­ consistency is due to [Lin, 1996], who introduces the notion of consistent belief by means of modal operators. This approach fails to satisfy reflexivity (not every premise is concluded).

5 Conclusion

We presented a semantical approach to dealing with incon­ sistent knowledge bases that is founded on the minimization of three-valued models. This was complemented by a formal proof system accomplishing model minimization by appeal to a circumscription axiom. The distinguishing features of our approach are (i) its desire to provide models making true (in­ stead of true and false) as many as possible items of the knowl­ edge base, (ii) its centering on inferences drawn by modus po­ nens by means of a primitive implication connective, and (iii) its property of restricted monotonicity. A major further devel­ opment will be lifting the approach to the first-order case. In this context, we draw the reader's attention to the fact that our approach (unlike [Priest, 1989]) does not rely on the notion of an atomic proposition, which is always problematic when passing from the propositional case to the first-order case.