Ex contradictione nihil sequitur

1 Introduction

Dating back to Aristotle, the classical principle ex con­ tradictione sequitur quodlibet has been considered funda­ mental by most logicians and philosophers. Clearly, it makes sense for mathematics 1 where it amounts to the postulate that contradictions in a theory must not be tol­ erated and have to be removed, otherwise the theory as a whole should be rejected as meaningless. This postulate, however, is neither acceptable for the logical modeling of cognitive processes nor for a semantics of databases, respectively knowledge bases, where the logic is required to be an adequate tool for information processing rather than a metaphysically correct theory.

In AI, notably in the field of knowledge representation and automated reasoning, inconsistency handling plays a crucial role:

• it is a real problem for expert system shells which don't seem to deal with it in a principled way

·The present paper extends ideas presented in [Wagner 1990a].

1 But even for mathematics some people, e.g. Wittgenstein [1956], have questioned it.

• it is the main issue of many nonmonotonic for­ malisms such as default logic, inheritance networks, defeasible reasoning and belief revision
• it will be a major issue in logic programming where - this is a forecast - negative conclusions will be allowed in future systems 2

There have been several suggestions to apply paraconsis­ tent logics in AI. 3 But the principle of paraconsistency, {p, "'P} If q, does not imply an answer to the question whether a derivation may rely on possibly contradictory information or not . Also in the aforementioned work this question was not addressed. 4 Usually, in paraconsistent logics contradictory sentences are accepted as a basis for further derivations. This corresponds to the 'dialethic' standpoint of e.g. Priest (1989] according to which a con­ tradictory sentence counts as both true and false , simul­ taneously: {p, ""P} f- pas well as {p, ""P} f- ""P·

From an information processing point of view, how­ ever, it seems to be more natural to discard contradictory information as neither true nor false, so it cannot be used in the derivation of further information: {p, ""p} If p as well as {p, ...... p} If ""'P· This view seems to be shared by Perlis (1989]: "when a contradiction is found in our reasoning we tend to notice that fact and take corrective action, such as temporarily suspending beliefs in one or both conflicting beliefs."

While in many other formalisms (in belief revision 5 , for instance) the logic is extended by adding a certain higher-level apparatus, our aim is to establish a basic­ level logical system capable of handling contradictory in­ formation in a satisfactory way.

2 The theoretical basis for this is discussed in [Pearce & Wagner 1989], [Gelfond & Lifschitz 1990], [Kowalski & Sadri 1990), [Wagner 1990b].

3 e.g. [Blair & Subrahmanian 1989], [Kifer & Lozinskii 1989], {da Costa et al. 1990), [Subrahmanian 1990]

4 Subrahmanian (1990] remarks as a criticism of the 4-valued approach of (Blair & Subrahmanian 1989] that we should not be allowed to use inconsistent information to draw further conclusions. However, no solution to this problem is offered.

5 cf. (Gii.rdenfors 1988]

2 Informal Presentation

We assume that a KB consists of rules, conclusion +­ premise, representing positive, resp. negative, conditional information. A fact can be represented as a rule with an empty premise, or, in an alternative notation, with premise 1, the verum, which is trivially accepted. Instead of conclusion +-- 1 we shall also simply write conclusion as an abbreviation. The following is an example of a KB in this sense:

2.1 Liberal Reasoning

The notions of liberal support and acceptance are defined by the following clauses:

(1) 1 is supported.

(support) A conclusion is supported if the KB contains a rule for it the premise of which is supported.

(accept) A conclusion is accepted if it is supported.

We denote the consequence operation collecting all lib­ erally accepted conclusions by LC,

Notice that certain conclusions are accepted together with their resp. contraries, i.e. they are simultaneously accepted and rejected. In order to avoid this strange situation acceptance should be defined in another way.

2.2 Semi-liberal Reasoning

The simplest contradiction banning modification of lib­ eral reasoning would be to delete all contradictory con­ clusions from LC(KB). The definitions of (1) and (sup­ port) from liberal reasoning are retained. Additionally, we have

• (doubt) A conclusion is doubted if its contrary is sup­ ported.
• (accept) A conclusion is accepted if it is supported and not doubted.

(reject) A conclusion is rejected if it is doubted and not supported.

The resulting consequence operation, collecting all semi­ liberally accepted conclusions, is denoted by LC'. In our example KB1, p and q are no longer accepted con­ sequences, since they are not only supported but also doubted. Only r and s are accepted, LC' (KB1) = { r, s}. At first glance this looks like we had cleaned up the mess of LC(KB!). But if we really don't want to accept con­ tradictory conclusions we should also ban them from en­ tering into derivations. Consequently, r should not be derivable since it depends on q which is contradictory.

One possible solution consists in a seemingly small change in the definition of support.

2.3 Conservative Reasoning

Conservative reasoning requires the premise of a rule to be accepted (and not only supported) in order that the conclusion be supported. (1), (doubt), (accept) and (re­ ject) are as above. Additionally, we have now

(support) A conclusion is supported if the KB contains a rule for it the premise of which is accepted.

Concerning KB1, this means that p is not accepted, since it is both supported and doubted, consequently q is not supported by q +-- p, but only doubted, by ....., q, hence ....., q is accepted. Also, s is accepted, and r is not . Thus, we obtain the following set of conservative consequences, CC(KB1) = {-q,s} . The interesting point here is that, by our redefinition of support, we have also redefined the concept of contradiction. So, in comparison with liberal and semi-liberal reasoning, we not just lose conclusions based on contradictions, but we also lose contradictions, and consequently, gain new conclusions.

2.4 Skeptical Reasoning

We might not want to rely on conclusions which are, al­ though not conservatively, but liberally doubted. As real skeptics we are not willing to accept any possibly incon­ sistent information. That is, we would not accept -q as a conclusion from KB1, since there is some evidence for the premise of a contrary rule, p (though there is evi­ dence for "'P, as well). This is achieved by (1), (support), (accept) and (reject) as in conservative reasoning, and a stronger notion of doubt,

(doubt) A conclusion is doubted if its contrary is liber­ ally supported.

According to skeptical reasoning we obtain the following set of skeptical consequences, SC(KB 1) = { s}.

2.5 Discussion

LC', CC and SC are nonmonotonic: the addition of new information to the KB may cause new contradictions in­ validating previously accepted conclusions. The question now is: which of LC, LC', CC and SC is the most appro­ priate consequence operation for knowledge bases. From the above example it becomes clear that LC' is not a good choice. It represents a bad compromise between liberal and skeptical reasoning. Obviously, LC is compu­ tationally cheaper than CC and SC which require two­ fold recursion. 6 So, it could make sense first to check the liberal derivability of a query, and if it succeeds, check in a second step whether it is grounded in noncontradic­ tory information, i.e. conservatively, or even skeptically, derivable.

6 SC seems to be computationally cheaper than CC.

But there might also be domains of application where the liberal rationale is perfectly reasonable and the con­ servative and skeptical reasoning procedures are too re­ strictive.

Example 2 Consider

It is conceivable that in certain cases both treatments are applicable since, due to the vagueness of the measure­ ment method, the first measurement might yield 37.3 and the second one 36.8, so we would obtain fever and also -fever by liberal reasoning. Both by conservative and skeptical reasoning the patient would not get any treat­ ment, since neither fever nor -fever would hold.

The difference between conservative and skeptical rea­ soning consists in the resp . concept of contradiction. A conclusion is considered contradictory if it is both sup­ ported and doubted. Skeptical doubt is much stronger than its conservative counterpart which allows for con­ clusions not acceptable to a skeptic.

We propose to use LC, CC and SC as complementary options in knowledge-based reasoning.

3 The Formal System

The language of KBs consists of the logical operator sym­ bols/\, V,....., and 1 standing for conjunction, disjunction, negation and the verum, respectively, predicate symbols, constant symbols, and variables. Notice that there are no function symbols and no explicit quantifiers.

A literal is either an atom or a negated atom (if it is neither 1 nor ....., 1 it is called proper) . We use a, b, . .. , I, k, ... and F, G, H, ... as metavariables for atoms, liter­ als and formulas, respectively. A variable-free expression is called ground. A KB consists of clauses of the form I +- F. We consider such clauses as specific inference rules expressing conditional facts, and not as implica­ tional formulas . A rule with premise 1 is also called a fact, and we abbreviate I +- 1 by I. Examples of clauses are -flies(x) +- emu(x)Vpenguin(x) or switch_onJight +- dark 1\ ....., illuminated.

We consider a KB containing non-ground clauses as a dynamic representation of the corresponding set of ground clauses formed by means of the current domain of individuals U and denoted by [KB]u. Formally,

where u ranges over all mappings from the set of vari­ ables of I and F into the Her brand universe U. We call u a ground substitution for I+- F and [KB]u the Herbrand expansion of KB with respect to a certain Herbrand uni­ verse U. We shall write [KB) for the Her brand expansion of KB with respect to the Herbrand universe UKB of KB.

We shall formulate our system proof-theoretically 7 by defining a derivability relation between a KB and a well­ formed formula in the style of a natural deduction system by means of the introduction rules (1),(/\),(- /\), (--) and (x) . 8 We first present the deduction rules for com­ plex formulas. We write "KB ~ F, G" as an .abbreviation of "KB ~ F and KB ~ G".

where F and G are ground formuas, and a non-ground formula is provable if some ground instance of it is,

We also stipulate that for any KB, KB 1- 1. The rules for disjunction, (V) and (....., V), are derivable according to the DeMorgan identities.

In order to complete this definition of derivability rel­ ative to a KB we have to specify what it means for a ground literal to be derivable, i.e. the rule (1) . While liberal, conservative and skeptical derivabiltity have the same rules for complex formulas,(/\), (- /\), (--), (x) , they differ in the base case, (/), which is defined in the next sections.

Notice that we do not have a 'trivialization rule', so as to conclude anything from a contradiction. The principle ex contradictione sequitur quodlibet, {F,....., F} ~ G, which is fundamental in classical and intuitionistic logic, has been dropped. Furthermore, in the conservative and in the skeptical system, we replace it by the principle ex contradictione nihil sequitur.

4 Well-founded KBs

Concerning the recursive structure of a KB, the most straightforward way to define liberal derivability for ground literals is the following

7 Notice that this seems to be the most natural way to define cognitively interesting nonstandard logics such as relevance logics, default logic, or the defeasible reasoning procedure of Nute, which all have in common that they have no simple and intuitively con­ vincing model theory.

8 There is no need for elimination rules because t- does not allow for arbitrary formulas in the premise.

However, this definition only works for 'well-behaved' KBs which we call well-founded according to the defi­ nition below. In other cases it enters a loop. 9

In order to say what it means for a KB to be well­ founded we need a few definitions. We define DNS(F), the disjunctive normal set of a formula F as follows:

With this the disjunctive normal form of a formula G can be obtained as

For a ground literal I we define Pre 1 ( /), the set of its single-step literal predecessors, Prei ( /), the set of its ith­ step literal predecessors, and Pre(/), the set of all proper ground literals preceeding it in KB:

Intuitively speaking, Pre(/) collects all ground literals on which the derivability of I possibly depends.

A KB is called well-founded, iffor every I +-- F E [KB) we have I fl. Pre(/). It is called strongly well-founded if ~or every I +-- F E [KB] we have I fl. Pre(/) and also I fl. Pre(/), where ,;:a = a and ii = ...... a.

For example, KB = {q, p +-- q, q +-- ""'P} is well­ founded but not strongly weli-founded since ...... p E Pre(p) .

For strongly well-founded KBs we can define conser­ vative and skeptical derivability, 1-e and 1- 3 , as follows:

Notice that these definitions are twofold recursive. Conservative derivability excludes only those contradic­ tory information the derivation of which does not itself rest on other contradictions, whereas skeptical derivabil­ ity also discards information as contradictory if its incon­ sistency is caused by other contradictory information.

We denote the resp. consequence operations associat­ ing the set of liberal, conservative and skeptical conse­ quences with a KB, {F: KB 1-. F} where *=I, c, s, by LC(KB), CC(KB) and SC(KB) .

9 This problem does not arise in standard logic where the notion of derivability is not operational but simply requires the existence of a proof.

Observation 1 SC(KB) ~ CC(KB) ~ LC(KB) ·:

Example 3 KB2 = {""'P, r, q +-- ""'P, s +-- r, -q +-- r, ...... r +-- p, ...... s +-- q 1\ r} is strongly well-founded. Thus, applying the resp. recursive derivability procedures we ob­ tain

5 Non-Well-Founded KBs

The simplest case of a non-well-founded knowledge base is KB = {p +-- p}. Clearly, we are interested in a decid­ able derivation procedure yielding KB fi p. In order to intercept such looping situations in the course of deriva­ tion we introduce an 'index' to the derivability relation. Let L be an arbitrary set of ground literals. First, we stipulate that (KB,L) 1-. 1 for*= l,c,s. Then we de­ fine

• (KB, L) 1-r I iff 3(1 +-- F) E [KB] 3K E DNS(F) : (i) Kn(LU{/})=0,and (ii) Vk E K : (KB, L U {/}) l-1 k

Nat ural cases of not strongly well-founded rules arise, for example, when incompatibility between predicates is ex­ pressed like in KB3 = {r(n), -q(x) +-- r(x), -r(x) +­ q(x)} where r and q ('being a republican' and 'being a quaker') are incompatible. Although such incompatibil­ ity rules are not strongly well-founded we want to employ them in derivations if possible. So, we want to be able to conclude from KB3 that Nixon, since being a republican, is not a quaker. For an arbitrary set A of ground atoms and an arbitrary KB we define:

(KB, A) 1-e I iff 3(1 +--F) E [KB] 3K E DNS(F) :

• (i) k n (A U { i}) = 0, and
• (ii) Vk E K: (KB, AU {f}) 1-e k, and
• (iii) 'V(l +--G) E [KB] VK E DNS(G) 3k E K: (KB, AU {f}) fie k

(KB,A) 1-, I iff

• 3(/ +-- F) E (KB] 3K E DNS(F) :
• (i) kn(Au{i}) = 0, and
• (ii) V k E K : (KB, AU { f}) 1-, k, and
• (iii) V(l +--G) E [KB] VK E DNS(G) 3k E K : (KB,AU {f}) fir k

where a=~= a and k = {k : k E K} .

Notice that condition (i) in the above definitions pro­ vides a kind of loop-checking.

Observation 2 (i) For every well-founded KB, KB 1-r I iff (KB, 0) l-1 I.

(ii) For every strongly well-founded KB, KB 1-. I iff (KB, 0) 1-. I for*= c, s.

This is because well-foundedness guarantees that condi­ tion (i) of the definition will be satisfied (proof by induc­ tion on the degree of 1). Thus, we can define derivability for general, not necessarily (strongly) well-founded, KBs by

Example 4 The following KB (about the barber shav­ ang anyone not shaving himself) is not strongly well­ founded,

We have SC(KB4 ) = {-s(b, b), -s(c, c), s(b, c)} since the only contrary rule for -s(b, b) fails through the loop check: (KB4, {"' ;{b: b)}} If. s(b, b) .

6 Relation to Other Formalisms

The logics of liberal, conservative and skeptical reasoning are non-classical. For instance, the law of the excluded middle is not a tautological consequence: in general, p V "'pis neither valid in liberal, nor in conservative, nor in skeptical reasoning. Rather, liberal derivability cor­ responds to a certain fragment of the paraconsistent constructive logic N- of Nelson [1949; Almukdad & Nelson 1984).

While liberal derivability is adequate with respect to general partial models 10 , or, equivalently, 4-valued mo­ dels11, the model theory for conservative and skeptical reasoning is still under investigation. It seems that a preferred model approach within general partial se­ mantics is needed.

Conservative and skeptical reasoning can be viewed as generalizations of ambiguity-blocking and ambiguity­ propagating skeptical inheritance. In fact, Ex. 1 is the logical representation of a net which illustrates the difference between these two strategies.

Conservative reasoning corresponds to Nute's de­ feasible reasoning procedure in the following way: if all clauses of a KB are considered to be defeasible rules in the sense of [Nute 1988), then our concept of conser­ vative consequence essentially agrees with the concept of consequence in Nute's formalism (without specificity defeat).

There is also a close connection to the partial logic of normal defaults 12 which is defined as follows . Let D be a set of normal 'conclusion unary' defaults, F : I I I, and r D an operator taking a set of literals to a set of literals, r D : 2Lit - 2Lit with r D (X) defined as the smallest set such that IE fv(X) whenever fv(X) 1- F & i ~X for all ground defaults F :I I I E [D) . E is called a partial default extension for D if fv(E) = E. Now, if all the clauses of a KB are considered to be normal defaults, i.e. 1 +- F is identified with F : 1 I 1, we can state Observation 3 For every KB, and every partial de­ fault extension E of KB, we have SC(KB) ~ E ~ LC(KB).

10 cf. [Langholm 1988)

11 cf. (Belnap 1977)

12 Default logic was introduced by Reiter (1980) .

7 Future Work

The logics of liberal, conservative and skeptical reason­ ing can be extended by adding another negation allow­ ing for the processing of implicit negative information in the spirit of negation-as-failure. This has been done for liberal reasoning in [Wagner 1991) where the resulting system is called vivid logic. This system and its conserva­ tive and skeptical variants seem to be a kind of common background logic for such areas like default logic, defea­ sible inheritance, generalized deductive databases 13 and generalized logic programs 14 .

For the model theory of the above systems we think that general partial semantics is a promising framework . As soon as we want to add a genuine implication to our systems we expect to end up with some kind of possible worlds semantics.

The addition of inconsistent hypothesis to a KB does not require any belief revision in our system. It should be interesting to compare the approach to inconsistency handling described in this paper with the 'consistency maintenance' approach of belief revision formalisms where contradictions have to be detected and eliminated. We expect computational advantages of our approach.

8 Concluding Remarks

We have presented a simple and natural nonmonotonic formalism for dealing with contradictory information. Since it is given by a recursive proof theory, it is computa­ tionally feasible . 15 By comparison with default logic and defeasible inheritance we obtained some evidence that it might be the logical kernel of inconsistency-tolerant rea­ soning.