A Four-Valued Fuzzy Propositional Logic

1 Introduction

The management of uncertainty in inference systems is an important issue due to the imperfect nature of real world information. There are several fields in which this information has to do with vague concepts, i.e. concepts without clear definition. The key fact about vague con­ cepts is that while they are not well defined, propositions involving them may be quite well defined. For instance, the boundaries of the Mount Everest are ill defined, whereas the proposition stating that the Mount Ever­ est is the highest mountain of the world is definite, and its definiteness is not compromised by the ill-definitess of it's exact boundaries. Propositions of this kind are called fuzzy propositions. Each fuzzy proposition may have a degree of truth between [0, 1]. On the other hand, there exists propositions which are true or false, but due to the lack of precision of the available information we can in general only estimate to what extend it is possible or necessary that they are true. This kind of propositions are called uncertain propositions. For example, the con­ cept triangle is well defined, but we can only estimate to what extend it is possible that e.g. a shape in a picture is a triangle if the segments are not exactly bounded. Certainly, any combination of the two is possible, e.g. uncertain fuzzy propositions are fuzzy propositions for which the available reference information is not precise.

In this paper we will concentrate our attention to ( cer­ tain) fuzzy propositions. In particular, fuzzy proposition we will handle are of the form [A~ n] (where A is a proposition and n E [0, 1]) and have intended meaning "it is certain that the degree of truth of A is at least n". But, rather mapping [A ~ n] as usual into true or false (as e.g. in [Chen and Kundu, 1996]) , we will give to it a four-valued semantics. This will be done by map­ ping [A~ n] into an element of 2{t.J}, where {t}, {!}, 0 and { t , !} stand for the four truth values true, fals e, un­ known and contradiction, respectively, as in [Levesque, 1984] . A first consequence of this semantics is that in certain "useful" circumstances the deduction process is tractable from a computational point of view. A second consequence is that the semantics enables us to deal with inconsistencies as the four-valued logic we will adopt is known to be paraconsisterit (see, e.g. [Wagner, 1991]) .

