Keywords

1 Introduction

Man had for long wanted to find a general decision procedure to prove theorems. Since 1930, consistent efforts were made by Herbrand and others in this respect. It was in 1965 that Robinson [1] made a major breakthrough. He introduced a machine-oriented logic based on resolution principle to check the (un)satisfiability of a set of formulae represented in some standard form.

Mechanical theorem proving techniques were first applied to deductive question answering systems and then to problem solving, program synthesis, program analysis and many others. In automated theorem proving, resolution acts as a rule of inference leading to a refutation based theorem-proving technique.

Now, given some formulae modelling vague knowledge, can we define an automated procedure which decides whether a given conclusion is logically entailed by the knowledge? A first step towards formalization of automated deduction in fuzzy logic was taken by Lee and Chang [2]. Lee’s works [2, 3] were continued and implemented by other researchers. Lee’s fuzzy formulae are syntactically defined as classical first-order formulae, but they differ semantically as the formulae have a truth value in [0,1]. Mukaidono [4, 5] generalized Lee’s [3] result. Dubois and Prade [6] established fuzzy resolution principle in the case of uncertain propositions. In Kim et al. [7], antonym-based fuzzy hyper-resolution was introduced and its completeness was proved. Fontana and Formato [8] introduced, a fuzzy resolution rule based on an extended most general unifier provided by the extended unification algorithm. Sessa [9] proposed a methodology to manage uncertain and imprecise information in the frame of the declarative paradigm of logic programming considering, a similarity relation between function and predicate symbols in the language of a logic program. Habiballa and Novak [10] presented refutational theorem proving system for fuzzy description logic based on the general resolution rule. Raha and Ray [11] investigated a generalized resolution principle that handles the inexact situation effectively and is applicable for both well-defined and undefined propositions. They associated a truth value to every proposition and used Zadeh’s concept of approximate reasoning based on possibility theory to model a deductive process. In this research, we extend our knowledge to present, a generalised resolution principle that deals with fuzzy propositions and uses the technique of similarity based reasoning. Similarity is inherent in approximate reasoning, but none used it in fuzzy resolution. Indeed, human reasoning is often performed on the basis of analogy and/or similarity between entities. We, therefore, accomplish the task of choosing an almost complementary pair in fuzzy resolution on the basis of similarity/dissimilarity measure of fuzzy sets instead of contradictory degree of the pair. The advantage of our method is that, it reduces significant and important drawback of compositional rule of inference and executes effective resolution to show its flexibility for automated reasoning. In this article, we have avoided the generic problem in generalised modus ponens (GMP) by using similarity-based inverse approximate reasoning method [12] in fuzzy resolution. However, for complex set of clauses the method is not suitable. In this case, we investigate similarity-based ordinary approximate reasoning [13] to deduce fuzzy resolution.

2 Preliminaries

We start by summarizing a few basic concepts of fuzzy logic connected with fuzzy resolution.

Definition 1

A resolvent of two clauses C 1 , C 2 containing the complementary literals p and \( { \neg p} \) respectively, is defined as

$$ res(C_{1} ,C_{2} ) = \{ C_{1} - \{ p\} \} \mathop \cup \nolimits \{ C2 - \{ \neg p\} \} , $$

∪ is understood as the disjunction of the literals present in them.

It is also a logical consequence of C 1 and C 2.

Definition 2

A resolution deduction of a clause C from a set S of clauses is a finite sequence of clauses C1, C2,..., C n  = C such that, each C i is either a member of S or is a resolvent of two clauses taken from S. From the resolution principle in propositional logic we deduce that, if S is true under some truth valuation v, then v(C i ) = TRUE for all i, and in particular, v(C) = TRUE [14].

A simple resolution scheme is:

$$ \frac{\begin{gathered} premise 1:{\text{a}} \vee {\text{b}} \hfill \\ premise 2:\quad \neg {\text{b}} \hfill \\ \end{gathered} }{conclusion:a} $$

In first order logic, resolution condenses the traditional syllogism of logical inference down to single rule. To recast the logical inference using the resolution technique, the formulae are represented in conjunctive normal form.

Definition 3

C 1 and C 2 being two clauses in fuzzy logic, R(C 1 , C 2) being a classical resolvent of C 1 and C 2, and A being the literal C 1 and C 2 are resolved upon (i.e., C 1A and C 2 ∈ ~ A or conversely), then fuzzy resolvent R(C 1 , C 2) cd ( A ) of C 1 and C 2, where cd(A) is the contradictory degree of keyword A or the confidence associated with the resolvent, is defined by

$$ R(C_{ 1} ,C_{ 2} )_{cd (A )} \triangleq R(C_{ 1} ,C_{ 2} ){\text{ V}}(A \wedge \, \sim A) $$

An important theorem which was proved in [4, 5] is given in the following [15]:

Theorem 1

A set S of fuzzy clauses is unsatisfiable if and only if, there is a deduction of empty clause with its confidence of resolvent cd ≠ 0 from S.

Fuzzy Implication:

