Lock, Linear Lambda-Paramodulation in Operator Fuzzy Logic

ABSTRACi'

The author proposed concepts of Operator Fuzzy Logic and A-Resolution in 1984. He and his cooperaters have obtained some theoretical results. This paper introduces A-paramodulation to handle a set of clauses with the predicate of equality, and thus the equality substitution can be used in fuzzy reasoning. Then the A-paramodulation method is proved Lo be complete with ~-lock-semantic method. Finallj, Yang Fengjie and I have improved the A-paramodulation, and proved that the linear A-paramodulation is complete too.

I · INTRODUCTION

The author proposed concepts of Operator Fuzzy Logic( or OFL for short) and ]\,-Resolution in 1984. During the past few years (1985-1987), he and H. Xiao, then he, K.Y.Fang, Carl.K.Chang and Jeff. J-P Tsai working together on the A.-resolution method obtained a series of results ·. \~e proved that a A-resolvent of two fuzzy clauses C1 and Cz is a A.-logical concequence of C1 and Cz , and that ~-resolution method is complete for ~-inconsistent set of clauses. We explained the practical meaning of fuzzy reasoning based on A.-resolution method in OFL. From the above results, we can see that some theorems which can not be proved with the traditional logic, can be proved fuzzily by using )\.;-resolution method in our logic system.

Equality relation is a very important relation in mathematics. This equality relation has some important special properties: it is transitive and can substitute equals for equals. Thus it is natural that the transitive and substitutive properties of fuzzily equality are needed in proving fuzzy

theorems.

Liu XuHua

DepL. of Camp. Scie. Jilin University Changchun, f'HC.

This paper proposed a ~-paramodulation to handle fuzzy equality. In conjunction with )I.-resolution, A.-paramodulation can be used to prove fuzzy theorems in OFL. We proved that A-paramodulation is complete for the A.-inconsistent set of clauses in conjunction with A.-resolution.

I I · l''UtlDAWIThL CONCEPTS AND PROPERTIES

From [1-3], we Fuz zy Logic is built and interval [0,1] is if we define: know that Operator on operator lattice an operator lattice

for any x,y [0,1].

In the following discussion, we assume that OFL is built on interval [ 0,1] and the amount of operator .A is finite.

These concepts such as literal, truth-value lattice, fuzzy interpretation, operator formula, T1 (G) of formula G under I, .A-complemented literal, A-identical literal, can be

found in Refs. [1-3].

Definition 1. Choose arbitrarily~E[O,l]. Formula G is called ~-valid if and only if for every I there exists T1 (�)~~; G is called ~-inconsistent if and only if for every I, there exists T1 (G),l\..

Obviously, Formula G is ~-valid if and only if Formula ( ,_ G) is (1-~l -inconsistent.

Definition 2. Let C1 and Cz be two clauses without the same variables and ~1 L1 and A-2 L2 be two literals of C1 and Cz respectively. If L1 and L2 have a Host Gen$ral Unifi~r ( MGU for short l t1 , and l\.1 L1 and J\2 12 are ]\.-complemental, then

(Cf- S1)U(C~-S2)

is the binary A-resolvent for Ct and C2 , denoted by R.._ ( C1 , C2 ) , where

If I is an interpretation of S and Tx (K~)>X, we can obtain results obviously as follows:

1. Tx( (()(:.;..) )=T for any term o(in S. 2. If Tx ((~=~))=T, because Tx (K~)>~, thus

Tx ( (1->...* )(ct=f)V]I.; (#J=o() l>A, therefore, there must be

Tx ( ~=ol) )=T.

3. Let Tx((ol=fS))=T, TI(((J=Y'))=T. According to TI(KA.)>}\, thus TI((1-~* )(ot.=P )V(l-N )(~=Y)V}..*(~=Y))>h,, there must be Tx ( (~=Y) )=T

4. Suppose Tx ((~=~))=T,

Tx (P( ... 0(. .··· ) )=T. Since

Tx ( ( 1-X* ) (CI(= ~)V( 1-).* )P( ... 0( ··· )

V ]...*P( ·.. ~· .· ) )>J\,

there must be Tx(P( ..· ~ .·· ))=T. Similarlyi we can easily see that if Tx ( (ct=~) )=T, TI(P( .·· p ... ) )=T, then there must be TI(P( .·. 0(. ··· ) )=T, namely,

TI(P( .· ·d..· ·· ) )=TI(P( ... tJ ··· )).

From the above discussion, we can easily see that I is an E-interpretation of S.

Therefore, we can obtain a theorem as follows:

Theore· 1. Let S be a set of clauses and KAbe the set of~-equality axioms for S. For any interpretation I of S, I is an £-interpretation if and only if Tx(kA)>J\.

Theorem 2. Let S be a set of clauses and KA be the set of }\-equality axioms for S. Then S is J.E-inconsistent if and only if (SUK-..) is }..-inconsistent.

( =* ) Suppose S is AE-inconsistent, but ( SUK~ ) is not }\-inconsistent. Then there exists an interpretation I such that Tx ( SUKA) >)\.

Thus Tx (S)>~ and Tx IK,..)>~.

From theorem 1, we know that I must be an E-interpretation. From Tx (S)>}\ 1 we know that S is not J\E -inconsistent, which contradicts the assumption that S

is~E -inconsistent.

( 4:=" ) · Suppose is }\-inconsistent, but ( SUK" s is exists that not )£ -inconsistent. Then there an E-int.erpretation IE such TIE(S)>J\. Clearly, TxE(K,.. )> 7\. Tx E ( ( SUK-.. ) ) > ]\. . This contradicts Hence the ) assumption that (SUKA is ).-inconsistent.