Our four-valued fuzzy semantics has been shown to be useful in the area of content-based retrieval of multime­ dia data [Meghini et al., 1997]. In this context the (se­ mantic) content of e.g. an image region r is described by means of fuzzy propositions like "r represents the Mount Everest with degree ~ 0.8". Since images (or any otlH'r media) are the subjective work of their authors, contra­ dictions could arise among their content representations (possibly together with domain knowledge), which typi­ cally may not be the subject of a belief revision process .

This paper is organised as follows. In the next section we will briefly resume some aspects of the four-valued logic we are based on and in Section 3 we will extend it to the fuzzy case. In Section 4 we will extend our logic by allowing a sort of conditional reasoning 1 . Calculi for deciding entailment will be given for all logics presented and Section 5 concludes.

2 Four-valued propositions

The four-valued logic we will base our work on is essen­ tially [Belnap, 1977; Levesque, 1984]. Let £ be the lan­ guage of propositional logic, with connectives A. v and ·. We will use metavariable A, B , C, ... and p, ,q, r , ... for propositions and propositional letters, respectively 2 . Negation Normal Forms (NNF) and Conjunctive Normal Forms ( CNF) are defined as usual.

A four-valued interpretation I maps a proposition into an element of 2{t ,f} and has to satisfy the following equations: t E (A 1\ B)I iff t E AI and t E BI; f E (A 1\ B)I iff f E AI or f E BI; t E (A V B)I iff t E AI or t E BI; f E (A V B)I iff f E AI and f E BI; t E (·A? iff f E AI and f E (·A)I iff t E AI. It is worth noting that a two-valued interpretation is just a four-valued inter­ pretation I such that AI E {{t}, {!}},for each A. We might characterise the distinction between two-valued and four-valued semantics as the distinction between im­ plicit and explicit falsehood: in a two-valued logic a for­ mula is (implicitly) false in an interpretation iff it is not true, while in a four-valued logic this need not be the case. Our truth conditions are always given in terms of belongings E (and never in terms of non belongings ¢) of truth values to interpretations.

1 Notice that in our basic logic modus ponens is not a valid rule of inference.

2 All metavariables could have an optional subscript.

Let I be an interpretation, let A, B be two proposi­ tions and let E be a set of propositions, called Know l­ edge Base (KB): I satisfies (is a model o/) A iff t E AI; A and B are equivalent (written A ::::4 B) iff they have the same models; I satisfies (is a model o/) E iff I is a model of A, for all A E E; E entails A (written E F4'A) iff all models of E are models of A. Without loss of gen­ erality, we can restrict our attention to propositions in NNF only, as -.-.A ::::4 A, ·(A 1\ B) ::::4 -.A v -.B and ..,(A VB) ::::4 -.AI\ -.B hold. For ease of notation, we will often omit braces, thus writing e.g. A, B F4 C in place of {A, B} F4 C and F4 A in place of 0 F4 A.

Relation 1 The following relations can easily be veri­ fied: 1. A ::::4 B does not imply -.A ::::4 -.B (and vice­ versa), 2. A 1\ B F4 A, 3. A F4 B and B F4 C implies A F4 C, A F4 A VB, A 1\ (·A VB) ~4 Band E F4 A implies E F2 A, where F2 is the classical two-valued entailment relation. Note that there are no tautologies, i.e. there is no A such that F4 A. Moreover, every KB is satisfiable. Hence, A 1\ -.A ~4 B, as there is a model I (AI= {t,f}, BI =0) ofA/\-.A not satisfying B. ·

Certainly, not allowing modus ponens is penalizing. But, we will include this form of inference in the extended language c+ described in Section 4.

2.1 Deciding entailment in£

Effe<:;tively deciding whether E F4 A requires a calcu­ lus. A well known algorithm for deciding entailment in £is Levesque's algorithm [Levesque, 1984]: in order to check whether A F4 B, we put A and B into an equiv­ alent CNF (say C and D) and verify whether for each conjunct Dj of D there is a conjunct Ci of C such that Ci ~ Dj, where Ci and Dj are clauses. Hence, entail­ ment between two propositions C and D in CNF can be verified in time O(ICIIDI), whereas checking whether A F4 B is a coNP-complete problem in the general case. We propose an alternative calculus which ( i) does not require any transformation into CNF, (ii) has the same polynomial complexity for the CNF case and (iii) is easy extensible to the treatment of conditional rea­ soning which will be the topic of Section 4. The calculus we have developed is one inspired on the calculus KE [D'Agostino and Mondadori, 1994]. The calculus, a se­ mantic tableaux, is based on signed propositions of type a ("conjunctive propositions") and of type f3 ( "disjunc­ tive propositions" ) and on their components which are defined as usual [Smullyan, 1968]3:

T A and NI' A are called conjugated signed propositions and with f]f we indicate the conjugate of f3i. An interpreta­ tion I satisfies TA iff I satisfies A , whereas I satisfies NI'A iff I does not satisfy A . A set of signed propositions is satisfiable iff each element of it is satisfiable. There­ fore, E F4 A iffTEU{NI'A} is not satisfiable, where TE = {TA: A E E} . The calculus is based on the rules:

TA V B , NI"A An instance of e.g. rule (Bl) is TB . Notice that the only branching rule is (PB) (called Principle of Bivalence). As usual, a deduction is represented as a tree, called deduction tree. A branch ¢ in a deduction tree is closed iff for some proposition A , both TA and NI'A are in ¢. With S¢ we indicate the set of signed propositions occurring in ¢. A set of signed propositions S has a refutation iff in each deduction tree all branches ¢ are closed. Furthermore, we will restricted the proof procedure to the so-called canonical form [D 'Agostino and Mondadori, 1994, p. 299] : a proposition is AB­ analysed in a branch ¢ if either ( i) it is of type a and both a 1 and a 2 occur in ¢; or ( ii) it is of type f3 and ( iia) if f]f occurs in ¢ then fJ2 occurs in ¢, ( iib) if !3~ occurs in ¢ then /31 occurs in ¢. A branch is AB-completed if all the propositions in it are AB-analysed. A proposition of type f3 is fulfilled in a branch ¢ if either fJ1 or fJ2 occurs in ¢. We say that a branch ¢ is completed if it is AB­ completed and, every proposition of type f3 occurring in ¢ is fulfilled. A deduction tree is completed if all its branches are completed. The procedure Sat(S) below determines whether S is satisfiable or not .

Algorithm 1 (Sat(S))

Sat(S) starts from the root labelled S and applies the rules until the resulting tree is either closed or completed. If the tree is closed, Sat(S) returns false, otherwise true. At each step of the construction the following steps are performed:

1. select a branch </> which is not yet completed;
2. expand</> by means of the rules (A) , (Bl) and (B2) until it becomes AB-completed, generating branch ¢>';
3. if</>' is neither closed nor completed then
4. (a) select a proposition of type f3 which is not yet ful­ filled in the branch;
5. (c) apply rule (PB) with /31 and f3f as PH-formulae and go to step 1.

otherwise, go to step 1.

The following proposition can be shown.

3 T and Nr play the role of "True" and "Not True" , respec­ tively. In classical calculi Nr may be replaced with F ( "False").

·

Proposition 1 Let S be a set of signed propositions in £. Then Sat(S) iff S is satisfiable. --1

Example 1 It can easily verified that a canonical proof of p V (q 1\ r) f=4 (p V q) 1\ (p V r) starts with S = {Tp V (q 1\ r), Nr(p V q) 1\ (p V r)} and generates two branches ¢1 and ¢2, by using fJ1 = Nr(p V q) and {3f = T(p V q) as PB-formulae, such that S¢ 1 = S U {Nrp V q, Nfp, Nfq, Tq 1\ r, Tq, Tr} and S¢ 2 = S U {Tp V q, Nfp V r, Nfp, Nfr, Tq 1\ r , Tq , Tr }. Both ¢1 and ¢2 are closed. ·

If E and A are in CNF 4 , then rule (PB) is not needed, i.e. we can eliminate Step 3. from Sat . Hence, any de­ duction tree will have one branch. As a consequence, by observing that E F4 A1 1\ . .. An iff for each 1 ::; i ::; n E F4 Ai, it can be shown that

Proposition 2 If E and A are in CNF then checking E F4 A can be done in time O(IEIIAI) using Sat. --1

Two-valued soundness and completeness is obtained by extending signed propositions as usual: ( i) T-,A i$ of type a and NrA is its a 1 and a2 component; (ii) Nf-,A is of type a and TA is its a 1 and a2 component. Just notice that in this case Sat is exactly the canonical procedure for KE [D'Agostino and Mondadori , 1994].

3 Fuzzy propositions

Now, we extend our propositional language .C to the fuzzy case. A fuzzy valuation is a function mapping propositions into [0, 1]. Consistently with our approach of distinguishing explicit from implicit falsehood (i.e. distinguishing f E AI from t ¢AI) we will use two fuzzy valuations, I · It and I · If : lA It will naturally be inter­ preted as the degree of truth of A, whereas lA If will anal­ ogously be interpreted as the degree of falsity of A. Clas­ sical "two-valued" fuzzy propositions I · It and I · If are such that IAif = 1-IAit, for each A. In our case, instead, we might well have IAit = 0.6 and IAif = 0.8. This is a natural consequence of our four-valued approach.

A (certain) fuzzy proposition is an expression of type [A~ n], where A is a proposition in .C and n E [0, 1]; .C/ is just the set of fuzzy propositions. For instance, [ItsCold ~ 0.7] is a fuzzy proposition meaning that it is certain that the degree of truth of It sCold is at least 0. 7, while [ItsCold ~ 1] means that it is definitely cold. On the other hand [-,ItsCold ~ 0.7] means that it is certain that it is likely to be not cold, while [-,ltsCold ~ 1] may be interpreted as saying that it is definitely not cold. [A~ n] is in CNF whenever A is.

A fuzzy interpretation I is a triple I = (( :)I, l · lt , I · If) , where I · It and I · If are fuzzy valuations and (-)I maps each fuzzy proposition into an element of 2{t,f}. Additionally, (-/,I · It and I · If have to satisfy the following equations: lA 1\ Bit = min{IAit, IBn; !A 1\ B!f = max{IAif, IBif}; !A V Bit = max{IAit, IBn; lA v Blf = min{IAif, IBif}; 1-,Ait = IA!f; 1-,Aif = IAit; t E [A~ nf iff IAit ~ n; and f E [A~ n]I

4 A set is in CNF iff each component of it is.

iff IAif ~ n. It is easy to see that , e.g. lA 1\ B it = 1-,A V -,Bif. Similarly for lA V Bit .

It is worth noting that there is a simple connection between the four-valued semantics given in Section 2 and the fuzzy counterpart. In fact, the above conditions can be reformulated as e. g. t E [A 1\ B ~ n]I iff t E [A ~ n] 7 and t E [B ~ n]I; and f E [A 1\ B ~ n] 7 iff f E [A~ nf or f E [B ~ nf If IAif = 1 - IAit and [A ~ nf E { {t}, {!}}, classical "two-valued" fuzzy logic is obtained.

Fuzzy satisfiability, fuzzy equivalence and fuzzy en­ tailment are defined as the natural extensions of the non fuzzy case. We will use the relation f:::t .) in place of F() whenever we refer to the fuzzy case (e .g. EP:::4[A ~ n]) . Since P:::4[A ~ 0], we will not consider those [A ~ n] for n = 0. Given a KB E and a proposition A, we define the maximal degree of truth of A with respect to E (written Maxdeg(E,A)) to be sup{n > 0 : EP:::4[A ~ n]} (sup0 = 0). Notice that E P:::4 [A~ n] iff Maxdeg(E, A)~ n .

There is a strict relation between fuzzy propositions and propositions. Given a KB E, let E be the (crisp) KB {A : [A~ n] E E} .

Proposition 3 Let E be a KB and let [A ~ n] be a fuzzy proposition. If EP:::4[A ~ n] then E F4 A. --1

Proposition 3 states that there cannot be fuzzy entailment without entailment. Hence, {[A~ 0.7], [-,A ~ 0.5]} ~ 4 [B ~ n], for all n > 0. In fact, consider an interpretation I such that IAit = 0.7, IA!f = 0.5, IB!f = 0 and !Bit=~-

Example 2 Let E be the set E = {[p ~ 0.1], [p /\ q ~ 0.5] [q V r ~ 0.6]}. Let A be p V r. One may check that E P:::4 [A~ 0.5] and Maxdeg(E, A)= 0.5. E 1=4 A is easily verified, thereby confirming Proposition 3. ·

3.1 Deciding fuzzy entailment in £)

The calculus is a straightforward extension of the procP­ dure Sat. In fact, just consider the following fuzzy signed propositions and the obvious extension of the definition of satisfiability:

By considering Sat extended to the fuzzy case, where T[A ~ n] and Nr[A ~ m] are conjugated whenever n ~ m . we obtain

Proposition 4 Let S be a set of signed fuzzy proposi­ tions in .Cf. Then Sat(S) iff S is sati.sfiable. --1

Example 3 The application of Sat to E and [A~ 0.5], as in Example 2, starts with S = TE U {Nr[A ~ 0.5]} and generates a closed deduction tree with unique branch ¢ such that S¢ = S U {T[p ~ 0.5], T[q ~ 0.6], Nr[p ~ 0.5], Nr[r ~ 0.5]}. Hence, E P:::4 [A~ 0.5]. ·

Using Proposition 4, fuzzy entailment and entailment may be shown to be in the same complexity class.

Proposition 5 Checking E~ 4 [A ;::: n] is a coNP-com­ plete problem, as is E F4 A. Given E, [A;::: n] in CNF', checking E ~ 4 [A;::: n] can be done in time O(IEIIAI). -1

One can notice that , any successful refutation of TE U{Nr[A ;::: n]} does not rely on those [B ;::: m] E E such that m < n. Hence, if we let E be a KB and consider the set En = {[A;::: m] E E: m;::: n}, then

Proposition 6 Let E be a£/ KB. Then E~4 [A;::: n] iff En F4 A. -1

As a consequence, fuzzy entailment inherits all the prop­ erties of entailment seen in Section 2 (Relation 1):

Proposition 7 Let E be a .c/ KB. If~ F4 A then there is an> 0 such that E~ 4 [A;::: n]. -1

which completes Proposition 3. Just note that Propo­ sition 6 does not hold for ~ 2 . In fact, con­ sider E1 = {[p;::: 0.2],[-.p;::: 0.3]} and E2 = {[p;::: 0.2] , [....,p;::: 0.9]}. It can easily be verified that E~· 1 f=2 q and E1~2 [q;::: 0.1], whereas E2~2 [q;::: 0.3] and Eg· 3 ~2 q.

Proposition 6 gives us a way for computing Maxdeg(E, A) in the style of the method proposed in [Hollunder, 1994]. This is important, as computing Maxdeg(E, A) , is in fact the way to answer a query of type "to which degree is A (at least) true, given the facts in E ?" The method, which requires an algorithm for computing (crisp) entailment (e.g. Sat), is based on the observation that Maxdeg(E, A) E {0} U Nr:,, where Nr:, = {n : [A;::: n] E E}, and that Em 2 En if n;::: m.

Algorithm 2

Let L: be a KB and A a proposition. Set Min= 0, Max= 2.

1. Pick n ENE such that Min< n <Max. If there is no such n , then set M axdeg(L;, A) := Min and exit.
2. Check if r;n F4 A. If so, then set Min = n and go to Step 1. If not so, then set Max = n and go to Step 1.

By a binary search on Nr:, the value of M axdeg(E, A) can be determined in O(log INr:.l) entailment tests. Hence, if E and A are in CNF, the complexity of determining Maxdeg(E, A) is O(IAIIEilog lEI) .

Example 4 Consider Example 2: Nr:, = {0.1, 0.5, 0.6}. By binary search, let n := 0.5. E 0 · 5 = {pl\q, qVr} f=4 A holds. Thus, Min := 0.5; pick n := 0.6. Now, E 06 = {q V r} ~4 A holds. Thus, Max:= 0.6. Since there is no Min < n < Max such that n E Nr:,, the procedure stops. Hence, M axdeg(E, A) = 0.5 as expected. ·

A drawback, which Algorithm 2 inherits is that checking entailment several times is generally not feasible from a practical point of view, as it could be exponential in time and Nr:, can be O(E). In Section 4.1 we will present a method where computing M axdeg(E, A) "corresponds" to performing the entailment test only once.

3.2 Relations to Possibilistic Logic

There is a strict connection between our logic and (necessity-valued) possibilistic logic [Dubois and Prade, 1986], which allows the expression of uncertain proposi­ tions. In possibilistic logics, the expressions are of type (A, Pn) and (A, Nn) . A weight Pn (resp. Nn) attached to A models to what extent A is possible (resp. necessar­ ily) true. The semantics is given in terms of fuzzy sets of interpretations, i.e. to each propositional interpreta­ tion T a weight rr(T) E [0, 1] is assigned. The possibility and necessity of a proposition is then given by II (A) = max{rr(T) : T satisfies A} and N(A) = 1 - II( ...... A). An interpretation satisfies an expression of type (A, Pn) (resp. (A,Nn)) ifii(A);::: n (resp. N(A);::: n).

A closer look to Proposition 6 reveals that it is similar to Hollunder's Theorem 3.4 in [Hollunder, 1994]:

Theorem 1 (Hollunder) Let E be a set of possibilistic propositions and n > 0. Then E f=~os (A , Nn) iff if>n F2 A , where f=ios is the possibilistic entailment relation and if>n ={A: (A,Nm) E E and m;::: n} . -1

As a consequence, let E be a £/ KB and let f: be {(A, Nn) : [A;::: n] E E}. Since p4Cf=2, from Propo­ sition 6 and Theorem 1 it follows that

Proposition 8 Let E be a£/ KB. lfEh [A;::: n] then f: f=i 08 (A, Nn) . -1

The converse of Proposition 8 is not true, i.e. "t f=ios (A, Nn) does not imply E~ 4 [A;::: n]. For instance, [p;::: 0.6],[-.p;::: 0.7] ~ 4 [q;::: 0.6], whereas (p, N0.6) , (·p,N0.7)f=i 08 (q, N0.6) and, thus, ~ 4 cf=ios holds. Nei­ ther Proposition 8 nor the converse of it holds for ~ 2 . We can confirm this by considering E1 and E2 of the pre­ vious section. Therefore, E2 ~2 [q ;::: 0.3] and "t2 ~ios (q , N0.3) , whereas E1 f)i2 [q;::: 0.1] and f:1 f=ios (q , N0.1) .

4 Conditionals

In Section 2 we have seen that modus pones is not a valid inference rule in £ and, thus, in £! . In order to deal with conditional reasoning we introduce a new con­ nective :::?. Let £+ be £ plus the set of propositions involving connective =>. From a semantic point of view, an interpretation T has also to satisfy the following con­ ditions: t E (A=> B)I ifft E AI implies t E BI, whereas f E (A=> Bl iff t E AI and f E BI . Notice, that now A , A => B F4 B holds. Moreover, ·(A => B) :::::4 A 1\ -.B, A => B ~4 -.B => ..,A (no contraposition) and F4 A => (B => A) hold. Hence, there are tautologies in £+ . As for £ , every £+ KB is satisfiable. A complete calculus with respect to £+ is obtained by extending the definition of signed propositions of type a and type (3 to the cases Nr A => B and T A => B , respectively, in a similar way as in [D'Agostino and Mondadori , 1994]. Furthermore, we extend Sat with Step 3b: if (31 is of type TA => B then let S' = (S<I>' U {NrA}) \ {TA => B} and if not Sat(S') then expand ¢' by means of one children node labelled T B and go to step 1.

Proposition 9 Let S be a set of signed propositions in £+. Then Sat(S) (with Step 3b) iff Sis satisfiable. -I

Checking whether ~ F4 A is a coNP-complete problem in £+. But, if we restrict £+ to£+ we obtain a tractable logic. z+ is defined inductively as follows: z+ is the min­ imal set such that ( i) every proposition in £ in CNF is in Z+; (ii) if A, A1, ... , An and B, B1, ... , Bm are literals in£, then both A11\ ... /\An::::} Band A::::} B1 V ... V Bm are in Z+. By considering that Step 3. can be eliminated (rule (PB) is not necessary), we have

Proposition 10 Let~ be a£+ KB and let A be in Z+. Checking if~ F4 A can be done in time O(I~IIAI). -I

Now, let £~ be the extension of£+ to the fuzzy case. An interpretation I has now also to satisfy the semantic clauses lA ::::} Bit = min{l, ~} (Godel impli­ cation) and lA::::} B)f = min{IAit, IBif}. It is worth noting that lA::::} Bl = lA 1\ --.Bit, whereas lA::::} Bit f. 1--.B ::::} --.Ait (no contraposition). The clause for lA::::} Bit models a sort of conditional Cond(BIA) = 11~~:11. It is easily verified that the above conditions are equivalent to: t E [A::::} B ~ nf iff Vm E [0, 1], if t E [A ~ mf then t E [B ~ n · mf; f E [A::::} B ~ nf iff t E [A~ nf and f E [B ~ nf, which are similar to the non fuzzy case. The semantics for £~ enables thus a simple form of modus ponens: [A ~ m], [A ::::} B ~ n] ~4 [B ~ n · m]. Just notice that if l·lt, 1·1/ E {0, 1} then classical two-valued ::::} is obtained.

Example 5 Let~= {[J::::}SAA~0.9], [B::::} T ~ 0.4], [G ::::} A ~ 0.9], [A ::::} T ~ 0.8], [K ::::} C ~ 0.7], [C ::::} T ~ 0.2], [S ::::} T ~ 0.5] }, where J, S, A, B, T, G, K and C stand for Jon, Student, Adult, Boy, Tall, Gil, Karl and Child, respectively. Then ~u{[� ~ 0.8]} ~4 [T ~ 0.576], ~U{[J ~ 0.7]} ~ 4 [T ~ 0.504] and ~U{[� V K ~ 0.8]} ~4 [T ~ 0.112] (the values are maximal). ·