Typically, a fuzzy rule ‘If X is A then Y is B’ (A and B are fuzzy sets) is expressed as I(a, b), where I is a fuzzy implication and a and b are membership grades of A and B respectively. From an algebraic point of view, some implication operators basically identified in [16] are classified with four families \( I_{i}^{T} ,\;i \in \{ 1,2,3,4\} \), where T and T* denote the specific t-norm and correlated t-conorm respectively (see, Table 1) to implement the implication operators. Here, we use only two families I 2 and I 3 of implication operators. Family I2, often named S-implication, derives from classical logic form \( a \to b = \neg a \vee b \). Family I3, known as R-implication, reflects a partial ordering on propositions. With reference to the t-norms and t-conorms in Table 1, the explicit expressions of fuzzy implication operators \( I_{i}^{T} \) are presented in Table 2.

Table 1 T-Norms and T-Conorms
Table 2 Expression of fuzzy implication operators

Similarity Index:

The notion of similarity plays a fundamental role in theories of knowledge and behaviour and has been dealt with extensively in psychology and philosophy. If we study the behaviour pattern of children we find that, children have a natural sense in recognizing regularities in the world and to mimic the behavior of competent members of their community. Children thus make decisions on similarity matching. The similarity between two objects suggests, the degree to which properties of one may be inferred from those of the other. The measure of similarity provided, depends mostly on the perceptions of different observers. Emphasis should also be given to different members of the sets, so that no one member can influence the ultimate result. Many measures of similarity have been proposed in the existing literature [17, 18]. A careful analysis of the different similarity measures reveals, that it is impossible to single out one particular similarity measure that works well for all purposes.

Suppose U be an arbitrary finite set, and \( {\mathcal{F}}\,(U) \) be the collection of all fuzzy subsets of U. For \( A,B\; \in \;{\mathcal{F}}\,(U) \), a similarity index between the pair {A, B} is denoted as S(A, B; U) or simply S(A, B) which can also be considered as a function \( S:\;{\mathcal{F}}\,(U) \times {\mathcal{F}}\,(U) \to [0,1] \). In order to provide a definition for similarity index, a number of factors must be considered. We expect a similarity measure S(A, B) to satisfy the following axioms :

  • P1. S(B, A) = S(A, B), S(not A, not B) = S(A, B), not A being some negation of A.

  • P2. 0 ≤ S(A, B) ≤ 1.

  • P3. S(A, B) = 1 if and only if A = B.

  • P4. For two fuzzy sets A and B, simultaneously not null, if S(A, B) = 0 then \( \hbox{min} \left( {\mu_{A} (u),\mu_{B} (u)} \right) = 0 \) for all u ∈ U, i.e., \( A \cap B = \varPhi \).

  • P5. If either \( A \subseteq B \subseteq C \) or \( A \supseteq B \supseteq C \) then S(A, C) ≤ min{S(A, B), S(B, C)}.

We now consider a definition of measure of similarity which has been proposed in [13, 19].

Definition 4

Similarity Indices Let A and B be two fuzzy sets defined over the same universe of discourse U. The similarity index S(A, B) of pair {A, B} is defined by

$$ S(A,B) = 1 - \left( {\frac{{\sum\limits_{u} {\left| {\mu_{A} (u) - \mu_{B} (u)} \right|^{q} } }}{n}} \right)^{\frac{1}{q}} , $$

where n is the cardinality of the universe of discourse and q ≥ 1 is the family parameter.

Measure of dissimilarity is another measure of comparison of objects in literature. Many authors like Meunier et al. [17] have defined measure of dissimilarity in different way. However, we use the dissimilarity measure in the context of similarity measure and consider measure of dissimilarity of two fuzzy subsets A and B defined over \( {\mathcal{F}}\,(U) \), denoted by D(A,B) as D(A, B) = 1 − S(A, B). Moreover, we assume D(A, B) = S(not A, B) = S(A, notB). Through out the chapter, we use this concept of dissimilarity.

In the next section, principle of fuzzy resolution is discussed based on the method of inverse approximate reasoning [12].

3 Fuzzy Resolution Based on Inverse Approximate Reasoning

Instead of complementary literal in the set of clauses in fuzzy logic, we introduce here a concept of similar/dissimilar literal. Let us consider two clauses \({C_{1}}= P\vee {C_{1}}^{\prime}\) and \({C_{2}}= {P^{\prime}} \vee {{C_{2}}^{\prime}}\). Resolvent of C 1 and C 2 denoted by \({\rm{res}}({C_{1}}, {C_{2}})= {{C_{1}}^{\prime}} \vee {{C_{2}}^{\prime}}\) if and only if similarity between P and P′ is less than Q or equivalently, dissimilarity between P and P′ is greater than 1 − Q, Q being pre-defined threshold.

The argument form of simple fuzzy resolution is as follows.

$$ \frac{{\begin{array}{*{20}l} A \hfill & \vee \hfill & B \hfill \\ {} \hfill & {} \hfill & {not\;B} \hfill \\ \end{array} }}{{\begin{array}{*{20}r} \hfill {} & \hfill A & \hfill {} \\ \end{array} }} $$

The scheme for Generalised Fuzzy Resolution is given in Table 3.