IV .~ARAMOOULATION

Definition 9. Let J\~0.5 and C1, Cz be two c lauses without any variables in common such that

k!L[t]VC1', J\l>J\.or J\1<1-1\, J\2 ( r=s )VCz ', 7\~1\,

where N.L[t] is a fuzzy literal containing ·the t.erm t and C1' and Cz' are clauses. If t and r have MGU tr , then 'J\* L'" [ s'"} uci"' uc2'"

is called a binary }\-paramodulant of C1 and Cz, NL[t] and 7'.z(r=s) are calledA-paramodulated literals where L'"[s'" ] denotes the result obtained by replacing one single occurrence of tr in L'" by sr 1 and

1\* = j(JI.i+Al )/2 when J\1>7\,

1 (J\1 +1-]1.2 )/2 when J\1 <1-ll..

Definition 10. A J\-paramodulant of C1 and Cz is a binary J\-paramodulant of C1 or all. -factor of C1 and C2 or a >...-factor of Cz, denoted by PA(C1,C2 ).

Definition 11. LetS be a set of clauses; G and H be two clauses in S. If TxE(H)>7\ when Tt!(G}>)I. for even E-iuterpretation h of S, then it is said that G AE-strongly implies H, denoted by �~H.

Theore· 3. Let C1 and Cz be two clauses,}\ ~0.5, and suppose P~(C1 ,Cz) is a )1.­ paramodulant. Then

(CiACz)~P,_!Ct, Cz).

Without loss of generality, we may assume that C1 is J\1 L[1; )VC1', Cz is J\2 (r=s)VCz' , P,_ (C1, Cz) is a binary ]1.-paramodulan t, with >..2 > A · Let MGU of t and r be !T , h be any one of E-interpretation such that

Tr E ( Ct ) > }\ and Tt! ( C2 ) >)...

