Resolution Principle

Fuzzy Multi-dimensional Analysis	Alexandr A. Savinov
[Home] [Contents] [Previous] [Next] [E-mail]	[0] [1] [2] [3] [4] [5] [6] [7] [8]

5. Resolution Principle

5.1. General Definition

Logical inference usually consists in that new disjunctions are built from the source disjunctions. Then they are added to the CNF and can serve as premises for continuing the inference process. Here we will not touch the question what logical inference is needed for and which requirements it have to meet. We will only consider how disjunctions can be generated.

The main operation for generating disjunctions can serve a fuzzy resolution. It is applied to two disjunctions on some section (variable) and results in a third disjunction called a resolvent. If u and v are two disjunctions and w is their resolvent on k-th variable, then we write:

u<x_k>v = w

where <x_k> denotes the resolution on k-th variable.

Now let us consider how given two premises the resolvent is built. Each section of the resolvent depends on (is constructed from) only two corresponding sections of the premises. k-th proposition of the resolvent (which the resolution is applied to) is equal to the conjunction of the two corresponding propositions from the source disjunctions; every non-k-th proposition of the resolvent is equal to the disjunction of the two corresponding propositions:

w_i = u_i AND v_i, w_ij = min(u_ij, v_ij), if i = k, j = 1,2,...,n _i
w_i = u_i OR v_i, w_ij = max(u_ij, v_ij), otherwise

Conjunction and disjunction of elementary propositions about the same variable are equal to the componentwise minimum and maximum, respectively.

The resolution operation can be represented in the form of the following pattern (Fig. 6):

	x₁ max		x_k min		x_n max
u	u₁	-/-/-	u_k	-/-/-	u_n
v	v₁	-/-/-	v_k	-/-/-	v_n
w = u<x_k>v	u₁ OR v₁	-/-/-	u_k AND v_k	-/-/-	u_n OR v_n

Fig. 6. Operation of fuzzy resolution.

Here are two examples of applying the resolution:

u	{0, 0.1, 0.2, 1}	{0, 1}
v	{1, 0.3, 0.5, 0}	{0, 0}
w = u<x₁>v	{0, 0.1, 0.2, 0}	{0, 1}

u	{0, 1}	{0, 1, 0.7}	{1, 0.2, 1}
v	{1, 0}	{1, 1, 0.2}	{0, 0.1, 0}
w = u<x₂>v	{1, 1}	{0, 1, 0.2}	{1, 0.2, 1}

The main property of the resolvent is that it is a consequence of two its premises: If w = u <x_k> v, then u AND v |= w.

It means that we can add any resolvent to the CNF containing its two premises and the the whole semantics will not change.

If there is only one variable, then we obtain extensional case and the resolution is reduced to ordinary conjunction. Thus the resolution operation in some sense can be viewed as a generalization of conjunction onto multidimensional case.

In the case of two-valued variables and two-valued distributions the behavior of this resolution coincides with that for the classical case of boolean propositions except for the fact that our resolution can be applied to any two disjunctions even if their k-th propositions are not contrary and/or there exist non-k-th contrary propositions. It is obvious that in the first case the resolvent will be a consequence of one of its premises, while in the second case it will be valid, i.e., involve the constant proposition 1.

Let us consider the following example.

u	{0, 1}=x₁	{0, 1}=x₂	{0, 0}=0
v	{0, 0}=0	{1, 0}=~x₂	{0, 1}=x₃
w = u<x₂>v	{0, 1}=x₁	{0, 0}=0	{0, 1}=x₃

In this classical example of the boolean resolution we obtain "good" resolvent since sections u₂ and v₂ are contrary, while other sections are not. Each section is written in sectioned form and conventional form with the help of boolean propositions.

In the following example we obtain the resolvent which is a consequence of (weaker than) both premises since the sections u₂ and v₂ are not contrary. Note that classical resolution is not applied to such disjunctions.

u	{0, 1}=x₁	{0, 1}=x₂	{0, 0}=0
v	{0, 0}=0	{0, 1}=~x₂	{0, 1}=x₃
w = u<x₂>v	{0, 1}=x₁	{0, 1}=0	{0, 1}=x₃

In this example we also obtain "bad" resolvent since two premises involve contrary non-k-th propositions which result in the constant proposition 1 in the resolvent.

u	{0, 1}=x₁	{0, 1}=x₂	{0, 0}=0
v	{1, 0}=0	{1, 0}=~x₂	{0, 1}=x₃
w = u<x₂>v	{1, 1}=1	{0, 0}=0	{0, 1}=x₃

5.2. Resolution on Reduced Disjunctions

If to consider the resolution as being a generalization of conjunction (multidimensional conjunction), then it is natural to suppose that its goal is to infer the disjunction which is equivalent to the conjunction of two source disjunctions. In that case the resolvent would represent just both source premises in one clause, and consequently the source disjunctions could be removed as superfluous. However, such ideal variant is unrealizable because the conjunction of two disjunctions in general case cannot be represented in the form of only one disjunction. Nevertheless, it is possible to formulate the criterion of "quality" of one resolution operation or another: the closer the semantics of two disjunctions is approximated by their resolvent, the better the resolution rule.

It is a characteristic property of the general definition of the resolution formulated in the previous section that the resolvent content (semantics, i.e., the corresponding fuzzy distribution) depends on the premises form. In the following two examples the premises have different forms but the semantics is the same, while the resolvents have different semantics:

u	{1, 0.3}	{0, 0}
v	{0, 1}	{1, 0}
w = u<x₁>v	{0, 0.3}	{1, 0}

u	{1, 0}	{0.3, 0.3}
v	{0, 1}	{1, 0}
w = u<x₁>v	{0, 0}	{1, 0.3}

