Äîêóìåíò âçÿò èç êýøà ïîèñêîâîé ìàøèíû. Àäðåñ îðèãèíàëüíîãî äîêóìåíòà : http://www.intsys.msu.ru/magazine/archive/v11(1-4)/mironov-219-260.pdf Äàòà èçìåíåíèÿ: Mon Feb 18 14:02:36 2008 Äàòà èíäåêñèðîâàíèÿ: Tue Oct 2 00:08:20 2012 Êîäèðîâêà: ISO8859-5

. .
, . , F K .

1.
. , , , , . . . , , . , , , .


220

. .

. , , , . . . 1) , . , , . , . 2) , . . , . , , [3]-[14]. . . . , ,




221

(., , [2]). , . . , .

2.
2.1.
, (B , ), , Q B , inf (Q) sup(Q) B , b B (q Q b (q Q q q) b) b inf (Q), b. sup(Q)

inf (B ) sup(B ) 0 1 . Q = {a1 , . . . , an } B inf (Q) sup(Q) a1 . . . a
n

a1 . . . a

n

. a1 ... an .

a1 ... an


222

. .

B , a, b B ab : c B c (a b) (c a) b (2) (1)

(1) ab B . a, b B a b (a b) (b a).

2.2.
P V , p p p. F m p ( ) p p: Ç P V . Ç B . Ç A B , A B , A B , A B . Ç A , a B , 2 a A . 2a . 2a A




223

, A, a. A1 , . . . , An F m A1 A 2 . . . A n A 1 A 2 . . . A n A1 (A2 (. . . An ) . . .) A1 (A2 (. . . An ) . . .) . A1 A1 ... ... An An . A, B F m A B (A B ) (B A).

2.3.
F m = ((p1 , . . . , pn ), (A1 , . . . , An )) n 1 . (3)

Ç (p1 , . . . , pn ) , Ç (A1 , . . . , An )

F m , , : A F m Ç A = pi {p1 , . . . , pn }, (A) = Ai ,
def


224

. .

Ç A P V \ {p1 , . . . , pn }, A = a B , (A) = A, Ç A B C, B C, B C, 2a B (A) (B ) (C ), (B ) (C ), (B ) (C ), 2 a (B ) .
def

2.4.
A B F m. , B A , Ç A a b, a b, a b a, b B , Ç B A B , a, b. F m , . A , , , A, (p1 , . . . , pn ). A , (3), , i {1, . . . , n} A i = ai B

(A) 1 B .




225

2.5.
L F m, : Ç L Ç A, B F m a B 2
a

A B



2a A 2a B L,

L,

(4)

Ç a B a 2a 1 (5) Ç A F m a B 2a A a Ç A, B F m A L A B L B L (7) L, (6)

Ç A F m A L (8) (A) L Ç A, B F m a, b B a (A B ) L a (2b A 2b B ) L (9)

Ç A F m {a i | i }B i ai A L (10) (sup ai ) A L.
i


226

. .

, ( ) , F K ( Fuzzy Kripke). , L : a1 A
1

L, . . . , an A

n

L



. A L [[A]]
L

a1 , . . . , an B , A1 , . . . , A n F m a1 A1 ... ... L. an An

(11)

{a B | a A L}. (12)

(10) a B aA L a [[A]]L .

3.
Ç , Ç Ç , Ç , [1].




227

3.1.
W = (X, Å) ÇX ÇÅ ( W ), Å:X çX B : x, y X x, y , z X Å(x, y ) = Å(y , x) Å(x, y ) Å(y , z ) Å(x, z ) (14) (15) (13)

x, y X Å(x, y ) x y . x X Å(x, x) x (13). (13) R R:X çX B : R(x, y ) Å(x, x ) x, y , x , y X Å(y , y ) x, y X R(x, y )

R(x , y ),

(16)

Å(x, x) Å(y , y )

.

(17)

(x, y ) X ç X R(x, y ) R.


228

. .

(13) s s:XB : x, x X x X s(x) Å(x, x ) s(x) s(x ), (18) (19)

Å(x, x).

x X s(x) x s. (13) S ub(W ). W W , x, y x y W (x, y ). , x W W (x) x W .

3.2.
M M = (W, {Ra | a B }, ) (20) : 1) W , , 2) {Ra | a B } B - W , , 3) : P V S ub(W ) (21) . .




229

3.3.
A F m (20) A M [[A]]
M

: W B,

x W [[A]] x B , : Ç p P V [[p]]x = (p)(x), Ç a B [[a]]x = Ç Ç Ç [[A B ]]x = Ç
def def def

(22)

a W (x)

,