Then, Obviously, we have TtE (C{}>}\ aud TH (C;")>}\.

(Notice: every variable in C1 and Cz is considered to be governed by a universal quantifer). Choosing au arbitrarily ground instance of C1 and a ground instance of Cz , we have the following considerations:

1. For 1\i >A

If Tx!(L,.[t·] l=F, Then TxE(d'" )7/\ ,thus Tu (P~(Ct ,Cz) }>J\..

If TIB(Lr[t·]J=T, we ltave 'I'o:(L· [s""ll=T;

because t""=r·and rr=s·, we know A*>/\

(~* occurring in the definition of P,_(C1, Cz)), therefore Tu:(P,.(Cl,Cz})>)l..

2. For ~1< A.

similarly tb the above proof, we can also obtain

T1 E ( P,. ( C1 , Cz ) ) > }\.

According to the above proof, we have the following fact:

(C1AC2 )$-P"(C1, Cz).

Q.E.D.

Definition 12. Lel Ct and Cz be two clauses, where evex·y l.ileral is locked with an integer and 7\ ~0. 5 and let P"(C1, Cz} be a X-paramodulant. Suppose

1. C1 and C2 are 1\-positive clause, namely, every fuzl!ly literal )\,.*L in clauses satisfies >...* ~l-}\.
2. the paramodulated literal of Ci contains the smallest lock in Ci(i=1,2). Then P ,.. ( C1, C2 ) is called

a 1\. -lock-hyperpa r·amod11lant, or a 1\.-LH-paramodulant for· short. Definition 13. Let )1.~0.5. A fiuile set of clauses {E1, ... ,Eq ,N} where every lite ral is locked with au integer is c alled a 1\.-lock-hypersemantic clash (or A-LH-Clash for short) if and only if E1 , ... , Eq satisfies the following conditions:

1. E1 , ··· ,Eq are ).-positive clauses. 2. Let Rt=N. For each i(1<i<q), there is a ~-resolvent Ri+l of Ei and Ri.
2. The resolved literal of Ei contain& the smallest lock in Ei.
3. Rq+l is a ~-positive clause, where Rq+l is called a ~-LH-resolvent.

Theore· 4. let S be a set of clauses, where every literal is locked with an integer and ~~0. 5. If S is ,\­ inconsistent, then there is a deduction of }\-empty clause fro· S by the }\-LH-resolution ·ethod.

proof. see [ 3].

Definition 14. Let S be a set of clauses and /\~0.5. The set F,. of ~-functionally reflexive axioms for S is the set defined as

FA= {J\.* ( f ( Xl , , ·. , Xn ) = f ( Xl , , , · , Xn ) ) } , where ~ * E [ 0, 1] and ]\. * > ]I.. and f is any funct i on symbol occurring in S.

Defi nition 15. Let A~0.5. The fuzzy literal ,\,*L is called a ,\-irrelevant literal if 1-)>,(~*~J\·

Definition 16. let C1 and C2 be two clauses. If we can build the one-to-one c orrespondence between the literals of C1 and of C2 such that the two corresponding literals are either )'..-identical or A.-irrelevant, then C1 is called ,\­ identical with Cz.

Theore· 5. Let ,\.~0. 5, C1 and Cz be two clauses, C be a ~-lock-resolvent or a }\-lock-paramodulant of C1 and Cz · If C1* and C2* are ).-identical with C1 and C2 respectively, then there is a A -lock-resolvent C" or a )..-lock-paramodulant C' such that C' is ).-identical with C.

Proof 1. Let C1 be )\.1 L1 VC1 ' and C2 be J\.2L2VC2', where }\I>J\.and }\,2 <1-A.,. Let C=(C{ -,\1Li )U(cr -)\2Lf ),

where~ is an MGU of L1 and L2.

It is c lear that C1* and C2* are two clauses as follows:

J\I*LIVCI*', .\2*L2VCz* ', where A.t*>.\., ~2*<1-)..., C1*' and C2*' are Mdentical with C1' and C2' respectively.

Let rr rr ~ ,.~ r C*=(CI* -)u*Ll )U(Cz* -....:*Lz ). Obviously, C* is a ~-resolvent of C1* and C2 * and is also a ]I.-lock-resolvent, C* being }\-identical with C.

2. We might as well assume that C1 is AIL[t]VCI' and Cz is 1\.z(r=s)VCz', where~~>~ and A2>\. Let C·A.JL,.[s,.]VCI '~VCz , .. ,

where /\.3 =( '?..! +).z )/2 and <1' is an MGU of t and r.

Then, C1* and Cz* are two clauses as follows:

>-2· ( r=s )VCz *',

).I*L[t)VCI* ',

where Al * > )\, 'XJ. * >A , C1 * ' . \-identical with C1' and C2' Let and Cz *' are respectively.

where }\3*=(7\.t*+)l.z*)/2. Obviously, C* is a ~-lock-paramodulant and is }\-identical with C. Q.E.D.

