Signed systems for paraconsistent reasoning

Journal of Automated Reasoning 20: 191–213, 1998. c 1998 Kluwer Academic Publishers. Printed in the Netherlands.

191

Signed Systems for Paraconsistent Reasoning PH. BESNARD1 and T. SCHAUB2 1

IRISA, Campus de Beaulieu, F-35042 Rennes Cedex LERIA, Facult´e des Sciences, Universit´e d’Angers, 2 boulevard Lavoisier, F-49045 Angers Cedex 01

2

(Received: September 1996) Abstract. We present a novel approach to paraconsistent reasoning, that is, to reasoning from inconsistent information. The basic idea is the following. We transform an inconsistent theory into a consistent one by renaming all literals occurring in the theory. Then, we restore some of the original contents of the theory by introducing progressively formal equivalences linking the original literals to their renamings. This is done as long as consistency is preserved. The restoration of the original contents of the theory is done by appeal to default logic. The overall approach provides us with a family of paraconsistent consequence relations. Our approach is semantical because it works at the level of the propositions; it deals with the semantical link between a proposition and its negation. The approach is therefore independent of the combination of the connectives that are actually applied to the propositions in order to form entire formulas. Key words: paraconsistent reasoning, inconsistent information, knowledge representation, semantics.

1. Introduction Although our knowledge often contains contradictions, they do not make our reasoning capabilities collapse. Rather, we are able to exploit various parts of our knowledge by ignoring inconsistencies. In fact, we can make sense of premises involving contradictions, so as to draw interesting conclusions. As an illustration, consider a theory containing the four following statements: A, ¬A, B, (¬B ∨ C).

(1)

This theory is inconsistent because of the presence of A and ¬A. If we were to apply classical reasoning, we could deduce any proposition like ¬C or D from it. We clearly do not wish to obtain all those conclusions. But what are the reasonable conclusions we still would like to obtain? We are close to answering this question when we observe that any contradiction is rooted in the derivability of a formula and its negation. Given a set of contradictory premises, we should thus identify those contradictions ϕ ∧ ¬ϕ whose derivation does not rely on any other contradictions. We refer to such contradictions as being genuine. Accordingly, we are interested in formulas whose derivation uses no literals from genuine contradictions. In our example, A ∧ ¬A

VTEX (J¯ u) PIPS No.: 146982 MATHKAP JARS9707.tex; 7/11/1997; 14:51; v.7; p.1

192

PH. BESNARD AND T. SCHAUB