Table 3 Generalised fuzzy resolution

In this case, we can say that the Disjunctive Syllogism holds if B′ is close to notB, A′ is close to A.

The scheme in inverse approximate reasoning is as given in the following Table 4. Here, fuzzy sets A and A* are defined over the universe of discourse \( U \, = \{ u_{1} , \, u_{2} , \ldots \, ,u_{m} \} \) and fuzzy sets B and B* are defined over the universe of discourse \( V = \{ v_{1} ,v_{ 2} , \ldots ,v_{n} \} . \)

Table 4 Inverse approximate reasoning

We, now, transform the disjunction form of rule into fuzzy implication or fuzzy relation and apply the method of inverse approximate reasoning to generate the required resolvent.

We proposed two algorithms SIAR and INAR for inverse approximate reasoning based on similarity given in [12]. We apply these methods to obtain a resolvent in fuzzy resolution.

In classical logic, we have

$$ a \to b \equiv \neg a \vee b,\;\forall a,b \in \{ 0,1\} . $$
(1)

Let us extend this classical logic equivalence to fuzzy logic, by interpreting the disjunction and negation as a fuzzy union (t-conorm) and a fuzzy complement, respectively. Fuzzy implication thus obtained is usually referred to in the literature as S-implication.

We now consider the classical logic tautology which is obtained from (1).

$$ a \vee b \equiv \neg a \to b,\;\forall a,b \in \{ 0,1\} . $$
(2)

Extending the classical equivalence (2) into fuzzy logic, we find that the fuzzy union is transformed to fuzzy implication. In fuzzy resolution, we deal with rule of type ‘X is A or Y is B’. Like classical logic, we may transform the rule into ‘If X is notA then Y is B’ under fuzzy logic. Hence, the equivalent scheme of Table 3 that conforms fuzzy resolution is considered in Table 5. It is noted that A* is similar to A, whenever B* is similar to notB.

Table 5 Equivalent scheme conforms fuzzy resolution

We have demonstrated in [12] that, if the given data is sufficiently dissimilar to the consequent part of a given rule then we conclude that the resulting fuzzy set is sufficiently dissimilar to the antecedent part of the rule. Applying this method, in the scheme given in Table 5, we get the required resolvent, which establishes the fuzzy resolution principle. The algorithm is as follows:

ALGORITHM—FRIAR:

  1. Step 1.

    Translate the rule into fuzzy implication as \( \mu_{R} \left( {u,v} \right) = I \left( {\mu_{notA} \left( u \right), \, \mu_{B} \left( v \right)} \right) \), where I is an implication operator;

  2. Step 2.

    Take cylindrical extension of B* in V on U × V, say R′, defined by \( R^{\prime } = \sum\nolimits_{U \times V} {\mu_{B} \left( v \right)/\left( {u,v} \right)} \);

  3. Step 3.

    Compute R* = RR′, where ∩ denotes any fuzzy conjunction operator;

  4. Step 4.

    Obtain A* = projR* on U defined by

    $$ projR^{*} {\text{on U}} = \sum\nolimits_{u} {\mathop {\text{Sup}}\limits_{v} \mu_{R} (u,v)/u} . $$

Mathematically, we get

$$ \begin{aligned} \mu_{A*} (u) = & proj_{v \in V} R^{*} (u,v) \\ = & \sup_{v \in V} T\left( {\mu_{R} (u,v),\mu_{{R{\prime }}} (u,v)} \right) \\ = & \sup_{v \in V} T\left( {\mu_{R} (u,v),\mu_{B*} (v)} \right) \\ \end{aligned} $$
(3)

where T is a t-norm used to describe fuzzy conjunction operator.

It is expected that, for the observation ‘Y is notB’ and the given premise ‘X is A or Y is B’ we can conclude ‘X is A’ by fuzzy resolution. However, for the the observation ‘Y is B’ no conclusion can be drawn. We establish the above criteria by the following theorem.

Theorem 2

Let B * = not B be normal and R be interpreted by any S-implication satisfying (3). Then A* ⊇ A for any t-norm T. (consistency)

Corollary

Let B * = not B be normal and R be interpreted by any S-implication satisfying (3). Then A* = A for Lukasiewicz t-norm T.

Example 1

Consider the premises

$$ \begin{array}{*{20}l} {p:} \hfill & {X\,\text{is}\,LARGE} \hfill & {\text{or}} \hfill & {Y\,{\text{is}}\,SMALL} \hfill \\ {q:} \hfill & {} \hfill & {} \hfill & {Y\,{\text{is}}\,{\text{not}}\,SMALL} \hfill \\ \end{array} $$

in which X and Y are defined over the universes U = {u 1 ,…, u 4 } and V = {v 1 ,…, v 4 } respectively and fuzzy sets labelled by LARGE, SMALL and not SMALL are defined by

