Theorem Proving Under Uncertainty - A Possibility Theory-based Approach

1 - Introduction

Logic programming is a well-established, coherent approach to automated reasoning in art~icial intelligence, when pmpos~ions are not uncertain and pradicates are not vague. What we propose here, is to extend tha logic programming approach in order to deal w~h uncertainty in a non-ad hoc and efficient manner. First of all ~ is important to distinguish between uncertain propositions and fuzzy ones. An uncertain (non-fuzzy) propos~ion is a propos~ion in the usual sense of binary logic, for which the available knowledge does not enables us to establish with complete certainty that the propos~ ion is true or is false. Such a propos~ion has only two possible degrees of truth, namely "true" or "false", but numerical measures of uncertainty can be used for estimating the extent to which the proposition can be believed to be true or to be false. Contrastedly, a propos~ion will be fuzzy as soon as it involves a vague predicate. Then excluded-middle or contradiction laws no longer hold generally for such propositions. Only fuzzy propositions may have an intermediary degree of truth (a.g. the truth of "John is young" knowing that John is 45 years old, can be a matter of degree in a given context). See (6).

In the following we only consider the case of uncertain propos~ions. Their uncertainty will be represented by means of possibility and necess~y measures [14) [4). The appropriateness of this model with respect to other mathematically-founded framework for handling uncertainty, will be emphasized. First the extension of the resolution principle and of the refutation method to clauses weighted by necessity measures, which has been recently proposed by two of the authors (5), is briefly recalled. Then a linear strategy making use of an ordered search method is proposed in order to obtain the best possible estimation about the uncertainty of a proposition to evaluate. An illustrative example is given. Further extensions of the proposed approach, especially to cope with inconsistent sets of clauses, are briefly mentioned.

2 - Beso!utjon jn the presence of uncertaintY

2. 1. Uncertain prqQQSjtjons