(23) (24) (25) , (26)

[[A B ]]x = [[A]]x [[B ]]x , [[A B ]]x = [[A]]x [[B ]]x , [[A]]x [[B ]] W (x)
x def

def

, [[A]] W .

a def inf (Ra (x, y ) [[A]]y ) [[2a A]]x = . yW W (x)
M

(27)

-

3.4.
A F m x (20), [[A]]x = W (x). (28)


230

. .

A F m (20), . , F K . , Ç , Ç (4), (5) (6) , Ç (7), (8), (9) (10) . : , F K .

4. L-
4.1.
L F m , a B , a , x, aL a = 1. (29)

F K . 3.4, a B , F K , a , (20), W W (x) = 1. (30)

(29) (23), (28) (30). . .

4.2. L-
ÇL ,




231

Çu

F m.

u L-, Ç u, {a1 A1 , . . . , an An } ( a1 , . . . , an B , A1 , . . . , An F m) Ç b B A .. A
1

(31)

.
n



b

L

(32)



4.3. L-
u1 , u2 F m u , a A u a = 0 b a : b A u2 .
1 1

a1 ... an

b.

(33)

u

2

1. u1 , u2 F m u1 u 2 , u
2

L-, u1 L-.

2. L L- .


232

. .

. (11) (31) L, a1 A1 ... ... (34) L. an An (32), (34) (7) a1 ... b L an

(35)

(35) (29) (33). . L . 3. Çu ÇA ÇQ L- , , a B , , u {a A} L-. (36)

a B a sup(Q) a Q.

. , Q = , 0 Q. a Q a sup(Q) . a sup(Q) aQ :




233

1) u {sup(Q) A} L- 2) u {a A} L-, a a (37)

u {a A} L-. 2 1. 1: Ç (31) (37), Ç b B (32) (33). u L-, (32) (33) , (31) : Ç (a1 A1 ) = (sup(Q) A) Ç i = 2, . . . , n (ai Ai ) u.

(33) : sup(Q) a2 . . . a (38) aQ a a2 . . . a b
n

b
n

(38)

(39)

(39) (36). .


234

. .

sup(Q), A u, [[A]]u (40) [[A]]u , u F m u L- A F m u {[[A]]u A} L- 4. u1 u
2

(41)

L- , , u
1

u2 .

A [[A]] . Ç u2 {[[A]] L-, Ç u1 {[[A]]
u
2

u

2

[[A]]u1 .

(42)

u

2

A}

A}

u2 {[[A]]

u

2

A}

1 , u1 {[[A]]
u
2

A}

(43)

L-. L- (43) [[A]] (42). . 5. Ç u Fm Ç A, B L- ,

u

1



, , AB L (44)




235

[[A]]
u

[[B ]]

u

(45)

. (45) L- u {[[A]]u B } , Ç (31) (46), Ç b B (32) (33). u L-, (32) (33) , (31) : Ç (a1 A1 ) = ([[A]]u B ) Ç i = 2, . . . , n ai A
i

(46)

u

(47)