$$ A \triangleq {\text{LARGE}} = \, 0/u_{1} + 0. 4 5/u_{ 2} + \, 0. 9 5/u_{ 3} + { 1}/u_{ 4} $$
(4)
$$ B \triangleq {\text{ SMALL}} = 1/v_{ 1} + 0. 6 5/v_{ 2} + 0. 1 5/v_{ 3} + 0.0/v_{4} $$
(5)
$$ {\text{B}}^{*} \triangleq not\,{\text{SMALL}} = \, 0/v_{1} + 0. 3 5/v_{ 2} + 0. 8 5/v_{ 3} + 1/v_{ 4} $$
(6)

The similarity between fuzzy sets B and B* is 0.0, i.e., fuzzy set B * in observation is dissimilar to fuzzy set B in the disjunctive form of rule.

Again, by INAR, we study the shape of the resolvent A* for data given in (4), (5) and (6) with different S-implications and different t-norms, which is described in the Tables 6, 7 and 8, where M, p and B indicate minimum, product and bounded product respectively for t-norms.

Table 6 A* for Reichenbach S-implication
Table 7 A* for Kleene-Dienes S-implication
Table 8 A* for Lukasiewicz S-implication

The result shows that the dissimilarity between B * and B assures the similarity between A * and A when the reasoning mechanism is handled using inverse approximate reasoning. Thus the proposition ‘given a disjunction and the negation of one of the disjuncts, the other may be inferred’ is established in fuzzy logic.

Example 2

Now, we consider the scheme and data of Example 1 except B*. Consider B* = 0.0/v 1 + 0.1225/v 2 + 0.7225/v 3 + 1.0/v 4 in (6). We shall observe the results for the given premise ‘p’ and data in (4) and (5).

In this case, S(B,B*) = 0.1304, i.e., fuzzy sets B and B* are dissimilar.

Let us execute the reasoning mechanism by INAR. The results are shown in Table 9, 10 and 11 respectively for different implications and t-norms.

Table 9 A* for Reichenbach S-implication
Table 10 A* for Kleene-Dienes S-implication
Table 11 A* for Lukasiewicz S-implication

That is, if B * is not exactly match with notB but these are dissimilar, the fuzzy resolvent can be obtained through inverse approximate reasoning method. The technique is new.

Theorem 3

Let B * = B be normal and R be interpreted by any implication satisfying (3). Then A* = UNKNOWN for any t-norm T.

We prove the theorem for Reichenbach S-implication and T = min only, but the above theorem can be proved for any other implications and any other t-norms in the similar way.

Example 3

In Example 1, if we take B* = BSMALL = 1.0/v 1 + 0.65/v 2 + 0.15/v 3 + 0.0/v 4 in (6) then either by SIAR or by INAR we get A* = 1.0/u 1 + 1.0/u 2 + 1.0/u 3 + 1.0/u 4 = UNKNOWN, for all of the cases.

Theorem 4

Let B * = not B be normal and R be interpreted by Rescher-Gaines R-implication satisfying (3). Then A* ⊆ A for any t-norm T.

Example 4

For the data given in Example 1, applying INAR for Rescher-Gaines R-implication combined with any t-norm T, we get the fuzzy resolvent A* as

A* = 0.0/u 1 + 0.35/u 2  + 0.85/u 3 + 1.0/u 4 which is a subset of A and S(A, A*) ≈ 0.929. It establishes Theorem 4.

We, now, apply another method SIAR [12] to obtain fuzzy resolvent for the scheme given in Table 3. Let us consider another classical logic equivalence

$$ a \vee b \equiv b \vee a \equiv \neg b \to a $$
(7)

The classical logic equivalence (7) can be extended in fuzzy logic with implication and negation function. Then we transform the rule in Table 3 into its equivalent form ‘p 1 : If Y is notB then X is A’ over the domain of [0,1 ] V × U. A fuzzy rule may be defined by means of a conjunction for defining a fuzzy Cartesian product rather than in terms of a multivalued logic implication [12, 20].

Therefore, the rule in p 1 is transformed into fuzzy relation R as

$$ \mu_{R} (v,u) = T(1 - \mu_{B} (v),\mu_{A} (u)), $$
(8)

where T is a t-norm describing a fuzzy conjunction.

Now, we can apply our method SIAR described in [12]. The algorithm is as follows :

ALGORITHM—FRSIAR:

  1. Step 1.

    Translate given premise p1 and compute R(not B, A) by (8);

  2. Step 2.

    Compute similarity measure S(not B, B*) using some suitable definition;

  3. Step 3.

    Modify R(not B, A) with S(not B, B*) to obtain the modified conditional relation R(not B, A|B*) using scheme in [12];

  4. Step 4.

    Use sup-projection operation on R(not B, A|B*) to obtain A* as

    $$ \mu_{A*} (u) = \, \mathop { \sup }\limits_{v} \mu_{{{\text{R(}}not \, B,A|B* )}} (v,u). $$
    (9)

    We now illustrate the method applied here by some suitable examples.

Example 5

Let us consider the data of Example 1. For completely dissimilar B* with B and for different t-norms T, the shapes of fuzzy resolvent A* in U are studied here, when we apply SIAR. In each case, it turns out exactly the fuzzy set A which corresponds ‘LARGE’.

Example 6