Note that F4 [A::::} (B::::} A) ~ 1] holds, whereas if Cis (p ::::} q) V ( (p ::::} q) ::::} q) then F4 C and ti6 4 [C ~ n], for all n > 0. In fact, let I be an interpretation such that !Pit = i and lqlt = n 3 2 . ICit = 2 ; < n holds. As a consequence, Proposition 7 is not valid in £~, whereas Proposition 3 and Proposition 8 remain valid 5 .

4.1 Deciding entailment in£~

Unfortunately, finding a calculus for entailment in£~ is not as easy as for £!, since Algorithm 2 does not work in the context of£~: Proposition 6 does not hold and M axdeg(~, A) may be not in {0} U Nr:,.

First, we generalise fuzzy propositions to the form [A ~ A], where A is a fuzzy value defined as follows. Let X be a new alphabet of fuzzy variables (with metavari­ able x). A multiset, (with metavariable L) is a finite set of fuzzy variables in which a variable x can occur more than once. A fuzzy value (with metavariable A) is a pair (n, L) where n E [0, 1] and L is a multiset. An interpretation I is such that xi E [0, 1], {x1, ... , xnf = X1I · ... · Xni, 0I = 1 and (n., L)I = n · LI. We ex­ tend the multiplication function · to fuzzy values by defining (n, L1) · (m, L2) as (n · m, L 1 U L2). For ease of notation we will write 0, n and x in place of (0, L), (n,0) and (1,{x}), respectively. Moreover, we will al­ low fuzzy values ~ and A~ ( n, m are positive integers) with obvious semantics. The greater equal relation ~ is extended to fuzzy values as follows: A1 ~ A2 iff for all interpretations I, A1I ~ A2I . Similarly for the re­ lation >. Checking whether A1 ~ A2 can be done by observing that (n, L) ~ (m, L') iff n ~ m and if m f. 0 then L ~ L'. The reader can verify that it is deter-~ ~ minable whether ~ ~ ~ and At 1 ~ A;' 2 . For instance, 0.7·x1 ~ 0.6·x1·X2, whereas (0.9-xl)! ~ (0.5·x1·x2)! , since (0.9 · x1) 2 ~ (0.5 · x1 · x2) 3 .

5 Note that (p,Nm), (p => q,Nn) Hos (q,Nmin{m,n}) holds and n · m :S min{m,n}.

In what follows, we will use the obvious extension of the definition of satisfiability with the following clauses on signed propositions involving ::::}: (i) Nr[A::::} B ~ A] is of type a:: and T[A ~ x] and Nr[B ~ A· x] are its a:: 1 and 0::2 components (for a "new" fuzzy variable x), and (ii) T[A::::} B ~ A1] is of type (3 and Nr[A ~ A2] and T[B ~ A1 · A2] are its (31 and (32 components (for a all A2). Moreover, T[A ~ A1] and Nr[A ~ A2] are called con­ jugated signed propositions if A1 ~ A2.

Algorithm MaxVal(S, A) below computes the set of maximal fuzzy values A1 , ... , An for which S U {Nr[A ~ Ai]} is not satisfiable. If MaxVal(T~,A)={ n}, where n E [0,1], then Maxdeg(~,A) = n, otherwise M axdeg(~, A) = 0.

Let ¢>i be a not closed and completed branch of a de­ duction tree and x a fuzzy variable. Let Ni be the set of all fuzzy values A such that (i) both T[A ~ xn 1 · A1] and Nr[A ~ Xn 2 · A2] are in S<l>i, where n 1 + n2 ~ 1 and n1 f. n2; (ii) if n1 < n2 then A= (~)"2~"1; (iii) if n1 > n2 then A = ( ~) n1 ~n2 . Ni is just the set of fuzzy values A such that ¢>i is closed whenever x is substituted by A, i.e. T[A ~ xn 1 · A1] and Nr[A ~ xn 2 · A2] will be a conjugated pair. It can be verified that 0 :s; A :s; 1.

Algorithm 3 (MaxVal(S, A))

Let the root node be labelled with S U {Nr[A ~ x]}, where x is a new fuzzy variable. At each step of the construction of a deduction tree the following steps are performecf:

1. select a branch </> which is not yet completed;
2. expand</> by means of the rules (A), (Bl) and (B2) until it becomes AB-completed. Let </>' be the resulting branch;
3. if</>' is neither closed nor completed then
4. {a) select a proposition of type (3 which is not yet ful­ filled in the branch;

6 The branches </>will be maintained maximal, i.e. not both T[A ~ AI] and T[A ~ A2] are in s<~> with A2 > A}. Moreover , T[A ~OJ if. s<~>. Similarly for case NI'.

• {b) if fJ1 is of type T[A =? B 2 >.] then let {>.1, ... , >.1} be MaxVal(S<i>\{T[A =? B 2 >.]},A}, ex­ pand ¢' by means of one children node labelled T[B 2 >. · >.1], ... ,T[B 2 >. · >.t] and go to step 1;
• (c) otherwise apply rule ( P B) with fJ1 and (Jf as P B­ formulae and go to step 1;

otherwise, go to step 1.

1. for all not closed and completed branches ¢; {1 ::; i ::; h) let n; : = max N; (max 0 = 0); for all closed and completed branches ¢; {h + 1 ::; i ::; k} , let n; := 1. MaxVal(S, A) := min{n1 , ... nk} . ·

Just notice that Step 3b is not needed in .C). Moreover, the procedure can be improved by performing Step 4. during Step 2. - 3. It can be shown that

Proposition 11 Let E be a£~ KB and A E £+ . Max­ deg(E,A) = n > 0 iff MaxVal('rE,A) = {n}, and check­ ing M axdeg(E, A) 2: n is a coNP-complete problem. -I

Example 6 Consider Example 2. MaxVal(TE, A) gen­ erates two branches ¢1 and ¢2, where S¢ 1 := S U {T[q 2: 0.6]}, S¢ 2 := S U {Nr[q 2: 0.6], T[r 2: 0.6]} and S ={T[p 2: 0.5], T[q 2: 0.5], Nr[p 2: x],Nr[r 2: x]} . Now, N1 = {0.5}, n1 =0.5, N2={0.5, 0.6} and n2 = 0.6. Hence, Maxdeg(E, A)=min{nt, n2} = 0.5. ·

Example 7 Let A be (p ==:. q) v((p ==:. q) ==:> q). We have seen that F4 A, whereas 1564[A 2: n], for all n > 0. Compute MaxVal(0, A). The computation generates an unique branch ¢ such that S<i> contains T[p 2: x1], Nr[q 2: x · x1], T[p ==:> q 2: x2] and Nr[q 2: x · x2]. By Step 3b, a recursive call MaxVal(S<I> \ {T[p ==:> q 2: x2]},p) will be performed answering with {xt}, i.e. the set of maxi­ mal degrees of p with respect to S<i>\ {T[p =:>q 2 x2]}. Hence, the computation proceeds with branch ¢', where s<P' is s<P u {T[q 2: X2 . Xt]}. Finally we will have Max­ Val(0,A)={Xt,X2}· Therefore, Maxdeg(0,A) = 0. ·

-! - Finally, let £+ be the extension of£+ to the fuzzy case. In this case, it can be shown that MaxVal(S, A), with­ out Step 3. and such that Ni is computed during Step 2., can be modified in such a way that it runs in poly­ nomial time. Roughly, given e.g. {T[A 1\ B ==:> C 2: 0.6], T[A 2: 0.7], T[B 2: 0.8], Nr[C 2: x]}, rule (B1) can be ap­ plied and we add T[C 2: min{0.7, 0.8} · 0.6] to the branch and finally we get x = 0.42.

-! - Proposition 12 Let E be a £+ KB and A E £+ . Computing Maxdeg(E,A) can be done in time O(IEIIAI). -I

Note that the KB in Example 5 is a :C{ KB.

5 Conclusions

There are two main contributions in this paper. The first one is an alternative procedure to Levesque's algorithm for deciding entailment in £ (with same complexity on propositions in CNF), but which works too for £+ , i.e. C with modus ponens. The second one is the defini­ tion of the logic £~ for reasoning in presence of vague concepts and inconsistencies with an expressively power­ ful and computationally tractable case. These two parts can be furthermore combined, without affecting the com­ putational complexity, by combining fuzzy propositions [A 2: n] with the operators /\, V, · and ==:> and, thus, al­ lowing fuzzy propositions of type, e. g. [A 2: n] V [B 2: m] and [A 2: n] ==:. [B 2: m]. A decision procedure can sim­ ply be obtained by combining the algorithms for deciding entailment in £+ and the one for £~.

Uncertain fuzzy propositions can be obtained by al­ lowing expressions of type (r, Pn) and (r, Nn) , where "( is a fuzzy proposition. The development of both a pre­ cise semantics within our four-valued framework and a calculus for automated reasoning in it , can be seen as interesting topics of further research.

Acknowledgements

This work is funded by the European Community ES­ PRIT project FERMI 8134. Thanks go to C. Meghini and F. Sebastiani for their suggestions and comments.