(32) A2 b) L B ( ... An (44) (48) A2 A ( ... b) An L

(48)

(49)

A A2 b ... An

L

(50)


236

. .

u {[[A]]u A} L-, (47) (50) [[A]]u a2 b (51) ... an 6. Ç L- u, Ç A F m : [[A]]
L

(33) . .

[[A]]

u

(52)

. (52) L- u {[[A]]L A} , Ç (31) (53), Ç b B (32) (33). u L-, (32) (33) , (31) : Ç (a1 A1 ) = ([[A]]L A) (53)




237

Ç i = 2, . . . , n ai A
i

u

(54)

(32) A2 A ( ... b) L An [[A]]L A L (55) A2 b) [[A]]L ( . . . An L

(55)

(56)

u L-, (54) (57) a2 [[A]]L b ... (58) an (58) (33). .

(56) A2 ([[A]]L b) ... An

L

(57)

5. L-
5.1. L-
x F m. x L-, Ç x L-, Ç A F m [[A]]x A x. (59)


238

. .

5.2. L-
Çu Çx L- , L- .

x u, u x (60)

7. L- u x. . B1 , B 2 , . . . F m. u1 , u 2 , . . . F m : Ç u1 = u, Ç k 1 u
def k +1 def

(61)

= uk {[[Bk ]]

u

k

Bk }

(41) , k 1 : uk L-, uk+1 L-. k 1 u
k

(62)

u1 L-, (62) , L-




239

x : x=
def k1

u

k

x L-, (31) k 1, , u k (, , L-). , A F m (59). (61), k , , A = Bk . [[Bk ]]uk Bk x [[Bk ]]
u
k

[[Bk ]]x .

(63)

uk x, 4 , [[Bk ]]
x

[[Bk ]]uk .

(64)

(63) (64), [[Bk ]]x = [[Bk ]]uk . , [[Bk ]]x B
k

(65)

= [[Bk ]]

u

k

B

k

u

k +1

x.

(66)

(66) (59) ( A = Bk ). , x L-. , x u, (a A) u x, k 1: A = Bk . a [[A]]x .


240

. .

(a Bk ) u u uk {a Bk } (67) (65) : a . [[Bk ]]
u
k

k

L-.

(67)

= [[Bk ]]x = Ax .

6. L-
8. x L- , a B . [[a]]x = a. (68)

. x L-, {[[a]] x a} : b B ab [[a]]
x

L

(69)

b

(70)

(69) b = a, (70) b = a, [[a]]x a. (71) L- x {a a}. (72) , Ç (31) (72), Ç b B




241

(32) (33). x L-, (32) (33) , (31) : (a1 A1 ) = (a a) i = 2, . . . , n ai A
i

x

(73)

(76) L- x a2 ... an

(74) A2 ... (a b) An

(33) a a2 ... an

(32) a A2 b L ... An

(74)

b

(75)

L

(76)

(75) (77). .

ab

(77)


242

. .

, B : a B (a 0) 0 = a. (78)

, , B , : a, b B a b = inf {a, b}, 9. Ç L- x, Ç A, B [[A B ]]x = [[A]]x [[B ]]x . (79)
def

a b = sup{a, b},

def

?a = a 0.

def

. (79) [[A B ]] [[A]]x [[B ]]
x x

[[A]]x [[B ]]

x

(80) (81)

[[A B ]]

x

(80). [[A B ]]x [[B ]]x (82) [[A]]x (82) L- x{ [[A B ]] [[A]]x
x

B}

(83)

, Ç (31) (83),




243

Ç b B (32) (33). x L-, (32) (33) , (31) : [[A B ]] [[A]]x Ç i = 2, . . . , n Ç a1 A
1

=

x

B

ai A

i

x

(84)

(33)

(32) A2 B ( ... b) L An [[A B ]] [[A]]x
x

(85)

a 2 ... an A AB

B

b

(86)

, A AB B L (87)


244 (85) (87) , A AB

. .

(88) A AB A 2 ... An

A ( .. A

2

.
n



b)

L

(88)

x L-, [[A]]x A x x (90) (91)

b L

(89)

[[A B ]]x (A B ) (89), (90), (91), (84) L- x (86). (81). L- x {([[A]]x [[B ]]x ) (A B )} , Ç (31) (92), Ç b B (32) (33). x L-, (32) (33) , (31) : (92)




245

Ç a1 A

1

=

([[A]]x [[B ]]x ) (A B )

Ç i = 2, . . . , n ai A
i

x

(93)

(32) A (A B ) ( . . A
2

.
n


x

b)

L

(94)

(33)



, (96), : b0 a2 [[A]]x (97) ... an b0 a2 ... an [[B ]]x 0 (98)

(95) b0 a2 [[A]]x (96) [[B ]]x 0 ... an

[[A]]x [[B ]] a2 ... an



b

(95)


246

. .

(97). x{

L b0 a2 A} ... an

(99)

,

Ç (99) {c1 C1 , . . . , c , c1 C
1 m

Cm }

i = 2, . . . , m Ç d B A C2 ... Cm

b0 a2 = A ... an ci C
i

x

(100)

d

L

(101)



b0 a2 ... an c2 ... cm

d

(102)




247

(102) a2 . . . a n c2 . . . c m (b 0) d (103)

C2 (( . . . d) B ) (A B ) Cm (104) (94) A C2 d) B ) ( . . (( . . . Cm A
2

(101) C2 d) L, A ( ... Cm L (104)

.
n



b)

L

(105)

(106), (93), (100) L- x [[d B ]]x a2 . . . a n b c2 . . . c m

, L. (105) dB A2 . . . A n b L (106) C2 . . . C m

C2 C2 ... d) B ) (( . . . Cm Cm dB


248

. .

a2 . . . a n c2 . . . c m [[d B ]]x b (107)

, [[d B ]]x b (108) [[d B ]]x b b0 [[d B ]]x b b0 [[d B ]]x 0 d (109) (b 0) d (108)

(109) [[d B ]]x 0 (110) d0 [[d B ]]
x

d

(110)

(111)

(111). (d 0) (d B ) , , , (d 0) (d B ) L (112)

(112) 5 [[d 0]]
x

[[d B ]]

x

(113)

(113) 8 (111).




249

(111) (108), (107) (108) (103). , L- (99) , , , (97) . (98). [[B ]]x a2 b (114) ... an (114) , 1) (94) B (A B ) A B ( .. A
2

L

.
n



b)

L,

2) {([[B ]]x B ), (a2 A2 ), . . . , (an An )} x, 3) x L-. . 10. Çx Ç A, B L- , .