Let us consider the data in Example 1 where B* is not completely dissimilar with B, but dissimilarity exceeds certain threshold. Applying SIAR we observe the shapes of A* and compare it with given A for different t-norms. Since S(A, A*) ≈ 0.92, i.e., A* is almost similar to A, it establishes fuzzy resolution in reasoning.

In the above methods, we applied INAR or SIAR when the disjunctive knowledge can be transformed into fuzzy implication. However, it may not always be the case. Moreover, when the expert knowledge is in complex form of disjunction it is difficult to apply INAR or SIAR. So, we extend our method in such a way that can deal with complex premises.

4 Fuzzy Resolution with Complex Clauses

In this section, we extend the scheme given in Table 3. Let X, Y and Z be three linguistic variables that take values from the domain U, V and W respectively. We consider the derivation of an inexact conclusion ‘r’ from two typical knowledge (premises) ‘p’ and ‘q’ according to the scheme given in Table 12, where A’s, B’s and C’s are approximations of possibly inexact concepts by fuzzy sets over U, V and W respectively. In 1993, Raha and Ray [11] applied Zadeh’s [21] concept of approximate reasoning with the application of possibility theory to model a deductive process ‘Generalised Disjunctive Syllogism’. They used projection principle and conjunction principle to deduce fuzzy resolvent. Here, we investigate another method which is described in the following algorithm.

Table 12 Generalised fuzzy resolution-extended form

ALGORITHM—FRCEP:

  1. Step 1.

    Translate the premise p into fuzzy relation

    $$ R_{1} \subseteq \, {\mathcal{F}}(U \times V)\;{\text{as}}\;\mu_{{R_{1} }} \left( {u,v} \right){\text{ = min}}(\mu_{A} (u),{ 1} - \mu_{B} (v)); $$
  2. Step 2.

    Translate the premise q into fuzzy relation

    $$ R_{2} \subseteq \, {\mathcal{F}}(V \times W)\;{\text{as}}\;\mu_{{R_{2} }} \left( {v,w} \right){\text{ = min}}(\mu_{{B{\prime }}} (v),\mu_{C} (w)); $$
  3. Step 3.

    Take cylindrical extension of R 1 in U × V on U × W, say R 1′, defined by

    $$ R_{1}^{{\prime }} = \sum\limits_{U \times V \times W} {\mu_{{R_{1} }} {{(u,v)} \mathord{\left/ {\vphantom {{(u,v)} {(u,v,w)}}} \right. \kern-0pt} {(u,v,w)}};} $$
  4. Step 4.

    Take cylindrical extension of R 2 in V × W on U × V × W, say R 2′, defined by

    $$ R_{2}^{{\prime }} = \sum\limits_{U \times V \times W} {\mu_{{R_{2} }} {{(v,w)} \mathord{\left/ {\vphantom {{(v,w)} {(u,v,w)}}} \right. \kern-0pt} {(u,v,w)}};} $$
  5. Step 5.

    Construct R′ = R 1′ ∩ R 2′, where ∩ denotes any fuzzy conjunction operator;

  6. Step 6.

    Compute S(notB, B′) and, say, s;

  7. Step 7.

    Modify R′ with s by a Scheme in [12] and, say, R*;

  8. Step 8.

    Obtain R = projR* on U × W defined by

    $$ projR^{*} \;{\text{on}}\;U \times W = \sum\limits_{U \times W} {\mathop { \sup }\limits_{v} \mu_{R*} (u,v,w)/(u,w);} \, $$
  9. Step 9.

    Obtain A’ and C’ by projecting R separately on U and W such that

    $$ \begin{aligned} A^{\prime} &= proj_{U} R \,= \sum\limits_{U} {\mathop {\sup }\limits_{w} \mu_{R} (u,w)/u\;{\text{and}}} \\ C{\prime } &= proj_{W} R \,= \sum\limits_{W} {\mathop {\sup }\limits_{u} \mu_{R} (u,w)/w)} \\ \end{aligned} $$

Symbolically, the fuzzy resolvent R is obtained by, for uU, v V and w W, μ R (u, w)

$$ \begin{aligned} = & \mathop { \sup }\limits_{v} \mu_{\text{R*}} { (}u, \, v, \, w )\\ = & \mathop { \sup }\limits_{v} \left\{ {s \to \mu_{{{\text{R}}{\prime }}} { (}u, \, v, \, w )} \right\}, \\ = & s \to \mathop { \sup }\limits_{v} \mu_{{{\text{R}}{\prime }}} { (}u, \, v, \, w )\\ = & s \to \mathop { \sup }\limits_{v} T\left( {\mu_{{{\text{R}}_{1} {\prime }}} (u, \, v, \, w ) ,\mu_{{{\text{R}}_{2} {\prime }}} (u, \, v, \, w )} \right) \\ = & s \to \mathop { \sup }\limits_{v} T\left( {\mu_{{{\text{R}}_{1} }} (u, \, v ) ,\mu_{{{\text{R}}_{2} }} (u, \, v )} \right) \\ = & s \to \mathop { \sup }\limits_{v} T\left( {\hbox{min} \left( {\mu_{A} (u),1 - \mu_{B} ( { }v)} \right),\hbox{min} \left( {\mu_{{B{\prime }}} ( {\text{v}}),\mu_{C} (w)} \right)} \right) \\ = & s \to T\left( {\hbox{min} \left( {\mu_{A} (u),1 - \mathop {\inf }\limits_{v} \mu_{B} (v)} \right),\hbox{min} \left( {\sup_{v} \mu_{{B{\prime }}} (v),\mu_{C} (w)} \right)} \right) \\ = & s \to T\left( {\mu_{A} (u),\mu_{C} (w)} \right), \quad {\text{iff}}\;1- \inf_{v} \mu_{B} (v) = \sup_{v} \mu_{{B{\prime }}} (v) = 1. \\ \end{aligned} $$