is the only genuine contradiction. C is thus a desired conclusion because it comes from B and ¬B∨C , while ¬C is not desirable conclusion because it is obtainable only by using both A and ¬A. The formal counterpart of the general phenomenon is given by the principle of paraconsistency, which can be stated as follows: {ϕ, ¬ϕ} 6` φ for some ϕ, φ. In other words, given a contradictory set of premises, this should not necessarily lead to concluding all formulas. In fact, we aim at proposing a simple approach to paraconsistent reasoning based on the following intuitive idea: Classical reasoning from inconsistent theories becomes somehow polluted by genuine contradictions. As a matter of fact, we aim at removing these contradictions from the premises initiating the reasoning process. We accomplish this aim by destroying the semantical link between a formula and its denial provided that they are involved in a genuine contradiction (thereby achieving paraconsistent inferences while reasoning under the rules of classical logic). Technically, we first transform an inconsistent theory into a consistent one by renaming all literals occurring in the theory. The renamings indicate what renamed literals were denials of each other—making explicit whether the renamed literal were ‘positive’ or ‘negative’. Then, we restore some of the original contents of the theory by progressively introducing formal equivalences linking the original literals to their renamings. We do this up to the point where introducing any further equivalence would reinstate inconsistency. The above example would be now written as A+ , A− , B + , (B − ∨ C + ).

Now, we can apply classical logic to reason from this ‘signed’ theory extended with increasingly many equivalences of the form α+ ↔ ¬α− (actually, the equivalences we use are slightly different because we deal at once with the signed and unsigned language). Then, a later interpretation of the signed formulas gets us back to the original language, classical inferences having thus been turned into seemingly paraconsistent inferences. 2. Formal Preliminaries We deal with propositional languages and use the logical symbols ¬, ∨, ∧, →, ↔ to construct formulas in the standard way. We write LΣ to denote a language over an alphabet Σ. The elements of Σ are called propositional letters, or simply propositions. The technical means we use to extend a signed theory by equivalences relating renamed literals to their renamings is default logic [25]. The central concepts in default logic are default rules along with their induced extensions of an initial set of premises. Default logic augments classical logic by default rules that differ from standard inference rules in sanctioning inferences that rely upon prov-

JARS9707.tex; 7/11/1997; 14:51; v.7; p.2

193

SIGNED SYSTEMS FOR PARACONSISTENT REASONING

able as well as consistent premises. Hence, a default rule αγ: β has two types of antecedents: a prerequisite α, which is established if α is derivable, and a justification β , which is established if β is consistent. If both conditions hold, the consequent γ is concluded by default. A default theory, is a pair (D, W ) where D is a set of default rules and W a set of formulas. A set of conclusions (sanctioned by a given set of default rules and by means of classical logic) is called an extension of an initial set of facts. The formal definition of an extension is as follows [25]. DEFINITION 2.1. Let (D, W ) be a default theory, and let E be a set of formulas. Define E1 = W and for n > 1 En+1

  α : β = Th(En ) ∪ γ ∈ D, α ∈ En , ¬β 6∈ E . γ

Then, E is an extension for (D, W ) if E =

S n∈ω

En .

As another formal matter, we write Th for the classical consequence operator and ω for the positive natural numbers in order to avoid a starred notation. Intuitively, a default rule is applicable when its prerequisite is in En and its justification is consistent with E (in general, the context makes it clear what En and E are). Consequently, the above definition is not strictly iterative as a procedure, since E appears in the specification of En+1 . On the whole, a default theory plays the role of a set of premises, and an extension plays the role of a set of consequences for that default theory. A major feature of default logic is that, on the one hand, not all default theories have extensions and, on the other hand, default theories exist that have more than one extension (even infinitely many in some cases where infinitely many default rules are given). 3. Description of the Basic Method We start with a finite set of formulas (a finite theory) W in a language LΣ . We are primarily interested in inconsistent theories. However, we do not impose a corresponding condition because our approach also applies to consistent theories, for which it nicely reduces to classical logic (cf. Theorem 3.2). As motivated in the introductory section, our approach relies on the restoration of semantic links between complementary literals from their renamings: Given a theory W , we proceed as follows. First, we transform theory W into a negation normal form (NNF). (This is a matter of convenience only; we show at the end of this section how the approach works without this transformation.) Following [15], formulas in NNF are defined as follows: – For every α ∈ Σ, α and ¬α are in NNF; – If φ and ϕ are in NNF, then (φ ∨ ϕ) and (φ ∧ ϕ) are in NNF.

JARS9707.tex; 7/11/1997; 14:51; v.7; p.3

194

PH. BESNARD AND T. SCHAUB

As shown in [15], every formula is equivalent to a formula in NNF. In this way, W is transformed into NNF. It is worth noticing that this transformation does not affect the logical contents of the original theory. Next, we rename the propositions in W as follows. Let ϕ be a formula in NNF in language LΣ . Then, we define ϕ± as the formula obtained from ϕ by replacing each occurrence of ¬α by α− and by replacing all remaining occurrences of α by α+ , for each propositional letter α in Σ. Accordingly, ϕ± is a formula in the new language LΣ± over alphabet Σ± = + {α , α− | α ∈ Σ} obtained from Σ by replacing each propositional letter α by α+ and its negation by α− . In this way, we turn the initial theory W into the consistent theory W ± in language LΣ± . This is so because each formula ϕ of W is substituted by a formula ϕ± that is always a positive formula.? Finally, we consider the default theory obtained from W ± and a set of default rules DΣ = {δα | α ∈ Σ} defined in the following way. For each propositional letter α in Σ, we define δα =

: α+ ↔ ¬α− . (α ↔ α+ ) ∧ (¬α ↔ α− )

(2)

For convenience, we denote the justification of δα by Justif (δα ) and its consequent by Conseq (δα ). Intuitively, such default rules provide means for closing the gap from W ± back to W again. That is, by checking whether the justification α+ ↔ ¬α− is consistent, we test whether we can reintroduce the ‘law of (non)contradiction’ for the proposition α without obtaining an inconsistent theory. If this is the case, we ‘restore’ the original meaning of propositions α+ and α− by adding equivalences (α ↔ α+ ) and (¬α ↔ α− ). Considering in turn each propositional letter α, we are thus gradually restoring the original contents of the theory – except that we stop at the borderline of inconsistency by leaving blank all propositions involved in genuine contradictions. Consider the theory {A, ¬A, B, (B → C)}.

(3)

This theory has the NNF given in (1), namely, {A, ¬A, B, (¬B ∨ C)} . Next, we rewrite this set of clauses into the consistent theory {A+ , A− , B + , (B − ∨ C + )}

(4)

by substituting ¬A, ¬B by A− , B − and A, B, C by A+ , B + , C + , respectively. In turn, we add for each propositional letter α occurring in the original theory a default rule of the form δα as defined in (2). This process yields three default In fact, W ± contains only positive literals apart from conjunctive and disjunctive connectives, ∧ and ∨. ?

JARS9707.tex; 7/11/1997; 14:51; v.7; p.4

195

SIGNED SYSTEMS FOR PARACONSISTENT REASONING

rules δA , δB , and δC , since the original theory is built from the propositional letters A, B, and C . In full detail, δA , δB , δC have the following form : A+ ↔ ¬A− , (A ↔ A+ ) ∧ (¬A ↔ A− )

: B + ↔ ¬B − , (B ↔ B + ) ∧ (¬B ↔ B − )

: C + ↔ ¬C − . (C ↔ C + ) ∧ (¬C ↔ C − ) Consider the default theory obtained from theory (4) along with the three latter default rules.


{δA , δB , δC }, {A+ , A− , B + , (B − ∨ C + )} .

(5)

Clearly, the first default rule is inapplicable, since its justification A+ ↔ ¬A− is inconsistent in the presence of A+ and A− . In contrast, the second and the third default rule are applicable and consequently restore the original meaning of B + , B − , C + , C − .? Accordingly, we obtain a single extension containing the propositions B and C (from the alphabet of our inconsistent initial theory) along with A− , A+ , B + , C + . The following result?? tells us that we always have at least one extension (of (DΣ , W ± )) to look at when it comes to extracting the paraconsistent conclusions of the initial theory (W ). COROLLARY 3.1 (Existence of extensions). Let W be a set of formulas in LΣ . Then, there exists at least one extension of default theory (DΣ , W ± ). For coherence, the formal elaboration of the underlying default logic machinery is given in Appendix A. At this stage, several policies are adaptable for deciding whether a particular formula is a (paraconsistent) conclusion of a possibly inconsistent theory W . Indeed, the crux of our method is to exploit the extension(s) of default theories of the form (DΣ , W ± ) in order to determine what formulas in language LΣ follow as conclusions from the original theory W . Anyway, the next theorem shows that our approach reduces nicely to classical logic in case of consistent theories: THEOREM 3.2. Let W be a consistent set of formulas in LΣ . Then, default theory (DΣ , W ± ) has a unique extension E . Moreover, Th(W ) = E ∩ LΣ . As mentioned above, our exposition relies on NNF for convenience only. This is because NNF allows for an easy distinction and localization of positive and ? Notice that the contribution of a default rule like δC to the theory formation process is in no way sufficient for deriving C, even though it is a necessary condition. Applying δC merely reestablishes the original meaning of C and ¬C from C + and C − , respectively. In our example, C is derived from B and ¬B ∨ C as a result of the preceding restoration of B and C. ?? This result is a corollary to Theorem A.3.

JARS9707.tex; 7/11/1997; 14:51; v.7; p.5

196

PH. BESNARD AND T. SCHAUB

negative occurrences of literals, since negation is attached to atoms only. In the general case, we need the notion of polarity, as defined for instance in [21]: For (arbitrary) formulas ϕ, φ, and ψ, define – the occurrence of ϕ in ϕ is positive, – if ϕ is a positive (negative) occurrence in φ, then ϕ is a negative (positive) occurrence in ¬φ and φ → ψ, – if ϕ is a positive (negative) occurrence in φ, then ϕ is a positive (negative) occurrence in φ ∨ ψ, φ ∧ ψ, ψ → φ. Then, we rename the propositions in a set of formulas W as follows. Let ϕ be an (arbitrary) formula in language LΣ . We define ϕ± as the formula obtained from ϕ by replacing each negative occurrence of α by ¬α− and by replacing each positive occurrences of α by α+ , for each propositional letter α in Σ. For example (A ∧ (A → B))± = A+ ∧ (¬A− → B + ). 4. Paraconsistent Consequence Relations A basic principle that we have followed in the preceding section is to identify the literals in which a contradiction is rooted and eliminate the contradiction by ‘forgetting’ these literals while reasoning. That is, whenever α+ ↔ α− is inferred, then a contradiction is detected that involves α, and (α+ ↔ α)∧(α− ↔ ¬α) is not added to the premises. In this way, neither α nor ¬α is used to infer any conclusion – not even α and ¬α themselves. Of course, sometimes more than one pair of literals is responsible for inconsistency, and ‘forgetting’ just any one pair is enough to restore consistency. In such a case, we have the choice of which pair is to be discarded for inference. Technically, this means that we have more than one extension. In the first place, it seems safe to consider as conclusions the common parts of the extensions at hand. By making sense of ‘common parts’ as set intersection, we get two alternative definitions for paraconsistent inference: DEFINITION 4.1. Let W be a finite set of formulas in LΣ and ϕ be a formula in LΣ . Let E be the set of all extensions of (DΣ , W ± ). For a set of formulas S in LΣ∪Σ± , let ΠS = {Conseq (δα ) | α ∈ Σ, ¬Justif (δα ) 6∈ S}.

Then, we define

T




W `p ϕ iff ϕ ∈ Th W ± ∪ E∈E ΠE
T W `s ϕ iff ϕ ∈ E∈E Th W ± ∪ ΠE

(prudent unsigned? consequence), (skeptical unsigned consequence).

The term ‘unsigned’ indicates that only unsigned formulas in Th W ± ∪ ∩ ΠE
∩ Th W ± ∪ ΠE , respectively, are taken into account. ?




and

JARS9707.tex; 7/11/1997; 14:51; v.7; p.6

197

SIGNED SYSTEMS FOR PARACONSISTENT REASONING

The following example shows that the two inference relations are not the same. Consider the following theory. W = {A, B, ¬C, ¬A ∨ ¬B, A → D, B → D}.

(6)

In order to obtain the above paraconsistent consequence relations, this theory is turned into the following default theory, (DΣ , W ± ),


{δA , δB , δC , δD }, {A+ , B + , C − , A− ∨ B − , A− ∨ D+ , B − ∨ D+ } .



We obtain two extensions, first Th W ± ∪ Conseq {δA , δC , δD , which contains among others A,
¬C, D, and B − in addition to W ± , and second Th(W ± ∪ − W ± . As a Conseq {δB , δC , δD }) , containing
B, ¬C, D and A apart from ± result, relation `p yields Th {¬C} , that is {ϕ ∈ LΣ | ϕ ∈ Th(W ∪Conseq({δC , δD ))}, as the set of prudent conclusions of W , while
relation `s for skeptical unsigned consequence yields Th {¬C, A ∨ B, D} . The two consequence relations `p and `s share some noticeable features, though. For instance, the example indicates that reflexivity holds for neither of the two relations (reflexivity is the property that any premise is also a conclusion). Indeed, we have W 6`p A and W 6`s A, even though A ∈ W. Despite this, the two relations exhibit the property of closure under classical deduction. This is to say that the set {ϕ | W `p ϕ} is always deductively closed. In symbols, {ϕ | W `p ϕ} = Th(X ) where X = W whenever W is consistent and X 6= W whenever W is inconsistent. Of course, the same holds for the second relation, `s . Interestingly, `p captures the notion of free-consequences introduced in [4]. The principle underlying a number of paraconsistent logics [24] is to keep all premises and reason unrestrictedly from them, but keep only some of the inference rules of classical logic. By contrast, we keep all inference rules and apply them as unrestrictedly as in classical logic, but we keep only part of the premises. Importantly, the word ‘part’ is not used here in the set-theoretic sense as done by [20, 27] and their followers. This would coincide with the approach known as ‘reasoning from maximal consistent subsets of the premises’, which is a syntactical approach as opposed to our approach that employs a more semantical device to delineate “parts’ of the premises. Our approach is semantical because it works at the level of the propositions; it deals with the semantical link between a proposition and its negation. Our approach is therefore independent of the combination of the connectives that are actually applied to the propositions in order to form entire formulas. As a simple example, consider the theory {¬A ∧ (B → C), A ∧ B}. This theory comprises two separate maximal consistent subsets corresponding to the two formulas, none of them combining the consistent subformulas B → C and B . Hence C is not derivable in such a syntax-dependent approach. In contrast to this, our approach recognizes B → C and B as a consistent part of the premises. For a complement, consider the CNF set W = {A, ¬A} and the one obtained by substituting A ∨ B and A ∨ ¬B for the logically equivalent formula A; this yields W 0 = {A ∨ B, A ∨ ¬B, ¬A}.

JARS9707.tex; 7/11/1997; 14:51; v.7; p.7

198

PH. BESNARD AND T. SCHAUB

Reasoning from maximal consistent subsets may give different results depending on whether we reason from W or W 0 . In the first case, one obtains {A} and {¬A} as the maximal consistent sets, while W 0 yields {A}, {¬A, ¬B}, and {¬A, B}. Our approach suffers from no such defect: Again, it does not depend on the syntactical form of consistent formulas. (We draw the reader’s attention to the fact that this behavior of our approach is independent of using formulas in NNF.) Up to now, we have taken a safe approach to drawing conclusions. More adventurous possibilities exist, which we explore now. At once, we could consider using set union instead of set intersection, thus yielding two definitions dual to the ones in Definition 4.1. The first one is Sactually
a dead-end: Defining paraconsistent consequences via ϕ ∈ Th W ± ∪ E∈E ΠE is pointless because it admits every formula of LΣ to be concluded whenever (DΣ , W ± ) has more than one extension. The second one takes the route of counting as a conclusion any formula for which an argument (manifested by an extension containing the formula) exists: DEFINITION 4.2. Given the prerequisites of Definition 4.1, we define W `c ϕ iff ϕ ∈

S

E∈E

Th W ± ∪ ΠE




(credulous unsigned consequence).

Independent of the controversial matter on whether one argument is enough for drawing a conclusion, `c has the disadvantage of not being closed under classical deduction. Anyway, `c provides us with more conclusions than its two predecessors. That is, we obtain from W as given in (6) the conclusions A, B, ¬C, D. Even in view of the premise ¬A ∨ ¬B , concluding A and B is in fact quite reasonable, as also exhibited by many other approaches like [20, 11]. In general, we observe that the three hitherto introduced consequence relations enjoy the inclusion property: `p ⊆ `s ⊆ `c . So far, we have chosen the option that literals involved in a contradiction are ‘forgotten’ while reasoning. This has the drastic consequence that reflexivity fails to hold. At the cost of losing closure under classical deduction, we can regain reflexivity by adapting the above three definitions of paraconsistent inference in following way. DEFINITION 4.3. Given the prerequisites of Definition 4.1, we define T




± W `± W ± ∪ E∈E ΠE p ϕ iff ϕ ∈ Th
T ± ± W `± s ϕ iff ϕ ∈ E∈E Th W ∪ ΠE

(prudent signed consequence), (skeptical signed consequence).

These two new relations can be shown to extend `p and `s in the most restrictive way. In fact, every additional paraconsistent conclusion is either a premise or a logical consequence of a single premise. It is worth mentioning that `± s (as well as `s ) bears some similarity with skeptical reasoning in inheritance systems. It notably suffers from the so-called

JARS9707.tex; 7/11/1997; 14:51; v.7; p.8

199

SIGNED SYSTEMS FOR PARACONSISTENT REASONING

prudent

unsigned ¬C

skeptical credulous

A ∨ B, ¬C, D A, B, ¬C, D

signed A, B, ¬C, ¬A ∨ ¬B, ¬A ∨ D, ¬B ∨ D A, B, ¬C, ¬A ∨ ¬B, D A, ¬A, B, ¬B, ¬C, D

Figure 1. Paraconsistent conclusions obtained from theory (6).

floating conclusions problem [17] (intuitively, it may happen that a formula is concluded but none of the expected intermediate conclusions from which the formula follows is itself concluded). Now, adapting the third relation (Definition 4.4) gives a less restricted result. DEFINITION 4.4. Given the prerequisites of Definition 4.1, we define ± W `± c ϕ iff ϕ ∈

S

E∈E

Th W ± ∪ ΠE




(credulous signed consequence).

Returning to the example (6), we obtain W `± c A, W `± c ¬B,

W `± c ¬A,

W `± c B,

W `± c ¬C,

W `± c D,

while W 6`± c C,

W 6`± c ¬D.

As already noted in the context of `c , we unproblematically have ± ± W `± c A and W `c ¬A but W 6`c A ∧ ¬A.

The same applies to proposition B . The salient conclusions drawn by means of our consequence relations from theory (6) are summarized in Figure 1. To sum up this section, we have defined a family of paraconsistent consequence relations that furnishes a flexible framework for reasoning from inconsistent theories. These relations compare with each other in the following way. THEOREM 4.1. Let Ci be the operator corresponding to Ci (W ) = {ϕ | W `i ϕ} where i ranges over {p, s, c}, and similarly for Ci± . Then, we have (1) Ci (W ) ⊆ Ci± (W ), (2) Cp (W ) ⊆ Cs (W ) ⊆ Cc (W ) and Cp± (W ) ⊆ Cs± (W ) ⊆ Cc± (W ) . That is, signed derivability gives more conclusions than unsigned derivability and within each series of consequence relations the strength of the relation is increasing. Moreover, we have the following logical properties:

JARS9707.tex; 7/11/1997; 14:51; v.7; p.9

200

PH. BESNARD AND T. SCHAUB

THEOREM 4.2. Let Ci be the operator corresponding to Ci (W ) = {ϕ | W `i ϕ} where i ranges over {p, s, c}, and similarly for Ci± . Then, we have (3) (4) (5) (6) (7) (8)

W ⊆ Ci± (W ),

Cp (W ) = Th Cp (W ) and Cs (W ) = Th Cs (W ) , Ci± (W ) = Ci± (Ci± (W )), Th(W ) 6= LΣ =⇒ Th(W ) = Ci (W ) = Ci± (W ), Ci (W ) 6= LΣ and Ci± (W ) 6= LΣ , W ⊆ W 0 6=⇒ Ci (W ) ⊆ Ci (W 0 ) and W ⊆ W 0 6=⇒ Ci± (W ) ⊆ Ci± (W 0 ).

The last item simply says that all of our consequence relations are non-monotonic.
For instance, we have Ci ({A, A → B}) = Ci± ({A, A → B}) = Th {A, B} , while neither Ci ({A, ¬A, A → B}) nor Ci± ({A, ¬A, A → B}) contains B . Moreover, we have that whenever two theories W and W 0 are logically equivalent but do not have the same NNF, they still have the same set of conclusions. In some sense, the unsigned relations are prone to an interpretation in terms of belief revision: They restore consistency, as witnessed by property Ci (W ) =
Th Ci (W ) 6= LΣ . Rather the signed relations are much more in accord with paraconsistent reasoning, as illustrated by W ⊆ Ci± (W ). 5. A Structural Refinement Whenever a problem instance may give rise to numerous solutions, it is useful to provide a preference criterion for selecting a subset of preferred solutions. However, unlike many other approaches like [4] that presuppose a given ordering on formulas, we aim at extracting preferences from the contents of the given knowledge base only. For this purpose, we restrict our attention to formulas in conjunctive normal form (CNF). This is a conjunction of disjunctions of literals, or simply a set of clauses. Let us motivate this option of our approach by the following theory. {A, B, A → C, B → ¬C}

(7)

Importantly, this theory comprises two qualitatively different sorts of items of information. Specifically, we can distinguish between ‘facts’ (exemplified by the first two premises A and B ) and ‘rules’ such as A → C and B → ¬C . In fact, both rules are applicable, thereby leading to inconsistency. Proceeding along our basic procedure described in the preceding section, we get the default theory


{δA , δB , δC }, {A+ , B + , A− ∨ C + , B − ∨ C − } .

This theory yields three alternative extensions, containing {A, B}, {A, C}, and {B, ¬C}, respectively.

JARS9707.tex; 7/11/1997; 14:51; v.7; p.10

SIGNED SYSTEMS FOR PARACONSISTENT REASONING

201

Intuitively, we prefer the first extension over the two last extensions on the grounds that it represents the most ‘definite’ knowledge (meaning that information provided by facts is more evidential than information obtained through rules). In fact, in such a case, we argue that the more ‘disjunctive’ a piece of information is, the less ‘definite’ it is. In terms of theories in CNF this means that facts provide more definite information than disjunctions. Accordingly, we want to stick to the more definite and so more evidential knowledge in the presence of a contradiction. This motivates the following definition ranking propositions according to their degree of definiteness: DEFINITION 5.1. Let C = hci ii∈I be a family of clauses in LΣ . For each propositional letter α ∈ Σ, we define ρC : Σ → N as ρC (α) = min{n | n = |ci | and α ∈ ci or ¬α ∈ ci for some i ∈ I},

where |c| is the number of literals in a clause c. We omit the parameter C in ρC (·) whenever the referential set of clauses C is clearly determinable from the context. For the example given in (7), we obtain the following values (intuitively ranking the propositions according to their degree of definiteness): ρ(A) = 1,

ρ(B) = 1,

ρ(C) = 2.

For a given clause set C , we use a ranking function %C : Σ → N on the alphabet Σ (such as ρC ) for inducing a hierarchy on the default rules in DΣ : DEFINITION 5.2. Let C = hci ii∈I be a family of clauses in LΣ , and let %C : Σ → N be some ranking function on alphabet Σ. We define the hierarchy of DΣ wrt %C as the partition hDn in∈ω of DΣ such that δα ∈ Dn iff %C (α) = n. Strictly speaking, hDn in∈ω is not always a genuine partition, since Dn may be the empty set for some values of n. In our example, our ranking function ρ (relying on the degree of definiteness) induces the following partition: D1 = {δA , δB },

D2 = {δC }.

In the construction of extensions, we can use such a hierarchy for giving priority to the restoration of propositional symbols having been assigned a higher value by the ranking function at hand. DEFINITION 5.3. Let W be a set of formulas in LΣ and E a set of formulas in LΣ∪Σ± . Let hDnSin∈ω be the hierarchy of DΣ wrt some ranking function %W . Then, E = n∈ω En is a hierarchic extension of (D, W ) relative to % if E1 = W ± and En+1 is an extension of (Dn+1 , En ) for all n > 1.

JARS9707.tex; 7/11/1997; 14:51; v.7; p.11

202

PH. BESNARD AND T. SCHAUB

In our example, there is only one hierarchic extension. It contains A and B , which is what we were aiming at. Observe that any hierarchic extension is an extension, but not vice versa. Using hierarchic extensions induced by ρ as given in Definition 5.1, we adapt in the obvious way the notion of paraconsistent inference defined in the previous section. We denote the corresponding consequence relations by adding an h to the respective index, eg. `sh or `± sh in the case of skeptical reasoning. In the example (7), we have for instance W `sh A ∧ B.

In contrast with this, observe that W 6`s A ∧ B

and W `s A ∨ B.

Switching from skeptical to credulous reasoning, we observe W 6`ch C,

W 6`ch ¬C

in contrast to W `c C,

W `c ¬C.

Even though our approach to ranking functions on the propositional letters of a given alphabet is a general one, we have committed ourselves more or less to functions measuring the degree of definiteness induced by the set of clauses at hand. Of course, there might be cases where one wants a more flexible treatment. For instance, one may want to distinguish between arbitrary clauses and clauses expressing integrity constraints. In such a case, one might want to attribute the latter clauses the highest priority while ignoring their degree of definiteness. On the other hand, our hierarchic paraconsistent inference should not be confused with paraconsistent inference systems applied to stratified theories [4]. The latter are based on a given ranking of the formulas in the theory. Instead, we deal with a ranking on the propositional letters, which is induced by the theory. In that way, our approach differs also from [28] among others, which employs a reliability relation. The next result shows that Theorem 3.2 extends to the hierarchic case. That is, our approach reduces nicely to classical logic in case of consistent theories. THEOREM 5.1. Let W be a consistent set of formulas in LΣ . Then, the default theory (DΣ , W ± ) has a unique hierarchic extension E . Moreover, Th(W ) = E ∩ LΣ . Moreover, all results given at the end of the preceding section carry over to the hierarchic case. In addition, we have the following relationship: `p ⊆ `ph ,

`s ⊆ `sh

but `ch ⊆ `c .

JARS9707.tex; 7/11/1997; 14:51; v.7; p.12

SIGNED SYSTEMS FOR PARACONSISTENT REASONING

203

In this way, we have obtained a conservative yet powerful refinement of our basic approach. 6. Toward More General Settings Up to now, we have pursued a somehow global approach in restoring semantic links between positive and negative literals. In fact, the application of a + ↔¬α− rule (α↔α: α+ )∧(¬α↔α − ) reestablishes the semantic link between all occurrences of proposition α and its negation ¬α at once. A finer-grained approach is to establish the connections between complementary occurrences of a literal individually. As an example, consider the theory W = {A, ¬A, A → B, ¬A → B}.

(8)

Because A and ¬A constitute a genuine contradiction, none of the former inference relations will allow for deriving B . Even though the signed consequence relations provide conclusions A → B and ¬A → B (because of reflexivity), none of them allows for deriving B . This is because our overall approach is so far based on the safe idea to discard all derivations that rely on propositions giving rise to genuine contradictions, like A ∧ ¬A. A closer look reveals, however, that the proof for B , namely: {A → B, ¬A → B} ` B , does not rely on A ∧ ¬A, even though it mentions propositional letter A. The idea is then to restore the overall semantic link between α and ¬α by incrementally restoring the semantic links between complementary occurrences of α. For this purpose, we use an index set I assigning different indexes to all occurrences of all literals in some given formula. This leads to the following definition: For all α ∈ Σ and all i, j ∈ I , define δαi,j

=

− : (α ↔ α+ i ) ∧ (¬α ↔ αj ) − (α ↔ α+ i ) ∧ (¬α ↔ αj )

(9)

provided that there are complementary occurrences of α, otherwise set δαi,j = δα . Compared with the definition of δα in (2), the justification of δαi,j had to be slightly strengthened. This is because unlike in the preceding sections, the application of default rule δαi,j is checked in the presence of both signed literals α+ and α− and unsigned literals α and ¬α. After indexing the diverse complementary occurrences in (8), we obtain the following default theory 1,2 1,3 4,2 4,3 − − + + + ({δA , δA , δA , δA , δB }, {A+ 1 , A2 , A3 ∨ B , A4 ∨ B }).

This results in two extensions, one in which all semantic links involving A+ 1 are spared out, and another one leaving blank the semantic link to A− 2 . Rules 4,3 δA and δB contribute to both extensions, which makes us derive B even under our prudent unsigned consequence relation. With the obvious modifications to

JARS9707.tex; 7/11/1997; 14:51; v.7; p.13

204

PH. BESNARD AND T. SCHAUB

Definition 4.1 needed for integrating default rules of the form δαi,j as given in (9), we thus obtain W `p B

while W 6`p A and W 6`s A.

While A and ¬A are obtainable by the signed counterpart of `p , this does not extend to A ∧ ¬A, that is W 6`± p A ∧ ¬A. Because of the inclusion property expressed in Condition 2 of Theorem 4.1, these derivations extend to skeptical and credulous inference relations. So far, we have focused on reestablishing semantic links between positive and negative literals from their signed counterparts. At the cost of neglecting and so restoring even less semantic links than above, we obtain an alternative approach based on signed formulas that aims at restoring foremost original (unsigned) − literals. This is achieved by decoupling in (9) the restoration of α+ i and αj and restoring separately the original meaning of each occurrence. This leads to the following definition: For all α ∈ Σ and all i, j ∈ I , we define for all positive and negative occurrences of α, respectively, δαi+ =

: (α ↔ α+ i ) , + (α ↔ αi )

δαj− =

: (¬α ↔ α− j ) (¬α ↔ α− j )

.

(10)

Alternatively, (10) can be obtained by dropping in (9) the condition about the existence of complementary occurrences. The series of default rules in (10) provides actually a rather fine-grained setting, since it allows for restoring in turn each occurrence of each propositional letter. As a final example, consider the theory W = {A, B, ¬A ∨ ¬B, C}.

(11)

Following the approach described at the start of this section, we obtain default theory 1,3 4,2 + − − + ({δA , δB , δC }, {A+ 1 , B2 , A3 ∨ B4 , C }).

This theory amounts actually to the one obtained in our basic approach using δA 1,3 4,2 and δB instead of δA and δB . In any case, we may either restore the semantic link between the two occurrences of A or those among B . In such a sparse setting, it is worthwhile to restore individual occurrences rather than their semantic links among each other. Taking default rules of the form (10) yields theory 1+ 3− 2+ 4− + − − + ({δA , δA , δB , δB , δC }, {A+ 1 , B2 , A3 ∨ B4 , C }).

Because all literal occurrences (apart from C + ) are involved in a common contradiction, we actually obtain four extensions, containing {A, B, B4− , C},

JARS9707.tex; 7/11/1997; 14:51; v.7; p.14

SIGNED SYSTEMS FOR PARACONSISTENT REASONING

205

+ + {A, B, A− 3 , C}, {¬A, B, A1 , C}, and {A, ¬B, B2 , C}. Applying this approach in a straightforward manner gives us obviously all possibilities for resolving an inconsistency. This is where our structural refinement of Section 5 steps in: We may define a ranking function that assigns to each occurrence of a propositional letter the length of the clause it occurs in. Formally, we define for a family C = hcj ij∈J of clauses in LΣ and some literal occurrence α in cj the ranking function σC as follows:

σC (α) = |cj |.

In our example, we obtain σ(A+ 1 ) = 1,

σ(B2+ ) = 1,

σ(B4− ) = 2,

σ(C + ) = 1.

σ(A− 3 ) = 2,

With the corresponding hierarchy, we obtain only those extensions containing A and B , namely, {A, B, B4− , C} and {A, B, A− 3 , C}. We thus obtain A, B and C from all resulting hierarchical consequence relations. It is worth mentioning that the two generalizations inherit the overall comportment of our original approach. Notably, they reduce to classical logic in the consistent case. 7. Discussion and Related Work A number of proposals address inconsistent information. First, there is the wide range of paraconsistent logics [24]. As already noticed in Section 4, there is a sharp contrast between our approach and such logics, in that they, 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 aforementioned approaches in general is given in [5]. The idea of ‘forgetting’ literals while reasoning from inconsistency is already present in [18]. However, the idea is then applied using, within the objectlanguage, an explicit representation of a lattice of truth-values (on using lattices for dealing with inconsistency see also [2, 3, 29]). The same disadvantage can be found in [10], which proposes an approach to reasoning in the presence of contradictions that translates a logic into a family of other logics, for instance, classical logic into three-valued logics. In contrast, our approach sticks to a standard propositional language because the signed formulas are only a technical device of the inner machinery for paraconsistent reasoning. 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 [1], and that is applying disjunctive syllogism to contradictory premises. However, we do not go as far as sanctioning any classical inference not

JARS9707.tex; 7/11/1997; 14:51; v.7; p.15

206

PH. BESNARD AND T. SCHAUB

using inconsistent subformulas. That is, we still follow the principle of relevant logics that an inference rule is a priori applicable to any premise. This is in contrast with the idea of restricted access logic [14], where all classical inference rules are admitted with some special application conditions. Although our approach mentions default logic and paraconsistent reasoning, it should not be confused with the one in [22]. In fact, that approach mixes both kinds of reasoning, whereas we are aiming only at paraconsistent reasoning. We resort to default logic simply as a technical device to achieve paraconsistency. Wagner [31] describes a framework for handling contradictions that relies on the notions of ‘support’ and ‘acceptance’. Although this is very appealing from a philosophical point of view, the realization of these concepts requires recursive derivability procedures that work only for ‘well-behaved’ theories that do not make the latter procedures loop. Also, the format of the theories is syntactically restricted to certain inference rules on which the aforementioned inference procedures rely. In contrast to this, our approach provides a general and uniform treatment that is syntax independent and has no procedural attachment. Considerable efforts have also been done by the logic programming community in order to capture belief revision and paraconsistent reasoning, in particular, when considering extended logic programs: Among others, logic programming with inconsistencies was addressed in [6, 7]. This avenue of research is further developed in [16], where it is shown how the approach of [6] can be extended by classical inferences, like reasoning by cases. Intuitively, the corresponding entailment relations amount to logic programming in a three-valued (and four-valued, respectively) logic. The major difference to our approach is that compared with classical entailment, these approaches are sound but not complete (even though the set of premises is consistent). As with other approaches, this is because they aim at paraconsistent reasoning in a logic programming setting that does not necessarily coincide with classical logic. A survey of paraconsistent semantics for extended logic programs can be found in [12]. In the course of the preceding sections, we have already mentioned the relationships and differences between our approach and [20, 27] and [4, 28], respectively, so that we refrain from repeating these here. 8. Conclusion We have presented a family of paraconsistent consequence relations that furnishes a flexible framework for reasoning from inconsistent theories. The idea is to transform an inconsistent theory into a consistent one by renaming all literals occurring in the theory. Then, we restore some of the original contents of the theory by introducing progressively formal equivalences linking the original literals to their renamings. This is accomplished by appeal to default logic in a consistency-sensitive way. Importantly, our approach works at the level of the propositions; it deals with the semantical link between a proposition and its nega-

JARS9707.tex; 7/11/1997; 14:51; v.7; p.16

SIGNED SYSTEMS FOR PARACONSISTENT REASONING

207

tion. It is therefore independent of the combination of the connectives that are actually applied to the propositions in order to form entire formulas. An advantage of our approach is that its inner machinery banks on a theoretically and practically well studied AI-technology, namely, default reasoning by supernormal default theories [23, 9, 13, 8] (see Appendix A). This fragment of default logic has already been implemented (e.g., Theorist [23]) and applied (e.g., to model-based diagnosis [26]) in several settings. In this way, our approach should allow for an easy application in practice. Appendix A. Formal Elaboration The formal elaboration of the default logic machinery underlying our paraconsistent approach is done through establishing a series of connections between theories. First, we have to account for the connection dealing with extending a theory by adding equivalences of the kind presented above. This is captured via the standard way? in classical logic dealing with definitions in theories: DEFINITION A.1. Let E ± be a set of formulas in LΣ± and E ] be a set of formulas in LΣ∪Σ± . Then, E ] is the definitional expansion for E ± iff E ] = E ± ∪ {α ↔ α+ | α+ ↔ ¬α− ∈ E ± and α ∈ Σ}.

The fundamental property is that a definitional expansion is conservative, which means that it does not introduce any further conclusions expressed in the initial language. In our specific case this property amounts to the next theorem.?? THEOREM A.2. Let E ± be a set of formulas in LΣ± and E ] be the definitional expansion for E ± . Then, we have for ϕ± ∈ L± that E ± |= ϕ± iff E ] |= ϕ± . We now take advantage of the preceding theorem to handle more easily the default theories of interest to us by relating any δα to a default rule whose justification and consequent are the same formula. THEOREM A.3. Let W ± be a set of formulas in LΣ± , and let (

±

D =



)

: α+ ↔ ¬α− α ∈ Σ . α+ ↔ ¬α−

Let E ± be a set of formulas in LΣ± , and let E ] be the definitional expansion

± ± ± ± ] for E . Then, Th E is an extension of (D , W ) iff Th E is an extension of (DΣ , W ± ). ? We do not follow the standard terminology (extension by definition), in order to avoid confusion over the word extension. ?? In fact, this is an easy corollary of a result that can be found in any logic textbook.

JARS9707.tex; 7/11/1997; 14:51; v.7; p.17

208

PH. BESNARD AND T. SCHAUB

This theorem has several important consequences. The first one, expressed in Corollary 3.1, tells us that we always have at least one extension (of (DΣ , W ± )) to look at when it comes to extracting the paraconsistent conclusions of the initial theory (W ). The second and the third consequences are more technical results, both useful in assessing the value of our method and interesting as specific properties of the default theories we consider. COROLLARY A.4. Let W be a set of formulas in LΣ and let ϕ be a formula in LΣ . (Semi-monotonicity) ? For any Σ0 , if E is an extension of (DΣ , W ± ) then there exists an extension E 0 of (DΣ∪Σ0 , W ± ) such that E ⊆ E 0 . (Cumulativity) E is an extension of (DΣ , W ± ∪ {ϕ}) iff E is an extension of (DΣ , W ± ) that contains ϕ. The property of semi-monotonicity is a desirable computational property that implies that extensions are constructible in a truly iterative way (without any fixed-points). Cumulativity is a formal property indicating a certain stability of inference relations by demanding that the addition of a conclusion to the premises should not change the entire set of conclusions. Full-fledged default logic enjoys neither semi-monotonicity [25] nor cumulativity [19]. From a more general perspective, Theorem A.3 tells us that our considered default theories amount to the class of prerequisite-free normal (also called supernormal [9]) default theories. This fragment of default logic is by now very well studied [23, 9, 13, 8] and there exist several implementations of it (e.g., Theorist [23]). B. Proofs of Theorems Let W be a consistent set of formulas in LΣ . Consider the set of formulas E ± = W ± ∪ {α+ ↔ ¬α− | α ∈ Σ}.

(12)

Observe that any interpretation I ± ⊆ Σ± for formulas in LΣ± of form (12) is uniquely characterized by sets I + ⊆ {α+ | α ∈ Σ} due to the presence of axiom α+ ↔ ¬α− for all α ∈ Σ. For any interpretation I ⊆ Σ over LΣ , define I + = {α+ | α ∈ I}. Clearly, + I is an interpretation over LΣ± . Moreover, an inductive argument over the structure of formulas shows that I is a model of W iff I + is a model of E ± . Hence, we have that E ± must be consistent because W is consistent by definition. As a consequence, we obtain that





Th E ± = Th W ± ∪ {α+ ↔ ¬α− | α ∈ Σ} ?

Observe that DΣ∪Σ0 = DΣ ∪ DΣ0 .

JARS9707.tex; 7/11/1997; 14:51; v.7; p.18

209

SIGNED SYSTEMS FOR PARACONSISTENT REASONING

is the unique extension of the default theory ( ±

±

(D , W ) =



)

!

: α+ ↔ ¬α− α ∈ Σ ,W± . α+ ↔ ¬α−


According to Theorem A.3, there is thus also a unique extension Th E ] of (DΣ , W ± ), where E ] is the definitional expansion for E ± , as defined in Definition A.1.
Moreover, we have that Th(W ) = Th E ] ∩ LΣ by the fact that the set of models of W is isomorphic to those of E ± and that E ] is the definitional expansion for E ± into language LΣ . This finishes the proof of Theorem 3.2. T




ϕ ∈ Ti for
i ∈S{p, s, c}, where Ti stands for Th W ± ∪ E∈E ΠE , (1) Consider
T ± ± E∈E Th W ∪ ΠE , E∈E Th W ∪ ΠE , respectively. For each (unsigned) occurrence of α or ¬α in ϕ there is an equivalence α ↔ α+ or ¬α ↔ α− , respectively, in the underlying theory Ti . By substitution of logical equivalences, we thus have also ϕ± ∈ Ti . This shows that Ci (W ) ⊆ Ci± (W ) for i ∈ {p, s, c}. (2) The set inclusions Cs (W ) ⊆ Cc (W ) and Cs± (W ) ⊆ Cc± (W ) follow immediately from elementary set theory. Let us thus turn to Cp (W ) ⊆ Cs (W ) and Cp± (W ) ⊆ Cs± (W ), respectively.
T Consider ϕ ∈ Th W ± ∪ E∈E ΠE = Cp (W ). That is, W± ∪

\

ΠE |= ϕ.

E∈E

By monotonicity, this implies W ± ∪ ΠE |= ϕ.




for each E ∈ E. That is,
ϕ ∈ Th W ± ∪ ΠE for all E ∈ E. In other words, T ϕ ∈ E∈E Th W ± ∪ ΠE = Cs (W ). The same argumentation shows that Cp± (W ) ⊆ Cs± (W ). Recall that we can identify W with its NNF (because they are logically equivalent). (3) Now, W ± = {ϕ± | ϕ ∈ W }. By Definition 2.1, W ± = E1 and E1 ⊆ E , so it follows that W ±
⊆ Ci± (W ). Hence, W ⊆ Ci± (W ). (4) Let ϕ ∈ Th Cp (W ) . By compactness, ϕ1 , . . . , ϕn ` ϕ for some ϕ1 , . . . , ϕn such that ϕi ∈ Cp (W ) forTi = 1, . .
. , n. Hence, W `p T ϕi for i =
1, . . . , n. That is, ϕi ∈ Th W ± ∪ E∈E ΠE . Then, Th W ± ∪ E∈ETΠE ` ϕ
i . In ± view of ϕ1 , . . . , ϕn ` ϕ, this means that ϕ ∈ Th W ∪ E∈E ΠE . So, W `p ϕ whence ϕ ∈ Cp (W ).
We have thus proven Th Cp (W ) ⊆ Cp (W ) and the converse inclusion is trivial.

JARS9707.tex; 7/11/1997; 14:51; v.7; p.19

210

PH. BESNARD AND T. SCHAUB

For the second equality, we adapt the same reasoning, after noticing that the intersection of a family of deductively closed sets is itself a deductively closed set. (5) By definition, Ci± (W ) = {ϕ | W `i ϕ} and Ci± (Ci± (W )) = {ϕ | {φ | W `i φ} `i ϕ}. Consider i = p. We have 

Cp± (W ) = ϕ | ϕ± ∈ Th W ± ∪

T

E∈E ΠE




and Cp± (Cp± (W )) = {ϕ | ϕ± ∈ Th([{φ | φ± ∈ Th W ± ∪

T

E∈E ΠE

Observe that [{φ | φ± ∈ Th W ± ∪ = {φ± | φ± ∈ Th




}]± ∪

T

F ∈F ΠF )}.




T

± E∈E ΠE }]
T W ± ∪ E∈E ΠE }.

By definition, E is the set of all extensions E of (DΣ , WT± ), while
F is the set of all extensions F of (DΣ , {φ± | φ± ∈ Th W ± ∪ E∈E ΠE }). By default logic, we thus have 

φ± | φ± ∈ Th W ± ∪

T

E∈E ΠE




⊆ F.

for each resulting extension F . This implies 

φ± | φ± ∈ Th W ± ∪

Clearly, W ± ⊆

T

F ∈F

T

E∈E ΠE




⊆

T

F ∈F ΠF .

ΠF . So that we obtain



Cp± (Cp± (W )) = ϕ | ϕ± ∈ Th W ± ∪

T

F ∈F ΠF




= Cp± (W ).

An adaptation of the same reasoning yields the result for i ∈ {s, c}. (6) By Theorem 3.2, E = {E}, where E ∩LΣ = Th(W ). Then, intersections and unions ranging over E identify with the simple value E , so that i = p, i = s,
±∪Π . and i = c are all identical. We thus have W ` ϕ iff ϕ ∈ Th W i E
But Th W ± ∪ ΠE = E as is known from default logic. Using Theorem 3.2, we get W `i ϕ iff ϕ ∈ Th(W ).
For the signed case, again, Th W ± ∪ ΠE = E . Now, observe that E extends Th(W ) by definition, namely, α+ =def α and α− =def ¬α for each α ∈ Σ. This means that ϕ± ∈ E iff ϕ ∈ E . From Theorem 3.2, it follows that ϕ± ∈ E iff ϕ ∈ Th(W ). Therefore, W `± i ϕ iff ϕ ∈ Th(W ). (7) Suppose Ci (W ) = LΣ . Then, α ∧ ¬α ∈ Ci (W ) for some α ∈ Σ. For i ∈ {i, s, c}, this implies α ∧ ¬α ∈ E for at
least one E ∈ E (since each extension E is such that E = Th W ± ∪ ΠE ). In other words, at least one extension is inconsistent. By default logic, this is possible only if W ± is inconsistent. This contradicts the fact that W ± is consistent (a model is obtained by assigning true to each α+ and each α− ).

JARS9707.tex; 7/11/1997; 14:51; v.7; p.20

211

SIGNED SYSTEMS FOR PARACONSISTENT REASONING

Let us now turn to the case Ci± (W ) 6= LΣ where i ∈ {s, p}. Assume ϕ± ∈ Ci± (W ) for each ϕ ∈ LΣ . Then, α+ ∧ α− ∈ Ci± (W ) for each α ∈ Σ. Hence, ¬(α+ ↔ α− ) ∈ Ci± (W ) for each α ∈ Σ. It follows that for each E in E , ¬(α+ ↔
α− ) ∈ E for each α ∈ Σ. Then, ΠE =
∅. So, W `± i ϕ iff ϕ± ∈ Th W ± . Hence, for each ϕ ∈ LΣ , ϕ± ∈ Th W ± . Now, W is finite. So there exists some α ∈ Σ that does not
occur in W . Then, α+ does not occur in W ± . Accordingly, α+ 6∈ Th W ± since the atomic formula α+ is
not logically valid. This contradicts ϕ± ∈ Th W ± for each ϕ ∈ LΣ . So, our assumption Ci± (W ) = LΣ is false. Finally, assume Cc± (W ) 6= LΣ . Since W is finite, there exists α ∈ Σ that does not occur in W . Then, neither α+ nor α− occur in W ± . So, α+ ∧ α− would follow from W ± ∪ΠE only if it would follow from Conseq (δα ) alone (according to default logic, W ± ∪ ΠE is consistent because W ± is). Clearly, α+ ∧ α− does not follow from Conseq (δα ); hence α+ ∧ α− does
+ − ± not follow from W ± ∪ ΠS E . So, for each E ∈
E , α ∧ α 6∈ Th W ∪ ΠE . As a result, α+ ∧ α− 6∈ E∈E Th W ± ∪ ΠE . That is, α+ ∧ α− 6∈ Cc± (W ) for each ϕ ∈ LΣ . (8) The proof is given immediately after Theorem 4.2. Theorem 5.1 is obtained by the same argumentation as given in Proof 3.2; however, it is wrapped into an induction over the layers of the underlying hierarchy. Theorem A.2 is a corollary of a result that can be found in any logic textbook, like [30]. Let W ± be a set of formulas in LΣ± , and let (

D± =



)

: α+ ↔ ¬α− α ∈ Σ . α+ ↔ ¬α−

Let E ± be a set of formulas in LΣ± , and let E ] be the definitional expansion for E ± . That is, E ] = E ± ∪ {α ↔ α+ | α+ ↔ ¬α− ∈ E ± and α ∈ Σ}.

Consider : α+ ↔ ¬α− ∈ DΣ . (α ↔ α+ ) ∧ (¬α ↔ α− ) The consequence of this default rule, (α ↔ α+ ) ∧ (¬α ↔ α− ), is actually equivalent to (α+ ↔ ¬α− ) ∧ (α ↔ α+ ). DΣ can thus be written as follows: (

DΣ =



)

: α+ ↔ ¬α− α ∈ Σ . (α+ ↔ ¬α− ) ∧ (α ↔ α+ )

JARS9707.tex; 7/11/1997; 14:51; v.7; p.21

212

PH. BESNARD AND T. SCHAUB







The claim that Th E ± is an extension of (D± , W ± ) iff Th E ] is an extension of (DΣ , W ± ) is then a direct consequence of the fact that E ] is the definitional expansion for E ± . This finishes the proof of Theorem A.3. References 1. Anderson, A. and Belnap, N.: Entailment: The Logic of Relevance and Necessity Vol. I, Princeton University Press, 1975. 2. Arieli, O. and Avron, A.: Logical bilattices and inconsistent data, in Proc. Logic in Computer Science Conference, 1994, pp. 468–476. 3. Belnap, N.: A useful four-valued logic, in J. Dunn and G. Epstein (eds), Modern Uses of Multiple-Valued Logic, Reidel, 1977. 4. Benferhat, S., Dubois, D. and Prade, H.: Argumentative inference in uncertain and inconsistent knowledge bases, in Proc. Ninth International Conference on Uncertainty in Artificial Intelligence, 1993, pp. 411–419. 5. Besnard, P.: Paraconsistent logic approach to knowledge representation, in M. de Glas and D. Gabbay (eds), Proc. First World Conference on Fundamentals of Artificial Intelligence, 1991. 6. Blair, H. and Subrahmanian, V. S.: Paraconsistent foundations of logic programming, J. NonClassical Logics 5(2) (1988), 45–73. 7. Blair, H. and Subrahmanian, V. S.: Paraconsistent logic programming, Theoretical Computer Science 68(2) (1989), 135–154. 8. Brass, S.: On the semantics of supernormal defaults, in Ruzena Bajcsy (ed.), Proc. International Joint Conference on Artificial Intelligence, Morgan Kaufmann Publishers, 1993, pp. 578–583. 9. Brewka, G.: Nonmonotonic Reasoning: Logical Foundations of Commonsense, Cambridge University Press, Cambridge, 1991. 10. Carnielli, W., Fari˜nas del Cerro, L. and Lima Marques, M.: Contextual negations and reasoning with contradictions, in J. Mylopoulos and R. Reiter (eds), Proc. International Joint Conference on Artificial Intelligence, Morgan Kaufmann Publishers, 1991, pp. 532–537. 11. da Costa, N.: On the theory of inconsistent formal systems, Notre Dame Journal of Formal Logic 15 (1974), 497–510. 12. Dam´asio, C. V. and Pereira, L. M.: A survey on paraconsistent semantics for extended logic programs and transformations for well-founded semantics, in D. Gabbay and P. Smets (eds), Handbook of Defeasible Reasoning and Uncertainty Management Systems Vol. 2, Oxford University Press, 1997, to appear. 13. Dix, J.: On cumulativity in default logic and its relation to Poole’s approach, in B. Neumann (ed.), Proc. European Conference on Artificial Intelligence, John Wiley and Sons, 1992, pp. 289–293. 14. Gabbay, D. and Hunter, A.: Restricted access logics for inconsistent information, in M. Clarke, R. Kruse, and S. Moral (eds), Proc. European Conference on Symbolic and Quantitative Approaches to Reasoning and Uncertainty, Springer-Verlag, 1993. 15. Gallier, J.: Logic for Computer Science: Foundations of Automated Theorem Proving, Harper and Row, New York, 1986. 16. Grant, J. and Subrahmanian, V. S.: Reasoning in inconsistent knowledge bases, IEEE Transactions on Knowledge and Data Engineering 7(1) (1995), 177–189. 17. Horty, J., Thomason, R. and Touretzky, D.: A skeptical theory of inheritance in nonmonotonic semantic networks, Artificial Intelligence 42 (1990), 311–348. 18. Kifer, M. and Lozinskii, E.: RI: A logic for reasoning with inconsistency, in Proc. Logic in Computer Science Conference, 1989, pp. 253–262. 19. Makinson, D.: General theory of cumulative inference, in M. Reinfrank, J. de Kleer, M. Ginsberg, and E. Sandewall (eds), Proc. Second International Workshop on Non-Monotonic Reasoning Vol. 346 of Lecture Notes in Artificial Intelligence, Springer-Verlag, 1989, pp. 1–18. 20. Manor, R. and Rescher, N.: On inferences from inconsistent information, Theory and Decision 1 (1970), 179–219.

JARS9707.tex; 7/11/1997; 14:51; v.7; p.22

SIGNED SYSTEMS FOR PARACONSISTENT REASONING

213

21. Murray, N.: Completely non-clausal theorem proving, Artificial Intelligence 18 (1982), 67–85. 22. Pequeno, T. and Buchsbaum, A.: The logic of epistemic inconsistency, In J. Allen, R. Fikes and E. Sandewall (eds), Proc. Second International Conference on the Principles of Knowledge Representation and Reasoning, Morgan Kaufmann Publishers, San Mateo, CA, 1991, pp. 453– 560. 23. Poole, D.: A logical framework for default reasoning, Artificial Intelligence 36 (1988), 27–47. 24. Priest, G., Routley, R. and Norman, J.: Paraconsistent Logics, Philosophica Verlag, 1989. 25. Reiter, R.: A logic for default reasoning, Artificial Intelligence 13(1–2) (1980), 81–132. 26. Reiter, R.: A theory of diagnosis from first principles, Artificial Intelligence 32(1) (1987), 57–96. 27. Rescher, N. and Brandom, R.: The Logic of Inconsistency, Blackwell, 1980. 28. Roos, N.: A logic for reasoning with inconsistent knowledge, Artificial Intelligence 57 (1992), 69–103. 29. Sandewall, E.: A functional approach to non-monotonic logic, Computational Intelligence 1 (1985), 80–87. 30. Shoenfield, Joseph, R.: Mathematical Logic, Addison-Wesley, Reading, MA, 1967. 31. Wagner, G.: Ex contradictione nihil sequitur, in J. Mylopoulos and R. Reiter (eds), Proc. International Joint Conference on Artificial Intelligence, Morgan Kaufmann Publishers, 1991, pp. 538–543.

JARS9707.tex; 7/11/1997; 14:51; v.7; p.23