B A2 b L, ... An


250

. .

[[A B ]]x = [[A]]x [[B ]]
x

(115)

. (115) [[A B ]] [[A]]x [[B ]]
x x

[[A]]x ,

[[A B ]]

x

[[B ]]x ,

(116) (117)

[[A B ]] L L

x

(116) (A B ) A (A B ) B

5. (117) L- x {([[A]]x [[B ]]x ) (A B )}. . 11. Çx L- , Ç A, B . [[A B ]]x = [[A]]x [[B ]]x . . (118) ([[A]]x [[B ]]x ) 0 = [[A B ]]x 0 (119) : ([[A]]x [[B ]]x ) 0 = = [[A 0]]x [[B 0]]x
x

(118)

(119)

[[A]]x 0 [[B ]]x 0 A0 B0 ]]
x

=

[[A]]x [[0]]x [[B ]]x [[0]]x
x

= =

= [[

= [[(A B ) 0]]

= [[A B ]]x [[0]] .

= [[A B ]]x 0.




251

12. x L- . A F m a B (120) [[2a A]]x a. . (6) (a 0) (2a A 0) L (121)

, 5 8, a0 [[2a A 0]]
x

(122)

, 9 8, [[2a A 0]]x = [[2a A]]x [[0]]x = [[2a A]]x 0 (122) (123) a0 [[2a A]]x 0, (124) (123)

(120). .

7.
7.1.
L M
def L

= (WL , {(RL )a | a B }, L )

: Ç WL L- . x, y WL WL (x, y ) =
def AF m

inf ([[A]]x [[A]]y )

(125)

, x W
L

WL (x) = 1.

(126)

, W L (14) (15).


252

. .

Ç a B (RL )a WL (RL )a : WL ç WL B : x, y W (RL )a (x, y ) =
def AF m L

inf ([[2a A]]x [[A]]y )

(127)

, (R L )a (16) (17). Ç
L

L : P V S ub(WL )

p P V L (p) : WL B : x W
L

L (p)(x) = [[p]]x .

def

(128)

, p P V L (p) (18) (19).

7.2.
13. A F m x W [[A]](x) = [[A]]
x L

(129)

. A. A = p PV (129) (128).




253

A=aB (23), (126) (68) [[a]](x) = a WL (x) = a 1 = a = [[a]]
x

A = B C, A = B C, A = B C , x W
L

[[B ]](x) = [[B ]]x ,

[[C ]](x) = [[C ]]x .

10, L- x [[B ]]x [[C ]]x = [[B C ]]x . , [[A]](x) = [[B C ]](x) = [[B ]](x) [[C ]](x) = = [[B ]]x [[C ]]x = [[B C ]]x = [[A]]x . A = B C A = B C . A = 2a B , y W , [[2a B ]](x) [[2a B ]]x . (132) (130), (126), (27) , (131) a (133) inf ((RL )a (x, y ) [[B ]]y ) .
y W
L

def

L

[[B ]](y ) = [[B ]]y .

(130) (131)

(132) = (133) , Ç (132) (133), Ç (132) (133).


254 (132) [[2a B ]]

. .

(133) (120)
x y W

inf ((RL )a (x, y ) [[B ]]y )
L

(134)

(134) , y WL (RL )a (x, y ) [[2a B ]]x [[B ]]
y

(135)

(135) (127). (132) (133). y WL , , a (RL )a (x, y ) [[B ]] [[2a B ]]
x

(136)

y

u , [[2a A]]x A (137) [[2a B ]]x 0 ([[2a B ]]x 0) (B 0) 1. u L-. . , Ç (31) u, Ç b B (32) (33). , (138) (31). (31) : Ç a1 A1 = (138) (138)




255

Ç i = 2, . . . , n ai = (32) B0 A2 b ... An [[2a Ai ]]x [[2a B ]]x 0 (139)

L

(140)

(140)

b0 [[2a A2 ]]x ... [[2a An ]]x

B0 A2 0) L (b 0) ( ... An A2 B) L (b 0) ( . . . An 2a A2 (b 0) ( . . . 2a B ) L 2a An [[2a A2 ]]x b0 ... [[2a B ]]x [[2a An ]]x







[[2a B ]]x .

(141)


256

. .

(141) [[2a B ]]x 0 [[2a A2 ]]x ... [[2a An ]]x

b.

(142)

(142) (33) . , (138) (31). B0 A1 A1 ... ... An An , (32) B0 A1 b ... An

L

(143)

(144) (33) . . y L- u. u y , [[2a B ]]x 0 [[B 0]]y = [[B ]]y 0

, [[2a B ]]x 0 [[2a A1 ]]x b. (144) ... [[2a An ]]x

(145)




257

A F m [[2a A]]x [[2a B ]]x 0 (145) [[B ]]
y

[[A]]y .

(146)

[[2a B ]]x .

(147)

(146) , A F m [[2a B ]]x 0 [[2a A]]x [[A]]
y

(148)

(148) (127) a [[2a B ]]x 0 (RL )a (x, y ). (149)

c = [[2a B ]]x . (150). a c0 a 0, (151) c c0 c0 a a c0 0,

(136) a a c c0
def

(147), (149), c (150)

(152)

, , . .

c


258

. .

8. F K
14. A F m : A FK (153) A . . (153) (154) (154)

3.4. , A F K , A F K . 2. {([[A]]
FK

0) (A 0)}

(155)

F K -. . , b B (A 0) b [[A]]
FK

FK

(156) (157)

0

b

(156) (b 0) A b0 [[A]]
FK

FK
FK



[[A]] 0

b.

, (155) F K -. . 7, F K - (155) , [[A 0]]x (158) x WF K : [[A]]F K 0




259

x F K -, 9 (158) , [[A 0]]x = [[A]]x [[0]]x = [[A]]x 0 (129), (158) (159) [[A]]
FK

(159)

0

[[A]](x) 0

(160)

[[A]](x) [[A]]
FK

(161)

, A x. A x, (28) (126) [[A]](x) = 1 (162)

(161) (162) [[A]] F K = 1, A F K , , A F K . .


[1] Goldblatt R. Top oi. The categorial analysis of logic // Studies in Logic and the Foundation of Mathematics. Vol. 98. Amsterdam, New York, Oxford: North-Holland Publishing Company, 1979. [2] Clarke E. M., Grumb erg O., Peled D. Mo del Checking. MIT Press, 1999. [3] BendovÄ K., HÄ a ajek P. Possibilistic logic as a tense logic // Proceedings of QUARDET'93. Barcelona, 1993. [4] Boutilier C. Mo dal logics for qualitative p ossibility and b eliefs // Uncertainty in Artificial Intelligence VI I I / D. Dub ois et al., eds. Morgan Kaufmann, 1992. 17-24. [5] Dub ois D., Lang J., Prade H. Possibilistic logic // Handb o ok of Logic in Artificial Intelligence and Logic Programming. Vol. 3: Nonmonotonic Reasoning and Uncertain Reasoning / D. M. Gabbay, C. J. Hogger, J. A. Robinson, eds. Oxford U. P., 1994. 439-513.


260

. .

[6] Farinas del Cerro L., Herzig A. A mo dal analysis of p ossibility theory // Symb olic and Qualitative Approaches to Uncertainty. Lecture Notes in Comput. Sci. 548 / R. Kruse, P. Siegel, eds. Springer-Verlag, 1991. 58-62. [7] Fitting M. Many-valued mo dal logics // Fund. Inform. 15. 1992. 235-254. [8] Fitting M. Many-valued mo dal logics I I // Fund. Inform. 17. 1992. 55-73. [9] Go do L., Lop ez de Mantaras R. Fuzzy logic // Encyclopaedia of Computer Science. 1993. [10] HÄ ajek P. On logics of approximate reasoning // Neural Network Word. 6. 1993. 733-744. [11] HÄ ajek P., HarmancovÄ D. A comparative fuzzy mo dal logic // a Fuzzy Logic in Artificial Intelligence / E. P. Klement, W. Slany, eds. Springer-Verlag, 1993. 27-34. [12] HÄ ajek P., HarmancovÄ D., Esteva F., Garcia P., Go do L. On mo dal a logics for qualitative p ossibility in a fuzzy setting // Uncertainty in Artificial Intelligence: Pro ceedings of the Tenth Conference / R. Lop ez de Mantaras, D. Po ole, eds. Seattle, WA, 1994. [13] HÄ ajek P., HarmancovÄ D., Verbrugge R. A qualitative fuzzy p ossia bilistic logic // International Journal of Approximate Reasoning. 12. North-Holland, 1995. 1-19. [14] Ostermann P. Many-valued mo dal prop ositional calculi // Z. Math. Logik Grundlag. Math. 34. 1988. 343-354.