Theore· 6. Let .\ ~0. 5 and S be a set of clauses, where every literal is locked with an integer. Then, S is AE -inconsistent if and only if there is a deduction of ,\-e·pty clause fro· (SU{ )\.* (x=x)}UF,._ ) by }\-LH-resolution ·ethod and )1.-LH-para~~Jodulation IIJethod, where :11...* >A and F11. is the set of )\.-functionally reflexive axioms for S. (}\-e·pty clause is co·posed of~irrelevant literals, denoted by )\.-Q.)

( ::> ) · Suppose K,. is the set of ~-functionally reflexive axioms for S. Because S is XE -inconsistent, we know from theorem 2 that ( SUK,.. is ,\-inconsistent. From theorem 4, we know that there is a A -LH-resolution deduction.- D of ).-empty clause from ( SU~ ). We now show that D can be transformed into the deduction satisfying this theorem.

For each 1\.-LH-clash ( E1 , ..· , Eq , N) in D, since E1, ... , Eq are }\.-positive clauses, E1 , ... , Eq must be in S or J\.*(x=x). If N~S, then the clash is the desired one. If N 6- KA , N is clearly not )\.*(x=x). Then we have the following four possible cases:

1. N is ( 1-"-~ J(x=y)V~ ( y=x) and '/1...* > )\.. Obviously, there must be q=l and E1=( Al(ti=tz)VEl'), where Al>A Therefore,

(E1, N)=!X:(tJ.=t&)VEl').

In addition,

P,..( )\.} (x=xl, ~ ( t1 =tz )VE1 ')

=(l.l (tz=t1 )VE1 ').

Because (El, N) is a )\.-LH-clash, P,._ ( "-l(x=x), E1) must be a }\ -LH-paramodulant and { E1 , N) is ?~.-identical wllh P~~.(Xl(x=x), E1 ).

2. N is (1-}\*)(x=y)V(1-A*)(y=z)V ~( x=z) and :11..* > )\.. Obviously, we have q=2 and two clauses E1 and E2 as follows:

Al * ( t1 =tz )VE1 ',/1.2* ( s1 =s2 )VE2', whereX1*>)\, .\z*>A. Thus,

(El, Ez, N)=(>-::(t{ =s2cr)VEl',.VE2',.), rbeing an MGU of tz and s1. Clearly, P"-(El ,Ez l=C~1*+.\z* l/2(ttr =Sz"' )VE1 'rVEz .r. We can see that P,_ ( E1, E2) is a X-LH-paramodulant and "- - identical with ( E1 , Ez , N).

3. N is (1->..* )(xj=xo )V( 1-:11..·

)P( ··· xj ··· )V7I: P( ··· xo ·.. ), with X* >)1.. Obviously, we have q=2 and E1 and E2 are two clauses as follows:

>v (tj=to )VE1 ', ~P( · · · sj ... )VEz ', whereA1 >:II... and A2 >)\.. Thus

(E1, E2, N)=()\.*P(s{ · · . tf" . .. s~)VE1 ·rvEz'r),

where tr is an MGU of ( Xl ·.· tj .·. xn ) and ( Sl , · , Sj , , , Sn ) ·

Clearly, Pa_(Ez, Ell=(Xl+l\.z)/2P(sf ... tr .·. sncr )VEl ·rvEz ,.,. ·

We can see that P l\ (Ez, Et) is a ~-LH-paramodulation and ~-identical with ( Et , Ez , N).

where A*>;\.. Obviously, we have q=1 and E,is a clause

as follows:

where ~t>},.. Thus,

( Et , N) =

IX* (f(xt .·· tj ..· xn )=f(xt ··· to ... xn) )VEt') Clearly, A.-paramodulant of

At ( f(xt ..· xj ·.. xn )=f(xt .·· xj ... xn)) and Et is a clause as follows:

P" ().t ( f = f ) , E t ) = ( At ( f ( X1 ... tj ... Xn ) = f ( Xt ..· to ..· Xn ) ) VEt ' ) We can see that P ~ ( '1\.t ( f= f) , E1 ) is a X-LH-paramodulant and )\.-identical with ( E1 , N).

From Theorem 5, we know that each ~-LH-Clash in D can be transformed into a 1\,-LH-paramodulant of two clauses which belong to the set (SU{).._*(x=x)}UF,.).

Therefore, we obtain a new deduction D' of ,X-empty from (SIJ{~*(x=x)}UF,.) by using -LH-resolution method and )\.-LH -paramodulation method.

( /p ) · If there is a deduction of ~-empty clause from (SU{J\..*(x=x)}UFJ\.) by using )\-LH -resolution and X,-LH -paramodulation, but S is not >.E-inconsistent, then there is an E-interpretation h such that TIE(S) > )\. Thus, for each clause C in (SU{~*(x=x)}UF,_), there must be TII!(Cl>A· From Property 11, Property 12 and theorem 3, we can easily see that TIE()\.-Q)>A,, which contradicts the definition of >..-c. Q.E.D.