This derivation can be achieved if there is a v 0V such that μ B (v 0) = 0 and μ B(v 0) = 1 which is possible if the fuzzy sets B and B′ are dissimilar, i.e., notB and B are similar for any implication → in derivation. We observe two criteria here.

Criterion 1: Taking x → y = min(1, y/x), we get

$$ \mu_{R} (u,w) = {{\hbox{min} (1,T\left( {\mu_{A} (u),\mu_{C} (w)} \right)} \mathord{\left/ {\vphantom {{\hbox{min} (1,T\left( {\mu_{A} (u),\mu_{C} (w)} \right)} {s)}}} \right. \kern-0pt} {s)}}; $$

Criterion 2: Taking x → y = 1 − x + xy, we get

$$ \mu_{R} (u,w) = 1 - s + T\left( {\mu_{A} (u),\mu_{C} (w)} \right).s. $$

From the two criteria above, we observe that when s = S(notB, B′) = 0, i.e., when B and B′ are completely similar, R = U × W = UNKNOWN. Therefore, fuzzy resolvent could be anything. However, if s is close to unity, i.e., if B and B′ are almost dissimilar we have R is close to \( \sum\limits_{U \times W} {T(\mu_{A} (u),\mu_{C} (w))/(u,w)} \) which, after re-translation, gives ‘If X is A or Z is C’. Again, we observe that a small change in B′ produces a small change in fuzzy resolvent—which ensures our method is reasonable one.

Let us consider a scheme given in Table 13 where variables X i (i = 1, 2,,m) and the respective fuzzy subsets A i (i = 1, 2,…,m) are defined on universe U i (i = 1,2,, m) respectively; variables Y j (j = 1, 2,…,n) and the respective fuzzy subsets B j (j = 1, 2,, n) are defined on universe V j (j = 1, 2, , n) respectively. (A k , B l ) is almost dissimilar over the same universe U k (= V l ) with the degree of confidence of keyword A k is cd(A k ) = 1 − S(A k ,B l ) and the corresponding variables X k ,Y l , defined over U k (= V l ) respectively, assign same linguistic variable.

Table 13 Generalised fuzzy resolution-another extension

The algorithm is as follows:

ALGORITHM—FRAE:

  1. Step 1.

    Check for pair of literals (A i , B j ), ∀ i, j from clauses C 1 and C 2 whether these are defined over same universe and are assigned by same linguistic variable; Otherwise, resolution is not possible;

  2. Step 2.

    If dissimilarity D(A k , B l ) is high, i.e., D(A k , B l ) > 1 − Q, Q is pre-defined threshold then go to the next step and say, A k is keyword; Otherwise, there is no fuzzy resolvent;

  3. Step 3.

    Modify B j either by B j ′ = min(1, B j /D(A k , B l )) or by B j = 1 − (1 − B j ).S(A k , B l ));

  4. Step 4.

    Fuzzy resolvent is R(C 1, C 2) = A 1′ ∨ ··· ∨ A m ′ ∨ B 1′∨· · ·∨B n ′ and R(C 1, C 2) cd  = cd(A k ) which is measured as cd(A k ) = D(A k , B l );

  5. Step 5.

    Repeat the process until empty clause, with the confidence cd ≠ 0, is derived for more than two clauses.

Hence, we prove the (un)satisfiability of a theorem by the deduction of empty clause from a set of fuzzy clauses.

Let us consider an example to illustrate the method. Suppose variables that range over finite sets or can be approximated by variables ranging over such sets.

Example 7

Let us consider the premises

$$ \begin{array}{*{20}l} {p:X\;{\text{is}}\;{\text{LARGE}}\;\quad \quad or\; \, Y\;{\text{is}}\;{\text{SMALL}}\;or\;Z\;{\text{is}}\;{\text{LARGE}};} \hfill \\ {q:X\;{\text{is}}\;{\text{not}}\;{\text{LARGE}};} \hfill \\ {r:Y\;{\text{is}}\;{\text{not}}\;{\text{SMALL}};} \hfill \\ \end{array} $$

in which X, Y and Z are defined over the universes U = {u 1,, u 4}, V = {v 1,, v 4} and W = {w 1, w 2, w 3, w 4} respectively. Fuzzy sets labelled by LARGE, SMALL and not SMALL defined over the universes U, V and W respectively are given in Example 1 and fuzzy set LARGE defined over W is given by