Thus the question arises: which form of premises is the best from the point of view of the above formulated criterion, or which form of premises generates the strongest resolvent.

The resolvent components are decreased only in k-th section when conjuncting two source sections (in the rest of sections the components can be only increased), i.e., it is exactly k-th section that is responsible for non-trivial semantical properties of the resolvent. The higher component values in disjunctive (non-k-th) sections, the weaker the resolvent. In ideal case when all non-k-th sections consist of only zero components the resolvent is exactly equal to the conjunction of two premises, for example:

u	{0, 0, 0}	{1, 0.5, 0.3}	{0, 0}
v	{0, 0, 0}	{0, 0.5, 1}	{0, 0}
w = u<x₂>v	{0, 0, 0}	{0, 0.5, 0.3}	{0, 0}

Here the constant of the first disjunction is equal to 0.3, and the constant of the second disjunction is equal to 0. If in this example the constant of the first disjunction is transferred from the second sections (u₂=u₂-0.3) into any other disjunctive section (e.g., the third one, i.e., u₃=u₃+0.3), then the resolvent becomes worse, i.e., weaker than that in the ideal case:

u	{0, 0, 0}	{1, 0.5, 0}	{0.3, 0.3}
v	{0, 0, 0}	{0, 0.5, 1}	{0, 0}
w = u<x₂>v	{0, 0, 0}	{0, 0.5, 0}	{0.3, 0.3}

It becomes more clear if the resolvent obtained is transformed into the following equivalent form (2nd reduced form):

w = u<x₂>v

{0, 0, 0}

{0.3, 0.5, 0.3}

{0, 0}

Thus our conclusion is that in order to infer the strongest resolvent on k-th section, the premises have to be transformed into the k-th reduced form. However all below described properties of the resolution will be formulated for the general definition independent of the premises form.

5.3. Adjacency of Disjunctions

Although the goal of the application of resolution is to obtain a new non-trivial disjunction differing from both the first premise and the second premise, this requirement can be satisfied not always (it is not satisfied for the majority of disjunction pairs and variables). More exactly two disjunctions u and v are said to be adjacent on the variable x_k if their resolvent on k-th variable is not a logical consequence of the disjunction u and disjunction v, i.e., it cannot be absorbed by its premises.

Now it is clear that it makes sense to apply the resolution to only adjacent disjunctions, otherwise the resolvent is a consequence of one of two premises and it does not contain new information. For example, the following two disjunctions are adjacent on the first variable and they are not adjacent on the second variable:

u	{1, 0.5, 0.2}	{1, 0}
v	{0, 0.2, 1}	{0, 0}
w = u<x₁>v	{0, 0.2, 0.2}	{1, 0}

u	{1, 0.5, 0}	{1, 0.2}
v	{0, 0.2, 1}	{0, 0}
w = u<x₂>v	{1, 0.5, 1}	{0, 0}

In this context the problem can be formulated as follows:

how to find out whether two disjunctions are adjacent or they are not, making use only their form, without constructing the resolvent

This problem can be solved with the help of the following criterion.

Disjunctions u and v are adjacent on the variable x_k iff forall i=1,...,n except for i=k

constant(u_i OR v_i) < incomp(u_k,v_k)

In other words the minimal value of the disjunction of two sections u_i and v_i has to be strictly less than the degree of incomparability of the sections u_k and v_k. Informally two disjunctions are adjacent if and only if the mutual degree of incomparability of two sections u_k and v_k (which the resolution is applied to) is high enough to compensate the validity resulted from the disjunction of non-k-th sections.

Thus the adjacency of two disjunctions is influenced by the following two factors:

too low degree of incomparability of the propositions about k-th variable;
too high constant (degree of validity) in non-k-th sections.

The first factor is a generalization of the conventional condition (see, e.g., [CL73]) that the resolution is applied only to disjunctions involving contrary literals. It is natural that in fuzzy case the contrariety of two literals is also fuzzy (the degree of incomparability). Note that the contrariety and incomparability coincide only in two-valued non-fuzzy case (classical propositional calculus); in any other case the incomparability condition is weaker.

The second factor influencing the adjacency of two disjunctions is a generalization of the conventional condition which consists in the absence in disjunctions of the second pair of contrary literals.

When computing the value constant(u_i OR v_i) we have to construct i-th section of the resolvent w_i=u_iORv_i, i.e., in fact, to find out if two disjunctions are adjacent or not with the help of this criterion it is necessary to construct n-1 sections of the resolvent. Thus it could be more easy to construct the resolvent and then to check if it is a consequence of one of its premises. However it is not so, since for the majority of disjunction pairs the condition incomp(u_k,v_k)=0 holds, and therefore the criterion constant(u_i OR v_i)<incomp(u_k,v_k) cannot be satisfied in any case. In addition, even if incomp(u_k,v_k)>0 it makes sense to check the criterion for each new section of the resolvent rather than check the adjacency after building all the sections. Thus the whole procedure for generating resolvents is as follows:

build the k-the section of the resolvent: w_k=u_kANDv_k;
find the value incomp(u_k,v_k);
if incomp(u_k,v_k)=0 then goto 9;
for i=1,2,...,n (except for i=k);
build the i-th section of the resolvent: w_i=u_iORv_i;
if constant(w_i)>=incomp(u_k,v_k) then goto 9;
next i (goto 5);
the disjunctions u and v are adjacent and the resolvent w is built;
the disjunctions u and v are not adjacent;

Fuzzy Multi-dimensional Analysis	Alexandr A. Savinov
[Home] [Contents] [Previous] [Next] [E-mail]	[0] [1] [2] [3] [4] [5] [6] [7] [8]