V. LINEAR. )..-PUAMODUI,AT!ON

Definition 17. Given .a set S of clauses and a clause Co in S, a linear )._-deduction of Cn from S with top clause Co by )\_-resolution and )\_-paramodulation is a deduction of the form shown in Fig. 1, where

1. For i=1, ... ,n-1, Ct+t is resolvent or a )._-paramodulation (called a center clause) and Bi ( a side clause). a A.­ of Ci called

2. Each Bi is either inS, or is a Cj for some j <i.

A Linear A-refutation by '~\,-resolution and >.,-paramodulation is a linear X-deduction of '1\,.- 0 by 1\-resolution and )._-paramodulation.

Definition 18. Let Ai0.5, and S be a set of clauses. Sa is said to be a >..-reduction of S if and only if SR is obtained by the following replacing: for any 1 i teral )1..* L 5,

1. if .).*~>,.and 1-Xp,,*, delete '1\.."'L.

2. if 7\.*>).., X*L is replaced by L.

3. if 1-'1\.>>..*, ,\*Lis replaced by_..L,

Let Sa denote the '~\,-deduction of S, Ca denote the >..-deduction of C.

Theorem 7. Let C1 R and Cz a be the 7\.-reducing clauses of C1 and Cz respectively. If C' is a resolvent ( or a paramodulant ) of C1 a and Cz a , then there is a A.-resolvent ( or a 1\-paramodulant) C of Ct and Cz such that C\1 =C '.

Proof. If C' and Cz 1 , we know correct. [1 is a that resolvent of C1 a this theorem is

If C' is a paramodulation of Cta and Cla, without. loss of generality, we may assume that C' is a binary paramodulant, let

C1='1\.tL[t1VC1', >..1 > '1\.or ~1<1-X, Cz=~z(r=s)VCz ', Az >.\.

But when >.t >A, ( \t +Al ) /2 > }\. and when Xt<1-~, (\1+1-A.z )/2<1-A.

Theore· B. If C is a clause in an A.E -inconsistent set S of clauses including A.* (x=x) and the set F,. of A.-functionally reflexive axio·s for S and if S-{C} is A.E-sat .isfiable, then. S has a linear A-refutation by >..-resolution and '1\,-para·odulation with top clause C.

Proof. According the theorem above we know that S is AE -inc onsistent it and only if ( SUK~) is '1\..;- inconsistent if and only if SRUK is inconsislent. (K is theA, -reducti.on of K,. ) ·

Since S-{C} is >-_E-satisfiable, clearly, SR-{CR} is E-satisfiable, then SR has a linear refutation D by r e solution and paramodulation with top clause CR [ 4- ] . By theorem 7, for every res o lvent R(ClR, C2R) or paramodulant P(ClR, CzR) in D, there is a ~-resolvent R (C1 ,Cz) or ~-paramodulation P~(C1, Cz ), and

R(CIR, C2R)=(RJ-.(Cl,C2))R

P(CIR, C2R)=(P,..(Cl,C2))R.

Therefore, we can obtain a linear deduction of ~-empty clause from S, by ,X-resolution and ~-paramodulation.

Up to now we have obtained ~-paramodulation method in operator fuzzy logic. This is an infere nce rule for the fuzzy equality relation. ~-paramodulation is essentially an extension of the fuzzy equality substitution.

Because OFL describes fuzzy the ~- propositions naturally [6], combination of ~-resolution and paramodulation is fuzzy reasoning. convenient in doing