$$ \begin{aligned} C \triangleq \, & LARGE = 0/w_{ 1} + \, 0. 20/w_{ 2} + \, 0. 7 5/w_{ 3} + { 1}/w_{ 4} . \\ {\text{A}}^{\prime} \triangleq & not\;LARGE \, = { 1}.0/u_{ 1} + 0. 5 5/u_{ 2} + \, 0.0 5/u_{ 3} + \, 0.0/u_{ 4} . \\ \end{aligned} $$

We execute the following steps with the given data, using ALGORITHM- FRCEP.

Execution:

  1. Step 1.

    Compute the fuzzy relation R 1  = A ⋁ B ⋁ C by

    $$ \mu_{{R{\prime }}} (u,v,w) = { \hbox{min} }( 1- \mu_{A} (u),{ 1} - \mu_{B} (v),\mu_{C} (w)); $$
  2. Step 2.

    Extend A′ in U cylindrically on U × V × W as

    $$ R_{2} = \sum\limits_{U \times V \times W} {\mu_{{A^{\prime }}} (u)/(u,v,w);} $$
  3. Step 3.

    Compute R′ = R 1 R 2 by \( \mu R'(u,v,w) = T(\mu R_{1} (u,v,w),\mu R_{2} (u,v,w)) \), taking fuzzy conjunction ∩ as t-norm T;

  4. Step 4.

    Modify R′ with \( S(1 - \mu_{A} (u), \mu_{A'} (u)) = s_{1} \) to get R* as \( \mu_{{R^{*} }} (u,v,w) = 1 - (1 - \mu_{R'} (u, v,w)) \cdot s_{1} \);

  5. Step 5.

    Project R* on V × W such that

    $$ R = \mathop \sum \limits_{V \times W} \mathop {\sup }\limits_{u} \mu_{R*} (u,v,w) = \left( {\begin{array}{*{20}c} {0.00} & {0.00} & {0.00} & {0.00} \\ {0.00} & {0.20} & {0.45} & {0.45} \\ {0.00} & {0.20} & {0.75} & {0.85} \\ {0.00} & {0.20} & {0.75} & {1.00} \\ \end{array} } \right) $$
  6. Step 6.

    Extend B′ in V cylindrically on V × W as \( R_{3} = \mathop \sum \limits_{V \times W} \mu_{B\prime } /(v,w) \)

  7. Step 7.

    Compute R  = RR 3 by μ R(v, w) = T(μ R (v, w), μ R3(v, w)), taking fuzzy conjunction ∩ as t-norm T;

  8. Step 8.

    Modify R with S(1 − μ b (v), μ B ′(v)) = s 2 to get R** as μ r **(v, w) = 1 − (1  μ r (v, w))·s 2 ;

  9. Step 9.

    Project R** on W such that

    $$ C^{\prime } = \mathop \sum \limits_{w} \mathop {\sup }\limits_{v} \mu_{R**} (v,w) = 0/w_{1} + 0.20/w_{2} + 0.75/w_{3} + 1/w_{4} , $$

    which is completely similar to C, i.e., S(C′, C) = 1.

Even if A′ and B′ in the respective premises p and q, are not completely dissimilar to A and B respectively, but the dissimilarity measures attain values greater than certain predefined threshold then we can get a fuzzy resolvent C′ which is almost similar to C, using FRCEP.

Suppose,

$$ \begin{aligned} A^{\prime } & = 1.0/\mu_{1} + 0.3025/\mu_{2} + 0.0025/\mu_{3} + 0.0/\mu_{4} ; \\ B^{{^{\prime } }} & = 0.0/v_{1} + 0.1225/v_{2} + 0.7225/v_{3} + 1.0/v_{4} . \\ \end{aligned} $$

S(notA, A′) = 0.873992; S(notB, B′) = 0.869604 are computed.

Then, it yields C′ = 0.24/w 1  + 0.39/w 2 +0.81/w 3  + 1.0/w 4 with S(C, C′) = 0.843441.

Therefore, it is possible to get a fuzzy resolvent from a set of fuzzy clauses if there is a pair of dissimilar literals contained in the respective clauses.

5 Example in Real Life

The statements in real life are mostly fabricated by vague, imprecise, uncertain and incomplete information which can be dealt with using fuzzy logic. In daily life, we have to often decide whether one statement follows from some other statements. Fuzzy resolution can be a way to deal with such phenomena. Let us consider the following example.

Example 8

Suppose, the stock price is low if the prime interest rate is high. Suppose, also, people are not happy when stock price is low. Assume that the prime interest rate is high. Can we conclude that people are not happy? Again, if we assume that the interest rate is very high, how can we conclude about the happiness of people?

For this problem, we construct the rule base in Table 14.

Table 14 Rule base and observations

(i) For Observation 1: The above scheme may be transformed into the equivalent scheme given in Table 15. in which prime interest rate, stock price and happiness are defined over the respective universes U = [0, 20]%, V = Rs. [10,000, 22,000] and W = [0,100]. Fuzzy sets defined over the respective universes U, V and W are given in Table 16.

Table 15 Equivalent scheme for observation 1
Table 16 Fuzzy sets in scheme

The membership grade of fuzzy complement is defined by 1 − a here, where a is the membership grade of a fuzzy set.

The similarity between complement of fuzzy set LOW in p and fuzzy set not LOW in q (denoted by s 1) is 1.0. Therefore, in two clauses, fuzzy sets are dissimilar. Hence, we can resolve upon these dissimilar pair and apply ALGORITHM—FRCEP to get the resolvent. Here,

$$ \begin{aligned} R_{1} & = \mathop \sum \limits_{U \times V} \hbox{min} (\mu_{not} \,HIGH(u),1 - \mu_{LOW} (v))/(u,v) \\ R_{2} & = \mathop \sum \limits_{V \times W} \hbox{min} (\mu_{not} \,LOW(u),\,\mu_{not} \,HAPPY\,(w))/(v,w) \\ \end{aligned} $$

We construct R′ = R 1′ ⋂ R 2′, where ∩ denotes any fuzzy conjunction operator (here, ⋂ = min) and

$$ \begin{array}{*{20}c} {R_{1} \prime = \mathop \sum \limits_{U \times V \times W} \mu _{R_{1}} (u,v)/(u,v,w),} \\ {R_{2} \prime = \mathop \sum \limits_{U \times V \times W} \mu_{R_{2}} (v,w)/(u,v,w).} \\ \end{array} $$

We modify R′ with dissimilarity s1 = 1.0 as we get μ R* = (u, v, w) = 1 − (1 − μ Rs 1 and we get

$$ R = projR^{*} \,{\text{on}}\,\,U \times W $$

Let us extend the fuzzy sets ‘HIGH’ cylindrically in the premise r on U × W as

$$ R_{3} = \mathop \sum \limits_{U \times W} \mu_{HIGH} /(u,w); $$

and compute R  = RR 3 by

$$ \mu_{R\prime \prime } (u,w) = T(\mu_{R} (u,w),\mu_{R_{3}} (u,w)), $$

taking fuzzy conjunction ∩ as t-norm T (here, ∩ = min);

Next, we calculate the dissimilarity measure of the fuzzy set not HIGH in p and the fuzzy set HIGH in r (denoted by s 2) and R is induced by the dissimilarity measure s 2 = 1 to get R ** as

$$ \mu_{{R^{**} }} (u,w) = 1 - (1 - \mu_{{R^{\prime \prime } }} (u,w)) \cdot s_{2} ; $$

At last, we project R ** on W such that

$$ \begin{aligned} C\prime & = \mathop \sum \limits_{W} \mathop {\sup }\limits_{v} \mu_{{R^{**} }} (u,w) \\ & = 0.50/0 + 0.50/25 + 0.50/50 + 0.25/75 + 0.0/100 \\ \end{aligned} $$

and S(C′, not HAPPY) = 0.75, which is rather similar to not HAPPY.

(ii) For Observation 2: In this case, the observation is changed into

$$ r:{\text{The}}\,{\text{prime}}\,{\text{interest}}\,{\text{rate}}\,{\text{is}}\,very\;HIGH $$

to the scheme given in Table 15.

Describing the membership grades of the fuzzy set ‘very HIGH’ in q as a 2, where a is the membership grades of the fuzzy set ‘HIGH’ defined over U, defining other parameters in the same way and executing in a similar way, we can derive a fuzzy set

$$ C^{\prime } = 0.46/0 + 0.46/25 + 0.46/50 + 0.37/75 + 0.16/100, $$

the similarity of which is 0.71 with the fuzzy set not HAPPY in the premise q, whenever dissimilarity between ‘not HIGH’ ⊂ U in premise p and ‘HIGH’ ⊂ U in observation r is 0.84.

Hence, in either case, we can derive a conclusion like ‘people are not so happy’ for the given observations. Therefore, our resolution method is effective in deriving a conclusion from some given statements in real life.

6 Conclusion

This chapter presented a resolution principle for fuzzy formulae based on similarity and approximate reasoning methodology. Similarity is inherent in approximate reasoning and resolution deduction can be used as a rule of inference to generate new clause from a given set of clauses. The essential idea of resolution of two clauses is to search for a literal in a clausal formula that is almost complementary to a literal in the other form. The clause formed by the disjunction of the remaining literals and subsequent removal of the pair of almost complementary literals is a logical consequence. If we put the resolvent in the set of clauses its behaviour (satisfiability) never changes. It can be applied directly to any set S of clausal formulae (not necessarily to ground clauses) to test the (un)satisfiability of S. To test the unsatisfiability it checks whether S contains the empty clause, (as a resolution deduction). This could be a powerful technique in constructing a proof of a theorem using refutation procedure. Examples cited in the chapter attempted to demonstrate how resolution can be effectively used to construct a proof of a theorem or to make a decision in real life. Inverse approximate reasoning may be applied to model different goal-directed search techniques. We apply inverse approximate reasoning method to avoid the inherent problem of GMP. Instead of testing complementary literals we use dissimilarity concept of fuzzy literals.