Let (P, v, "· -,) be a Boolean algebra of propositions. A possibility measure TI defined on P satisfies the following axioms (14), (4)

Il(O) · o ; Il(t). 1 ; v p, v q, Il(p v q) · max(ll(p),ll(q)), (1) where 0 (rasp. 1) denotes the ever-false (rasp. ever-true) pmpos~ion ; i.e. V p e P, p "-,p · 0 and p v -,p · 1. ll(p), which belongs to the real interval (0,1) is an estimate of the degree of possibil~y that the propos~ion pis true. By duality a necessity measure N is associated with a possibility measure n according to a definition [3) which extends the usual relationship between possibil~y and necessity in modal logic ; namely N satisfies

N(p) is the extent to which the proposition p can be considered as necessarily (or certainly) true with respect to the current state of knowledge ; note that, due to (3), as soon as N(p) > o, then N(-,p) · o, i.e. two opposite propositions cannot be simultaneously considered as somewhat certainly

Didier DUBOIS -Jerome LANG - Henri PRADE

L.S.I., Universite P. Sabatier, 118 route de Narbonne, 31062 TOULOUSE Cedex (FRANCE)

true. When the propos~ion p is known or proved to be true, we have N(p) · 1 (or equivalently TI(-,p). 0) ; it entails TI(p) · 1, but ll(p) · 1 is not a sufficient condition for asserting that p is true. When the propos~ion p is known or proved to be false, -,p is true and we have N(-,p) · 1 (or equivalently TI(p) · 0). In case of total ignorance about the truth or the fals~ of p, we have ll(p) · 1, N(p) · 0. Note that we only have the following . inequal~ies

V p, V q, N(p v q) <: max(N(p), N(q)) ; ll(p" q) ~ min(ll(p), ll(q)) (4) The corresponding equalities do not hold in general. Indeed, for instance for q · -,p, we have ll(p A -,p) · 0, while we may have ll(p) > 0 and ll(-,p) > 0. More generally, it can be proved that if p entails q, i.e. p-> q. 1, then ll(q) <: ll(p) and N(q) <: N(p) where q-> p stands for -.p v q. The inequalities (4) depart from many - valued logic where we have truth - functionality, i.e. v(p A q) · min(v(p), v(q)), v(p v q) · max(v(p), v(q)) and v(-,p) · 1 - v(p) which differs from (2), where v(p) stands for the degree of truth of proposition p. This degree of truth can be related to the membership function(s) of the fuzzy set(s) which represent the fuzzy predicate(s) involved in p. Besides TI(p) and N(p) can be obtained as the result of a pattern matching procedure [1) between the contents of the proposition p represented by means of ordinary sets and the contents of the available knowledge represented in terms of possibility distributions ; see (6).

Moreover necessity measures can be extended to formulas involving predicates, by postulating that

where P is a predicate and 0 is the domain of variable x. Note that (5) is in agreement with (3) when 0 is finite, since then V x P(x) is equivalent to the conjunction P(a1) A .. . /\ P(an) where 0 · {a1, ... , an>·

Possibility and necess~y measures are an alternative to probabil~y measures for representing uncertainty ; they enable us to distinguish between the total lack of certainty in the truth of p (N(p) · 0) and the total certainty that p is false (ll(p) · 0), while in probabil~y we have Prob(p) · 0 (=~ Prob(-,p) · 1.

2.2. Besofutjon princiPle

The resolution principle (Robinson (9)) corresponds to the following pattern of reasoning in the propos~ional case

(6)

q v r is called the resolvent of the parent clauses p v q and -,p v r. The pattern (6) can be generalized to uncertain propositions und.er the form (5)

If N(p v q) <:a., N(-,p v r);., ~ then N(q v r) <: min(a..~) (7) For a. · ~ · 1, the pattern (6) is recovered. Note that the values of N(p v q) and of N(-,p v r) can be independently assigned except ~ q · r. 0, where we must have min(N(p), N(-,p)). 0 due to (3). If we know that N(p" q) <: y we can distribute the lower bound yon the elementary clauses p and q, i.e. we have N(q);., y and N(p);., y, using (3). In case the available information gives lower bounds on the literals of a clause, e.g. N(p) ;., y and N(q) ;., II owing to (4) we obtain a lower bound on the necess~y measure attached to the clause p v q, namely N(p v q) <: max(y,li). In the following we attach the greatest known lower bound of its necessity measure to a clause ; by convention this number will be written between parentheses after the clause. Note that we do not take into account upper bounds on necess~y measures in our approach. Indeed N(p) ~ y is poor information since ~ is equivalent to ll(-,p) <: 1 - y, which leaves Il(p) completely indeterminate.

Let S be a set of ground clauses. By B(S) we mean the union of S with the set of all ground clauses obtainable from S using one application of the resolution principle (i.e. all the resolvents of the pairs of members of S). Let Rn(S) be result of iterating the rule n times. Then, due to (7) and the associativity of the min operation, we can state the following ~ [5) : Lets K {C1·····Cml · Let 'Vi= 1,m, N(Ci) ~ ai. Let en denote any clause in Rn(S). Then 'V n ~ 0, N(Cn) ~ min i. 1,m ai.

This theorem expresses that the degree of certainty (expressed in terms of necessity) of any logical consequence obtained by repeatedly applying the resolution principle, will be at least equal to the one of the most uncertain parent clause. This simple result agrees w~h our intuition. M..e.J. : A pattern similar to (7) can be easily established for a set function g which is a probability measure or more generally a Shafer [1 0) belief function (see [51). Namely, we have

If g(p v q) ~a, ghp v r) ~ ~ then g(q v r) ~ max(O, a+ ~ - 1) (8) The repeated application of (8) may lead to a lower bound which is not very much informative, whatever is the quality of lower bounds attached to the parent clauses . This behavior does not exist with min. For necessity measures, which are a particular case of Shafer belief functions [3), the

lower bound in (8) is improved since min(a,b) ~ max(O, a+ b - 1 ). in [0,1). N...6..Z : Quite early in the development of fuzzy set theory, an extension of resolut ion principle was proposed by Lee [7) for ground clauses in fuzzy logic, where conjunction and disjunction are defined via min and max operations as already mentioned. Basically, it was proved that if all the truth-values of parent clauses are strictly greater than 0.5, then a resolvent clause derived by the resolution principle always has a truth-value between the maximum and the minimum of those of the parent clauses. See [5) for further discussions. Moreover, due to the lack of contradiction law for fuzzy propos~ions, the refutation cannot be easily extended as it is the case for (7) (see next section). Recently another attempt has been made by Van Emden [12) for introducing quantitative aspects in the framework of a rigorous logic programming approach. However the meaning of the so-called truth values, intermediary between 0 and 1, remains ill-defined since they are not related to some axiomatically-based modelling of uncertainty such as probability, Shafer evidence or possibility / necessity theories. Indeed thg propagation of the truth-values in [12) resembles somewhat to the ad hoc treatment of certainty factors in MYCIN (11).

The resolut ion principle for predicate calculus can be stated in the following way. Let L1 be an atomic formula, i.e. a predicate symbol of degree n followed by n terms (a constant is a term, a variable is a term, a function bearing on terms is still a term) . Let p[cr] denote the clause obtained by applying the set of elementary substitutions specified by a to the occurences of variables in the clause p. If the elementary substitution cr 1 , applied to the variables in L1 and L2, make L2 identical to ~L1. then from L1 v q and L2 v r the resolvent (q v r) [cr 1 ) can be deduced. From (5), it is

easy to see that the following pattern is valid

which extends the usual particularization mode of inference. Thus, the subst itution of a variable by a constant in a universally quantified proposition can only increase the necessity degree attached to the proposition. More generally from N('V x P(x)) ~a we can infer that N('V y P(f(y))) ~a where f is a mapping ; note that N('V y P(f(y))) may be greater than N('V x P(x)) since f is not necessarily onto. Thus the application of the resolution principle for predicate calculus is compatible with a computation of a lower bound of the necessity degree attached to the resolvent using (7) and (9).

For instance if we know that N(3 x P(x)) ~a and that N('V y P(y)-> Q(y)) 2: ~.this can be written in a logic programming style, using a Skolem constant A, as

from which we infer (applying the substitution A(y) that

This very simple example is considered by Nilsson [8) with a probabilistic modelling of uncertainty, but is not deatt with by resolution.

2.3. Refutation

A very popular way of using the resolution principle is the refutation method, i.e. the proposition to be proved is assumed to be false, and its negation is added to the set of ground clauses ; when the proposition is actually true, the resolution principle enables the empty clause 0 to be derived, thus establishing a contradiction. The refutation method can provide conclusions which could not be derived by direct application of the resolution principle. This procedure is valid when the initial set of clauses is consistent. The refutation method can be extended to the case of uncertain propositions. To do so, the negation of the proposition to prove is added to the set of ground clauses, with a necess~y degree equal to 1. We have the following Ilw2am : The grade of necessity obtained for the empty clause, using the refutation method, corresponds to a lower bound of the grade of necess~y of the proposition to prove.

f!r2g1: Let C be the set of clauses Ci (with their weighting) and q be the proposition to evaluate. Let us suppose we have obtained N(O) ~a. Obviously 0 with the weight a has been produced by application(s) of the resolution principle (using (7) and (9)) to the set of clauses Ca U {~qJ (with Nhq) · 1 ), where Ca . {Ci I N(Ci) ~a}. Observe that 0 would be obtained as well by application of the standard resolution principle to CaU {~q}, forgetting the weights. Hence q is a logical consequence of Ca. which means that ~(Ai {Ci e Ca)) v q · 1 i.e. NHAi {Ci e CcJ) v q) - 1. Now N(Ai {Ci e CaJ) - mini {N(Ci) 1 Ci e Ca)2: a. Applying (7) in the restricted form

of the modus ponens, we conclude that N(q) 2: a. Q.E.D.

l':i...6...3. : Let C · be a set of uncertain clauses, and C the set of clauses obtained by deleting the uncertainty coefficients in c·. Then c · is said to be inconsistent if and only if the uncertainty coefficients in c· violate the axioms of the adopted theory of uncertainty, here (3). Then the following theorem can be proved ; see (5).

~: If all uncertain clauses inc· are such that N(Ci) ~ ai > 0, then c· is consistent if and only if C is consistent in the usual sense. This equivalence is no longer true with probability measures.

3 - Linear strategy wjth an ordered search method

We are interested not only in obtaining the empty clause as in the classical refutation method, but more particularly in reaching it with the greatest possible lower bound on the associated necessity. In order to have a tree-like search graph, we use a linear resolution strategy (see [2)). Such a strategy only allows resolutions between a center clause CC issued from a top center clause c 0 (chosen among the in~ial set of clauses C such that C- {Co} is consistent) and a side clause which is e~her a clause in C- {Co) or a center clause ancestor of CC. A state (i.e. a node) will be defined by a center clause and the set of ~s ancestor clauses. See Fig. 1.

c 0 will be chosen among the clause(s) produced by the negation of the proposition to evaluate. Thus we have N(Co) · 1. The cost associated with a

c ·i+1 link (C 0 c 1 ... Ci) _________,. (C 0 c 1 ... cici+ 1 ) is w(C'i+ 1 ) where w(C'i+ 1) stands for a known lower bound of N(C'i+1l· Ci+1 is obtained by application of the resolution principle between the center clause Ci and the side clause c ·i+ 1· The global cost of a path c 0 -> C1 -> .. . -> Ci+ 1 corresponding to a state Sk+1 is g(Sk+1) · min(g(Sk). w(C' i+1)) · min {w(C} j -1. i + 1} where Sk = (C 0 , ... ,Cil· Ci denotes a center clause, and c·j a side clause. A weight w(Ci+ 1) · g(Sk+ 1) is assigne<J.to the resolvent Ci+ 1· (Co··· Cnl is a goal state if Cn · 0 and w(Cnl > 0. A state (C0c 1 ... Cil is expanded by producing all the resolvents of Ci with {C0, .. . ,Ci-1l U C - {Col · The search for the empty clause w~h the greatest lower bound is equivalent to the search for a path whose cost is maximum (called by Yager [13) "path of least resistance· in the framework of a possibilistic interpretation). In the following we use an analog of the A"- algorithm, where the sum is replaced by the min operation in the defin~ion of the evaluation function f(Sk) - min(g(Sk)· h(Sk)) w~h Sk · (C 0 c 1 ... Cil· where g(Sk) · w(Cil and h(Sk) is an overestimate of the cost of any path from Ci to 0. We shall propose in the following various possible choices for h(Skl· The next state to expand is chosen among the pending states with the greatest f(Skl· Then we are certain that the algorithm stops, finds a goal state if any and that the first goal state which is obtained is optimal, as for a standard A' - algorithm. The procedure we use can be viewed as a heuristically guided linear strategy. We have the following resu~.

I.ll.ill.am : An optimal refutation (i.e. a refutation which leads to the empty clause with the greatest possible lower bound of the necessity measure) can be obtained using a linear strategy.

fmgf : Let c· be the subset of C used in a considered optimal refutation. Since c· - {Co) is consistent, there exists a linear refutation from c·. This

refutation is obviously such that w(O) 2: minee c· w(C) ; but W this inequality strictly holds, only a proper subset of c· would be useful in the refutation, which is contradictory. Hence w(O)·mincec·w(C) and consequently there exists an optimal linear refutation of C (since a linear refutation of c· is a linear refutation of C). Q.E.D.

In order to be sure that the first refutation which is obtained, if any, is optimal, the evaluation function must be admissible, I.e. here h(Sk) must be an over-estimate of the cost of any path from Ci to 0 where Sk · (CoC1 ···Cil· An obvious possible choice is 'of k, h(Sk) · 1 ("uniform cost· algorithm). For any refutation developed from a clause C, for any literal I of C, we have to use a clause c· where the literal ...J is present at a step or another in order to obtain the empty clause. Note that the arguments (which may be dHferent) of I and -.1 are not considered here. Thus a refutation developed from C has a cost less than or equal to H(l). max{w(C'), -.1 e C', c · e R(C)), 'of I, literal of C where R(C) is the set of all clauses produced from C (including the clauses in C). H(l) can be easily computed and is in fact a static function since we have

Indeed if C' e R(C), one of its ancestor already including -.1. This is true in particularforthe clause C' which maximizes H(l), W C' e R(C). w(C') can be neither greater than the weight attached to an ancestor including -.1, nor smaller since C' maximizes H(l) and c· e R(C). Hence the result. Thus an overestimate of the cost of a path to 0 developed from a clause C is

h1 (S) · min 1 e C· max{w(C'), c · e C, -.1 e Cl· min{H(I), I e C) with S · (Co ... C). An admissible evaluation function is then obtained 11 (S). min(w(C), h1(S)). Note that h1(S) depends only on C. In the following we write f1(C) and h1(C). A sequence of admissible evaluation functions can then be defined by

~ can be checked that any refutation using C has a cost less than or equal to fp(C), and then 'of p, hp is still an overestimate, that 'of p, hi>+ 1 (C) 2: hp(C), and that hp(C) becomes stationary when p increases. However the computation of hp may be time consuming for p > 1.

~ : A subsumed clause can be eliminated only if the clause which subsumes it has a greater or equal weight. lnd11ed for instance P(x) subsumes P(a), but an optimal refutation of {P(x) (0.5) ; P(a) (0.8) ; -.P(a) (1)) leads to 0 with a weight equal to 0.8 while from {P(x) (0.5); -.P(a) (1)}, we only obtain a lower bound equal to 0.5.

4-~

Let us consider the following knowledge base

C1 If Robert attends a meeting, then Mary does not ; C2 Robert comes at the meeting to-morrow ; C3 If Beatrix comes to-morrow, it is likely that the meeting will not be quiet ; C4 Perhaps Beatrix comes to-morrow ; C5 If Albert comes to morrow and Mary does not, then it is almost certain that the meeting will not be quiet ; C6 It is likely that Mary or John will come to­ morrow ; C7 If John comes to-morrow it is rather likely that Albert will come.

This can be represented by the following weighted clauses ; first names are coded by the initial and m denotes the meeting to-morrow

C1 : -.R(x) v -.M(x) (1) ; C2 : R(m) (1) ; C3 : -.B(m) v -.quiet(m) (0.8) ; C4 :

B(m) (0.3) ; C5 : M(m) v -.A(m) v -.quiet(m) (0.9) ; C6 : M(m) v J(m) (0.8) ; C7

: ....J(m) v A(m) (0.7).

Note that the weights have essentially an ordinal value since they are combined by the min operation. This makes their elicitation easier. If we want to try to prove that the meeting to-morrow will not be quiet, we add the clause CO : quiet(m) (1 ). Then it can be checked that there exist two possible refutations pictured on Figure 2.

The procedure described in section 3 (presently running on a micro­ computer) yields the optimal path which enables us to conclude that the meeting will not be quiet, with a necessity degree at least equal to 0.7. In our example it may seem interesting to produce the two refutations since it leads to two distinct justifications ; we might even think of some reinforcement of the certainty degree of the conclusion, but this is out of the scope of a purely logical approach.

Note that an uncertain clause (i.e. with a weight strictly less than 1 ), involving variable's such as -.P(x) -+ Q(x) (a) should be understood as N('ot x P(x) v O(x)) 2! a. i.e. as an uncertain conjecture which either holds for all .x or to~ wh~ch there exists an unknown proportion of counter-examples. Thts Is quite dtfferent from a default rule whose exceptions are by definition not often encountered. However, once instantiated the clause considered above gives -.P(a) -+ O(a) (a), where a can then be viewed as a lower bound of the a priori degree of certainty that the value of x, here a, does not correspond to an exceptional case.

5 - Concludjng remarks

A knowledge base provided by a human may be inconsistent. We can define the degree of inconsistency of a set of clauses C as the greatest weight with which the empty clause can be obtained by resolution from C. Let a be this degree. Note that the subset of clauses in C with a weight strictly greater than a Is consistent. Then if by optimal refutation we obtain from C U {-.C (1)}, where Cis a clause to prove, the empty clause with a weight ~ > a, then we can conclude that N(C) 2: ~ ; in his case the proof of C uses only a consistent part of C. When p · a (obviously ~ <a is impossible), the consistent part of C defined by the clauses with a weight strictly greater than a is not sufficient for proving C and then we have to try to find another consistent subpart of C from which it is possible to establish C. This is a topic for further research.

Another topic of research is the completeness of the extended resolution principle. For this purpose we need to interpret a piece of knowledge such as N(p) 2: a> 0. An interpretation is then a fuzzy set where any model of p has a degree of membership equal to 1 and any model of -.p has a degree of membership at most equal to 1 - a. .

A further topic of research will be to accomodate vague predicates in our framework. An idea for doing this might be to approximate a vague statement by a collection of weighted, non-vague statements (since a fuzzy set can be approximated by a finite collection of nested ordinary subsets).