Документ взят из кэша поисковой машины. Адрес оригинального документа : http://www.intsys.msu.ru/staff/mironov/fuzzy.pdf Дата изменения: Thu Jan 10 23:01:57 2008 Дата индексирования: Mon Oct 1 21:09:08 2012 Кодировка: Поисковые слова: m 101

mODALXNYE LOGIKI DLQ PREDSTAWLENIQ NE^ETKIH UTWERVDENIJ
a m mIRONOW
. .

aNNOTACIQ
w STATXE WWEDEN I IZU^EN KLASS LOGI^ESKIH IS^ISLENIJ DLQ PREDSTAWLENIQ UTWERVDENIJ, W KOTORYH MOGUT PRISUTSTWOWATX MODALXNYE OPERATORY, WYRAVA@]IE MERU ISTINNOSTI SOSTAWNYH ^ASTEJ \TIH UTWERVDENIJ. wWEDENNYE IS^ISLENIQ QWLQ@TSQ OBOB]ENIQMI PROPOZICIONALXNYH MODALXNYH LOGIK. |TI IS^ISLENIQ NAZYWA@TSQ NE^ETKIMI MODALXNYMI LOGIKAMI. wWEDENO PONQTIE NE^ETKOJ MODELI kRIPKE I OPISANA SEMANTIKA NE^ETKIH MODALXNYH LOGIK W KLASSE NE^ETKIH MODELEJ kRIPKE. dOKAZANA TEOREMA O POLNOTE MINIMALXNOJ NE^ETKOJ MODALXNOJ LOGIKI W KLASSE NE^ETKIH MODELEJ kRIPKE.

1

aPPARAT MODALXNOJ LOGIKI I OSNOWANNYE NA NEM METODY RASSUVDENIJ IROKOISPOLXZU@TSQ W RAZLI^NYH ZADA^AH, OTNOSQ]IHSQ K INTELLEKTUALXNYM SISTEMAM, W ^ASTNOSTI, W ZADA^AH PREDSTAWLENIQ ZNANIJ I PROWEDENIQ RASSUVDENIJ O DINAMI^ESKIH SISTEMAH, BAZAH DANNYH, IT.D. w NASTOQ]EJ STATXE MY WWODIM PROPOZICIONALXNYJ MODALXNYJ FORMALIZM, KOTORYJ POZWOLQET WYRAVATX UTWERVDENIQ S MODALXNOSTQMI, INDEKSIROWANNYMI \LEMENTAMI NEKOTOROJPOLNOJALGEBRY gEJTINGA. w\TOMFORMALIZME KAVDOE UTWERVDENIE A MOVET BYTX DOPOLNENOMODALXNYM OPERATOROM WIDA 2a, KOTORYJ MOVET BYTX INTERPRETIROWAN, NAPRIMER, KAK MERA PRAWDOPODOBIQ UTWERVDENIQ A, ILI MERA UWERENNOSTI W ISTINNOSTI A, ILI WEROQTNOSTX ISTINNOSTI UTWERVDENIQ A, ILI KAK-LIBO E]E. |TOT FORMALIZM MOVET SLUVITX OSNOWOJ DLQ RASSUVDENIQH OB OB_EKTAH, INFORMACIQ O KOTORYH NEPOLNA, NEDOSTOWERNA, I PROTIWORE^IWA. kROME TOGO,
1

wWEDENIE


NA OSNOWE PREDLAGAEMOGOPODHODA MOVNO RASSMATRIWATX ZADA^I WERIFIKACII MODELEJ DISKRETNYH DINAMI^ESKIH SISTEM, KOTORYE QWLQ@TSQ NEPOLNYMI APPROKSIMACIQMI ANALIZIRUEMYH SISTEM. mATEMATI^ESKIE PODHODY K PREDSTAWLENI@ ZNANIJ, W KOTORYH PRISUTSTWUET NE^ETKOSTX I NEPOLNOTA, BYLI RASSMOTRENY WO MNOGIH RABOTAH, SM. NAPRIMER 3]{33]. bOLX INSTWO IZ NIH SWQZANO S KOLI^ESTWENNOJ OCENKOJ NEOPREDELENNOSTI. oDNAKOW RQDE SLU^AEW MERU NEOPREDELENNOSTI OBRABATYWAEMOJINFORMACII BOLEE RAZUMNO OCENIWATX NE KOLI^ESTWENNYMI, A KA^ESTWENNYMI PARAMETRAMI. dANNAQSITUACIQ IMEET MESTO, NAPRIMER, WSLEDU@]IH SLU^AQH. 1. oBRABATYWAEMAQ INFORMACIQ MOVET BYTX NEPOLNOJ, NEQSNOJ, PRIBLIZITELXNOJI NEPROWERENNOJ. pOLNOCENNU@ OBRABOTKUTAKOJINFORMACII MOVNOPROIZWODITX TOLXKO W RAMKAH TAKOJFORMALXNOJSISTEMY, WKOTOROJKAVDOMU UTWERVDENI@ MOVET BYTX SOPOSTAWLEN NEKOTORYJ PARAMETR, WYRAVA@]IJ KA^ESTWENNU@ OCENKUNADEVNOSTI DANNOGO UTWERVDENIQ. 2. eSLI MY ISSLEDUEM SLOVNU@ SISTEMU, TAKU@, ^TOEEDETALXNOE I TO^NOE PREDSTAWLENIE NEWOZMOVNO, TO MY STROIM GRUBU@ MODELX \TOJSISTEMY, KOTORAQ IMEET NEBOLX U@ SLOVNOSTX, I WMESTO ISSLEDOWANIQ SISTEMY MY ISSLEDUEM \TU GRUBU@ MODELX. nO, POSKOLXKUISHODNAQSISTEMA I EEMODELX SU]ESTWENNO RAZLI^NY, TO IH SWOJSTWA MOGUT OTLI^ATXSQ. tAKIM OBRAZOM, DLQ KORREKTNOGO ISSLEDOWANIQ SISTEMY NA OSNOWE TAKOJ MODELI NEOBHODIMOIMETX METODOCENIWANIQ RAZLI^IQ MEVDU SWOJSTWAMI TAKOJMODELI I SWOJSTWAMI ISHODNOJ SISTEMY. mERY RAZLI^IQ MEVDU SWOJSTWAMI MOGUT BYTX NETOLXKOKOLI^ESTWENNYMI, NOTAKVEI KA^ESTWENNYMI. nAPRIMER, MNOVESTWO TAKIH MER MOVET PREDSTAWLQTX SOBOJBULEWU ALGEBRU WSEHPODMNOVESTW NEKOTOROGOMNOVESTWA SITUACIJ (T.E. SOSTOQNIJ OKRUVA@]EJ SREDY, WKOTOROJ RABOTAET ANALIZIRUEMAQSISTEMA). mERA \KWIWALENTNOSTI MEVDU SISTEMOJ I EE MODELX@ (OTNOSITELXNO PROWERQEMYH SWOJSTW) MOVET BYTX OPREDELENA, NAPRIMER, KAK MNOVESTWO TEH SITUACIJ, W KOTOROJ \TI SWOJSTWA \KWIWALENTNY DLQ ISHODNOJ SISTEMY I DLQ EEMODELI. mERA NALI^IQ NEKOTOROGO PROWERQEMOGO SWOJSTWA MOVET BYTX OPREDELENA KAK PODMNOVESTWO \TOGOMNOVESTWA, KOTOROE SOSTOIT IZ SITUACIJ, WKOTORYH \TOSWOJSTWO IMEET MESTO.
2


|TOMNOVESTWO SITUACIJ MOVET BYTX DOPOLNENO KOLI^ESTWENNYMI PARAMETRAMI KAVDOJ SITUACII, WYRAVA@]IMI IH ZNA^IMOSTX, WEROQTNOSTX, IT.P. w^ASTNOSTI, ESLI MNOVESTWA PARAMETROW SITUACIQ QWLQ@TSQ LINEJNO UPORQDO^ENNYMI MNOVESTWAMI, TOMNOVESTWO MER WYPOLNIMOSTI SWOJSTW PREDSTAWLQET SOBOJNEKOTORU@ ALGEBRU gEJTINGA. gLAWNYJ REZULXTAT NASTOQ]EJ RABOTY ZAKL@^AETSQ W POSTROENII FORMALXNOGO APPARATA, KOTORYJ MOVET RASSMATRIWATXSQ KAK LOGI^ESKAQOSNOWA DLQ PREDSTAWLENIQ NE^ETKOJINFORMACII TAKOGO TIPA. wWEDENNYJ FORMALIZM MOVET TAKVE ISPOLXZOWATXSQ DLQ RAZRABOTKI QZYKOWSPECIFIKACII DINAMI^ESKIH SISTEM S NEPOLNOJINFORMACIEJ OB IH STRUKTURE I POWEDENII, KOTORYE ANALOGI^NY QZYKAM SPECIFIKACII, OSNOWANNYM NA TEMPORALXNOJLOGIKEIPREDNAZNA^ENNYM DLQ OPISANIQ SWOJSTW PROGRAMMNYH SISTEM I APPARATNYH USTROJSTW (2]). sTATXQ ORGANIZOWANA SLEDU@]IM OBRAZOM. w PARAGRAFE 2 MY OPISYWAEM SINTAKSIS NE^ETKIH MODALXNYH LOGIK (nml) IOPREDELQEM MINIMALXNU@ nml FK . w PARAGRAFE 3 MY WWODIM PONQTIE NE^ETKOJMODELI kRIPKE (nmk) IOPREDELQEM SEMANTIKUFORMUL nml W KLASSE nmk. mY TAKVE RASSMATRIWAEM PRIMER nmk, SWQZANNYJ S DESKRIPTIWNYMI LOGIKAMI. w PARAGRAFE 4 MY WWODIM PONQTIE KANONI^ESKOJ MODELI nml, KOTOROE ISPOLXZUETSQ W PARAGRAFE 5 DLQ DOKAZATELXSTWA POLNOTY MINIMALXNOJnml FK W KLASSE WSEH nmk. w ZAKL@^ENII MY REZ@MIRUEM REZULXTATY RABOTY I PREDLAGAEM NEKOTORYE PROBLEMY DLQ DALXNEJ IH ISSLEDOWANIJ W DANNOJ OBLASTI.

2
2.1

nE^ETKIE MODALXNYE LOGIKI
pOLNYE ALGEBRY gEJTINGA

mY BUDEM PREDPOLAGATX, ^TOMNOVESTWO MER NE^ETKOSTI, KOTORYE MOGUT WHODITX W FORMULY NE^ETKIH MODALXNYH LOGIK, PREDSTAWLQET SOBOJPOLNU@ ALGEBRU gEJTINGA. wNASTOQ]EM PUNKTEMYNAPOMNIM OPREDELENIE \TOGOPONQTIQ. pOLNOJ RE ETKOJ NAZYWAETSQ ^ASTI^NO UPORQDO^ENNOE MNOVESTWO H, TAKOE, ^TO DLQ KAVDOGO PODMNOVESTWA Q H SU]ESTWU@T \LEMENTY inf (Q) I sup(Q) MNOVESTWA H, TAKIE, ^TO DLQ KAVDOGO b 2 H (8q 2 Q b q) , b inf (Q) (8q 2 Q q b) , sup(Q) b: |LEMENTY inf (H) I sup(H) OBOZNA^A@TSQ TAKVE SIMWOLAMI 0 I 1 SOOTWETSTWENNO.
3


dLQ KAVDOGOKONE^NOGOPODMNOVESTWA Q = fa1 ::: ang H \LEMENTY inf (Q) I sup(Q) BUDUT OBOZNA^ATXSQ ZNAKOSO^ETANIQMI a1 ^ ::: ^ an I a1 _ ::: _ an SOOTWETSTWENNO. |TI \LEMENTY BUDUT TAKVE OBOZNA^ATXSQ ZNAKOSO^ETANIQMI 89 23 > a1 > <= 6 a1 7 ::: > ::: > I 4 a 5 : an n SOOTWETSTWENNO. pOLNAQALGEBRA gEJTINGA { \TOPOLNAQRE ETKA H, NA KOTOROJZADANA BINARNAQOPERACIQ TAKAQ, ^TO DLQ KAVDOJTROJKI a b c 2 H IMEET MESTOSOOTNO ENIE a^b c , a b!c (1) nIVE SIMWOL H OBOZNA^AET NEKOTORU@ FIKSIROWANNU@ POLNU@ ALGEBRU gEJTINGA. ( dLQ KAVDOJ PARY a b 2 H ZNAKOSO^ETANIE a $ b OBOZNA^AET \LEMENT ) a!b . b!a oDNIMIZNAIBOLEE WAVNYH PRIMEROWPOLNOJALGEBRY gEJTINGA QWLQETSQ MNOVESTWO n{\LEMENTNYH KORTEVEJ f(a1 ::: an ) j a1 2 M1 ::: an 2 Mn g GDE M1 ::: Mn { POLNYE LINEJNOUPORQDO^ENNYE MNOVESTWA (NAPRIMER, KAVDOE Mi QWLQETSQ OTREZKOM 0 1]), I SOOTNO ENIE (a1 ::: an) (b1 ::: bn) IMEET MESTO, ESLI I TOLXKO ESLI DLQ KAVDOGO i = 1 ::: n WYPOLNENO NERAWENSTWO ai bi dLQ KAVDOJ PARY a =(a1 ::: an) b =(b1 ::: bn) GDE ci = 1i ESLIOaiIWNbiM SLU^AE b WPR T O
4
!: H H!H

(

a

!

b def (c1 ::: cn) =


pUSTX PV { NEKOTOROE S^ETNOE MNOVESTWO, \LEMENTY KOTOROGOMY BUDEM NAZYWATX PROPOZICIONALXNYMI PEREMENNYMI. mNOVESTWO FORMUL NE^ETKIH MODALXNYH LOGIK (NAZYWAEMYH NIVE PROSTO FORMULAMI) OPREDELQETSQ INDUKTIWNOSLEDU@]IM OBRAZOM. kAVDAQPEREMENNAQ p 2 PV { FORMULA. kAVDYJ \LEMENT a 2 H { FORMULA. eSLI A I B { FORMULY, TO ZNAKOSO^ETANIQ A ^ B , A _ B , I A ! B { TOVEFORMULY. eSLI A { FORMULA, I a 2 H, TO 2aA { FORMULA. sIMWOLY 2a NAZYWA@TSQ NE^ETKIMI MODALXNYMI OPERATORAMI. fORMULU 2aA MOVNO INTERPRETIROWATX KAK UTWERVDENIE \MERA PRAWDOPODOBIQ UTWERVDENIQ A RAWNA a". dLQ KAVDOGO SPISKA FORMUL A1 ::: An ZNAKOSO^ETANIQ A1 ^ A2 ^ ::: ^ An I A1 _ A2 _ ::: _ An QWLQ@TSQ SOKRA]ENNOJ ZAPISX@ FORMULY A1 ^ (A2 ^ (::: ^ An) :::) I A1 _ (A2 _ (::: _ An) :::) SOOTWETSTWENNO. |TI FORMULY TAKVEBUDUT OBOZNA^ATXSQ ZNAKOSO^ETANIQMI 89 23 > A1 > <= 6 A1 7 ::: > ::: > I 4 A 5 : An n SOOTWETSTWENNO. dLQ KAVDOJ PARY FORMUL A B ZNAKOSO^ETANIE A$B ( ) A!B : QWLQETSQ SOKRA]ENNOJ ZAPISX@ FORMULY B ! A

2.2

fORMULY NE^ETKIH MODALXNYH LOGIK

5


2.3

pODSTANOWKA { \TOPARA
= ((p1 ::: pn ) (A1 ::: An)) (2)

pODSTANOWKI

GDE
p1 ::: pn { RAZLI^NYE PEREMENNYE, I A1 ::: An { FORMULY. dLQ KAVDOJ PODSTANOWKI (2) I KAVDOJ FORMULY A ZNAKOSO^ETANIE (A) OBOZNA^AET FORMULU, POLU^AEMU@ IZ A ZAMENOJ DLQ KAVDOGO i = 1 ::: n KAVDOGOWHOVDENIQ PEREMENNOJ pi W A NA SOOTWETSTWU@]U@ FORMULU Ai.
2.4

pUSTX A I B { FORMULY. mY BUDEM GOWORITX, ^TO B POLU^AETSQ IZ A \KWIWALENTNYM PREOBRAZOWANIEM, ESLI A SODERVIT PODFORMULU ODNOGOIZ SLEDU@]IH WIDOW: a ^ b a _ b ILI a ! b GDE a b 2 H, I B POLU^AETSQ IZ A ZAMENOJ \TOJ PODFORMULY NA \LEMENT ALGEBRY H, KOTORYJ QWLQETSQ REZULXTATOMPRIMENENIQ SOOTWETSTWU@]EJ OPERACII KPARE a b. fORMULY A I B NAZYWA@TSQ \KWIWALENTNYMI, ESLI ODNA IZ NIH MOVET BYTX POLU^ENA IZ DRUGOJ PRI POMO]I NESKOLXKIH \KWIWALENTNYH PREOBRAZOWANIJ. eSLI A I B \KWIWALENTNY, TOMYBUDEM OBOZNA^ATX \TOT FAKT ZNAKOSO^ETANIEM A B . pUSTX A { FORMULA BEZ MODALXNYH OPERATOROW, I SPISOKPEREMENNYH, WHODQ]IH W A IMEET WID (p1 ::: pn ): A NAZYWAETSQ TAWTOLOGNEJ, ESLI (A) 1 DLQ KAVDOJ PODSTANOWKI (2), TAKOJ, ^TO 8i 2 f1 ::: ng Ai = ai 2 H

tAWTOLOGII

6


2.5

nE^ETKAQ MODALXNAQ LOGIKA (nml) { \TO PODMNOVESTWO L MNOVESTWA
WSEHFORMUL, UDOWLETWORQ@]EE SLEDU@]IM USLOWIQM. kAVDAQTAWTOLOGIQ PRINADLEVIT L. dLQ KAVDOJ PARY A B FORMUL I KAVDOGO a 2 H () ( ) A $ 2aA 2a B 2L 2aB
2a1 dLQ KAVDOJFORMULY A I KAVDOGO a 2aA ! a
a
!

nE^ETKIE MODALXNYE LOGIKI

(3) (4) (5)

dLQ KAVDOGO a

2H

2

L L
!

2H 2

dLQ KAVDOJ PARY FORMUL A B ESLI A 2 L I A TO B 2 L

B

2

L

(6)

dLQ KAVDOJFORMULY A I KAVDOJPODSTANOWKI ESLI A 2 L TO (A) 2 L dLQ KAVDOJ PARY FORMUL A B I KAVDOJ PARY a b ESLI a ! (A ! B ) 2 L TO a ! (2bA ! 2bB ) 2 L
2H

(7)

(8)
2 =g H

dLQ KAVDOJFORMULY A I KAVDOGOPODMNOVESTWA fai j i ESLI 8i 2 = ai ! A 2 L TO (sup ai) ! A 2 L:
i2=

(9)

iZ \TOGOOPREDELENIQ SLEDUET, ^TO SU]ESTWUET MINIMALXNAQ (OTNOSITELXNOPONQTIQ WKL@^ENIQ MNOVESTW) nml, KOTORU@ MY BUDEM OBOZNA^ATX SIMWOLOM FK .
7


nETRUDNODOKAZATX, ^TO PRAWILO WYWODA ESLI a1 ! A1 2 L ::: an ! An 2 L ! GDE a1 ::: an 2 H I A1 ::: An {FORMULY 898 9 >>> > < a1 = < A1 = TO > ::: > ! > ::: > 2 L : an : An QWLQETSQ DOPUSTIMYM DLQ KAVDOJnml. dLQ KAVDOJFORMULY A IKAVDOJnml L ZNAKOSO^ETANIE A] L OBOZNA^AET TO^NU@ WERHN@@ GRANX MNOVESTWA fa 2 H j a ! A 2 Lg: iZ \TOGOOPREDELENIQ I (9) SLEDUET, ^TO 8a 2 H a ! A 2 L , a A ] L:

(10)

(11)

3
3.1

nE^ETKIE MODELI kRIPKE
gEJTINGOZNA^NYE MNOVESTWA

nAPOMNIM (1]), ^TO GEJTINGOZNA^NYM MNOVESTWOM (gm) NAD POLNOJ ALGEBROJ gEJTINGA H NAZYWAETSQ PARA W =(X ) (12) GDE X { NEKOTOROE MNOVESTWO (KOTOROE NAZYWAETSQ NOSITELEM gm W ), I { OTOBRAVENIE WIDA :X X !H TAKOE, ^TO (x y)= (y x) (13) 8x y 2 X ) ( (x y) (x z) (14) 8x y z 2 X (y z)
8


dLQ KAVDOJ PARY x y 2 X \LEMENT (x y) NAZYWAETSQ MEROJ BLIZOSTI xy. nAPRIMER, PUSTX X { MNOVESTWO WSEH L@DEJ, fa1 ::: an g { PERE^ENX NEKOTORYHIHHARAKTERISTIK (TAKIH, NAPRIMER, KAK WOZRAST, POL, ZARPLATA, REPUTACIQ, ZDOROWXE, IT.D.), M1 ::: Mn { POLNYE LINEJNOUPORQDO^ENNYE MNOVESTWA OCENOKSHOVESTI, KAVDOE IZ KOTORYH OTNOSITSQ K SOOTWETSTWU@]EJ HARAKTERISTIKE, ALGEBRA gEJTINGA H IMEET WID M1 ::: Mn (15) mY MOVEM RASSMATRIWATX X KAK gm NAD (15), GDE DLQ KAVDOJPARY x y 2 X MEROJ IH BLIZOSTI (x y) QWLQETSQ n{\LEMENTNYJ KORTEV c1 ::: cn, TAKOJ, ^TO DLQ KAVDOGO i 2 f1 :::ng ESLI x I y PRIMERNOODINAKOWY OTNOSITELXNO HARAKTERISTIKI ai, TO\LEMENT ci BLIZOKKMAKSIMALXNOMU \LEMENTU MNOVESTWA Mi. dLQ KAVDOGO x 2 X \LEMENT (x x) NAZYWAETSQ MEROJ PRINADLEVNOSTI \LEMENTA x GEJTINGOZNA^NOMU MNOVESTWU (12). gEJTINGOZNA^NOE OTNO ENIE (go) NA gm (12) { \TO OTOBRAVENIE R WIDA R:X X!H TAKOE, ^TO 8 9 > R(x y) > < = 8 x y x0 y 0 2 X (x x0) > R(x0 y0) (16) > (y y 0 ) : ( ) (x x) : 8x y 2 X R(x y) (17) (y y) dLQ KAVDOJ PARY (x y) 2 X X \LEMENT R(x y) MOVNO INTERPRETIROWATX KAK MERU PRNNADLEVNOSTI \TOJ PARY go R. gEJTINGOZNA^NOE PODMNOVESTWO (gp) Wgm (12) { \TOOTOBRAVENIE s WIDA (18) s:X !H TAKOE, ^TO ( ) s(x) 02X 8x x s(x0) (19) (x x0) 8x 2 X s(x) (x x): (20) dLQ KAVDOGO x 2 X \LEMENT s(x) MOVNO INTERPRETIROWATX KAK MERU PRINADLEVNOSTI \LEMENTA x PODMNOVESTWU (18). mNOVESTWO WSEHgp W gm (12) BUDET OBOZNA^ATXSQ SIMWOLOM Sub(W ). nIVE
9


DLQ KAVDOGOgm W EGONOSITELX BUDET OBOZNA^ATXSQ TEM VE SIMWOLOM W, DLQ KAVDOJ PARY x y \LEMENTOWNOSITELQ MERA BLIZOSTI MEVDU x I y BUDET OBOZNA^ATXSQ ZNAKOSO^ETANIEM W (x y), I DLQ KAVDOGO x 2 W MERA PRINADLEVNOSTI \LEMENTA x GEJTINGOZNA^NOMU MNOVESTWU W BUDET OBOZNA^ATXSQ ZNAKOSO^ETANIEM W (x).
3.2

nE^ETKAQMODELX kRIPKE (nmk) { \TOTROJKA M WIDA
M =(W fRa j a
2 Hg

oPREDELENIE NE^ETKOJMODELI kRIPKE
) (21)

GDE

1. W { gm, \LEMENTY KOTOROGO NAZYWA@TSQ TO^KAMI (ILI MIRAMI), 2. fRa j a 2 Hg { H{INDEKSIROWANNOE SEMEJSTWO GEJTINGOZNA^NYH OTNOENIJ NA W , KOTORYE NAZYWA@TSQ NE^ETKIMI OTNO ENIQMI DOSTIVIMOSTI, 3. { OTOBRAVENIE WIDA : PV ! Sub(W ) (22) KOTOROE NAZYWAETSQ OCENKOJPEREMENNYH.

3.3

w \TOM PUNKTE MY PRIWODIM PRIMER nmk, OTNOSQ]IJSQ K DESKRIPTIWNOJ LOGIKE (34]{36]). dESKRIPTIWNAQ LOGIKA { \TO LOGI^ESKIJ APPARAT, PREDNAZNA^ENNYJ DLQ FORMALXNOGOOPISANIQ SLOVNYH PONQTIJ S ISPOLXZOWANIEM ATOMARNYH PONQTIJ, I BINARNYH OTNO ENIJ, NAZYWAEMYH ATOMARNYMI ROLQMI. pREDPOLOVIM, ^TO ZADANY MNOVESTWO I INDIWIDUALOW, MNOVESTWO C ATOMARYH PONQTIJ, PRI^EM KAVDOMU ATOMARNOMU PONQTI@ c 2 C SOOTWETSTWUET NEKOTOROE PODMNOVESTWO c] I , KOTOROE SOSTOIT IZ WSEH INDIWIDUALOW, PREDSTAWLQ@]IH PONQTIE c,
10

pRIMER nmk


MNOVESTWO R ATOMARNYH ROLEJ, PRI^EM KAVDOJATOMARNOJ ROLI r 2 R SOOTWETSTWUET NEKOTOROE BINARNOE OTNO ENIE r] I I . sOOTNO ENIE (a b) 2 r] INTERPRETIRUETSQ KAK UTWERVDENIE O TOM, ^TO a WYSTUPAET W ROLI r POOTNO ENI@ K b. dESKRIPTIWNAQ LOGIKA POZWOLQET WYRAVATX SLOVNYE PONQTIQ PRI POMO]I PONQTIJNYH TERMOW, KOTORYE PREDSTAWLQ@T SOBOJ WYRAVENIQ, POSTROENNYE IZ ATOMARNYH PONQTIJ I ATOMARNYH ROLEJ S ISPOLXZOWANIEM SLEDU@]IH PONQTIJNYH KONSTRUKTOROW: BULEWSKIE OPERACII (KONX@NKCIQ (^), IT.D.), I KWANTORNYH OPERACIJ WIDA 8r, GDE r 2 R. kAVDOMU PONQTIJNOMU TERMU SOOTWETSTWUET PODMNOVESTWO t] I KOTOROE SOSTOIT IZ WSEH INDIWIDUALOW, PREDSTAWLQ@]IH \TOPONQTIE, IOPREDELQETSQ INDUKTIWNOSLEDU@]IM OBRAZOM: t1 ^ t2] def t1] \ t2]], = ( ) DLQ KAVDOGO b 2 I . def 8r:t] = a 2 I (a b) 2 r] ) b 2 t] rASSMOTRIM SLEDU@]IJ PRIMER (KOTORYJ ZAIMSTWOWAN IZ 37]). pUSTX I PREDSTAWLQET SOBOJMNOVESTWO L@DEJ, ATOMARNOE PONQTIE Woman INTERPRETIRUETSQ KAK MNOVESTWO WSEH VEN]IN, I ATOMARNAQROLX child INTERPRETIRUETSQ KAK MNOVESTWO WSEH PAR L@DEJ (a b), TAKIH, ^TO b QWLQETSQ DITEM a. tOGDA PONQTIE WSEH VEN]IN, KOTORYE IME@T TOLXKO DO^EREJ, MOVET BYTX PREDSTAWLENOPONQTIJNYM TERMOM Woman ^ 8child:Woman oBOZNA^IM SIMWOLOM R MNOVESTWO WSEHKONE^NYH POSLEDOWATELXNOSTEJ \LEMENTOWMNOVESTWA R. kAVDAQPOSLEDOWATELXNOSTX r =(r1 ::: rn ) 2 R SOOTWETSTWUET BINARNOMU OTNO ENI@ r] def r1] ::: rn] = II
11


|LEMENTY MNOVESTWA R MOVNO INTERPRETIROWATX KAK PROIZWODNYE ROLI, MY BUDEM NAZYWATX IH PROSTO ROLI. pUSTX H ESTX MNOVESTWO P (R ) WSEHPODMNOVESTW MNOVESTWA R . H QWLQETSQ POLNOJ ALGEBROJ gEJTINGA, TAK KAK ONOQWLQETSQ POLNOJ BULEWOJALGEBROJ. mY MOVEM RASSMATRIWATX MNOVESTWO I L@DEJ KAK GEJTINGOZNA^NOE MNOVESTWO NAD H = P (R ), GDEDLQ KAVDOJ PARY (x y) 2 I I MERA BLIZOSTI I (x y ) SOSTOIT IZ WSEH ROLEJ r 2 R TAKIH, ^TO x I y SOWPADA@T W ROLI r (MY NEUTO^NQEM PONQTIE SOWPADENIQ L@DEJ W NEKOTOROJ ROLI, T.K. ONO INTUITIWNOQSNO, NOFORMALXNOE OPREDELENIE DANNOGOPONQTIQ TREBUET SERXEZNOGO LINGWISTI^ESKOGO OBOSNOWANIQ). nmk, SWQZANNAQ S \TIM PRIMEROM, IMEET SLEDU@]IE KOMPONENTY. 1. oB_EKTAMI \TOJ nmk QWLQ@TSQ L@DI, MERA BLIZOSTI MEVDU NIMI BYLA OPISANA WY E. 2. dLQ KAVDOGO 2 H I KAVDOJ PARY x y L@DEJ MNOVESTWO R (x y) SOSTOIT IZ WSEH ROLEJ r 2 , TAKIH, ^TO (x y) 2 r]]. 3. mNOVESTWO PV PROPOZICIONALXNYH PEREMENNYH RAWNO MNOVESTWU C ATOMARNYH PONQTIJ, I DLQ KAVDOGO c 2 C OCENKA (c): I ! P (R ) OPREDELQETSQ SLEDU@]IM OBRAZOM: DLQ KAVDOGO^ELOWEKA x 2 I ( def (c)(x) = I (x) ESLI x 2 c]M SLU^AE: W PROTIWNO dLQ KAVDOJ FORMULY A I KAVDOJ nmk (21) OCENKA A A M PREDSTAWLQET SOBOJOTOBRAVENIE A] M : W ! H KOTOROE OTOBRAVAET KAVDU@ TO^KU x 2 W W\LEMENT A] x 2 H NAZYWAEMYJ MEROJ ISTINNOSTI FORMULY A WTO^KE x I OPREDELQEMYJ SLEDU@]IM OBRAZOM: ESLI A = p 2 PV , TO A] x def (p)(x) = (23)
12
3.4

oCENKA FORMULW nmk


ESLI A = a

2 H,

TO

A] x =

def

(

a W (x)
x^ x_

)

(24) (25) (26)

ESLI A = B ^ C , TO ESLI A = B _ C , TO ESLI A = B
!

A] x def B ] = A] x def B ] = A] x =
def

C] x C] x
x

C , TO

(

B] x ! C ] W (x)

)

(27)

ESLI A = 2aB , TO

8 >a < def A] x = > yinf (Ra(x y) 2 : WWx) (

!

9 > = B ] y) : >

(28)

nETRUDNODOKAZATX, ^TO A] M QWLQETSQ GEJTINGOZNA^NYM PODMNOVESTWOMgm W.
3.5

fORMULA A NAZYWAETSQ ISTINNOJW TO^KE x nmk (21), ESLI A] x = W (x): (29) fORMULA A NAZYWAETSQ ISTINNOJ W nmk (21), ESLI A ISTINNA W KAVDOJ TO^KE (21). nETRUDNODOKAZATX, ^TO KAVDAQFORMULA A 2 FK ISTINNA W KAVDOJnmk, T.K. KAVDAQTAWTOLOGIQ ISTINNA W KAVDOJ nmk, FORMULY W (3), (4) I (5) ISTINNY W KAVDOJnmk, I PRAWILA WYWODA (6), (7), (8) I (9) SOHRANQ@T SWOJSTWO FORMUL BYTX ISTINNYMI W KAVDOJ nmk. nIVEMY DOKAVEM OBRATNOE UTWERVDENIE: ESLI FORMULA A ISTINNA W KAVDOJ nmk, TO A 2 FK .
13

iSTINNOSTX FORMULW nmk


4
4.1

kANONI^ESKIE MODELI nml
nEPROTIWORE^IWYE nml

nml L NAZYWAETSQ NEPROTIWORE^IWOJ, ESLI 8a 2 H a 2 L ) a =1: (30) dOKAVEM, ^TO FK NEPROTIWORE^IWA. kAK BYLO SKAZANO W PUNKTE 3.5, DLQ KAVDOGO a 2 H IZ UTWERVDEIIQ a 2 FK SLEDUET, ^TO FORMULA a ISTINNA W KAVDOJnmk, W ^ASTNOSTI, W nmk WIDA (21), GDE W SOSTOIT IZ ODNOGO\LEMENTA x, I W (x)= 1: (31) (30) SLEDUET IZ (24), (29) I (31). nIVEKAVDAQ RASSMATRIWAEMAQ nml PREDPOLAGAETSQ NEPROTIWORE^IWOJ. pUSTX L { NEKOTORAQNEPROTIWORE^IWAQnml, I u { NEKOTOROE MNOVESTWO FORMUL. mNOVESTWO u NAZYWAETSQ L{SOWMESTIMYM, ESLI DLQ KAVDOGOKONE^NOGOPODMNOVESTWA MNOVESTWA u, IME@]EGOWID fa1 ! A1 ::: an ! An g (GDE a1 ::: an 2 H A1 ::: An { FORMULY) I KAVDOGO b 2 H IZ SOOTNO ENIQ 89 > A1 > <= > ::: > ! b 2 L : An SLEDUET NERAWENSTWO 89 > a1 > <= > ::: > b: : an
14
4.2

L{SOWMESTIMYE

MNOVESTWA FORMUL

(32)

(33) (34)


4.3

dLQ KAVDOJ PARY u1 u2 MNOVESTW FORMULNERAWENSTWO u1 u2 (35) OZNA^AET, ^TO DLQ KAVDOJFORMULY WIDA a ! A 2 u1 a =0 ILI 9 b a : b ! A 2 u2: tEOREMA 1. dLQ KAVDOJ PARY u1 u2 MNOVESTW FORMUL IZ NERAWENSTWA (35) SLEDUET IMPLIKACIQ u2 { L{SOWMESTIMO ) u1 { L{SOWMESTIMO

sWOJSTWA L{SOWMESTIMYH MNOVESTW

eSLI MY PRIMENIM PRAWILO (10) K MY POLU^IM SOOTNO ENIE 898 > a1 > > <=< > ::: > ! > :a :
n

tEOREMA 2. kAVDAQNEPROTIWORE^IWAQ nml QWLQETSQ L{SOWMESTIMYM MNOVESTWOM. dOKAZATELXSTWO.
9 A1 > = ::: > 2 L: An OOTNO ENIE 9 a1 > = ::: > ! b 2 L a
n

PODMNOVESTWU (32) MNOVESTWA L, TO
(36)

iZ (33), (36) I (6) SLEDUET S 8 > < > : iZ (37) I (30) SLEDUET (34).

(37)

nIVE SIMWOL L OBOZNA^AET NEKOTORU@ FIKSIROWANNU@ NEPROTIWORE^IWU@ nml.

tEOREMA 3

pUSTX u { L{SOWMESTIMOE MNOVESTWO, A { FORMULA, I
15

.


Q { MNOVESTWO WSEH\LEMENTOW a 2 H, TAKIH, ^TO u fa ! Ag { L{SOWMESTIMO.

(38)

tOGDA DLQ KAVDOGO a

2H

zAMETIM, ^TO Q 6= , TAK KAK 0 2 Q. iMPLIKACIQ a 2 Q ) a sup(Q) O^EWIDNA. iMPLIKACIQ a sup(Q) ) a 2 Q \KWIWALENTNA SLEDU@]EJ PARE UTWERVDENIJ: 1. MNOVESTWO u fsup(Q) ! Ag (39) L{SOWMESTIMO 2. ESLI MNOVESTWO u fa ! Ag L{SOWMESTIMO, TO DLQ KAVDOGO a0 a MNOVESTWO u fa0 ! Ag TOVE L{SOWMESTIMO. uTWERVDENIE 2 SLEDUET IZ TEOREMY 1. dOKAVEM UTWERVDENIE 1: DLQ KAVDOGOPODMNOVESTWA (32) MNOVESTWA (39), I KAVDOGO b 2 H (33) WLE^ET (34). tAK KAK u QWLQETSQ L{SOWMESTIMYM PO PREDPOLOVENI@, TO DLQ DOKAZATELXSTWA IMPLIKACII

dOKAZATELXSTWO.

a sup(Q)

,

a 2 Q:

(33) ) (34) DOSTATO^NO RASSMOTRETX SLU^AJ, KOGDA MNOVESTWO (32) IMEET SLEDU@]IJ WID: (a1 ! A1) = (sup(Q) ! A) 8 i =2 ::: n (ai ! Ai ) 2 u. 16


w\TOM SLU^AE (34) IMEET WID ) ( sup(Q) b a2 ^ ::: ^ an (40) \KWIWALENTNO SOOTNO ENI@ ( ) a 8a2Q b a2 ^ ::: ^ an (41) SLEDUET IZ (38).

(40)

(41)

|LEMENT sup(Q), KOTORYJ ODNOZNA^NO OPREDELQETSQ PO A I u, NIVEBUDET OBOZNA^ATXSQ ZNAKOSO^ETANIEM A] u (42) iZ OPREDELENIQ \LEMENTA A] u SLEDUET, ^TO DLQ KAVDOGOMNOVESTWA u FORMULIMEET MESTO IMPLIKACIQ: u L{SOWMESTIMO ) 8 A 2 Fm (43) u f A] u ! Ag L{SOWMESTIMO tEOREMA 4. pUSTX u1 I u2 { L{SOWMESTIMYE MNOVESTWA, TAKIE, ^TO u1 u2: tOGDA DLQ KAVDOJFORMULY A A] u A] u : (44) dOKAZATELXSTWO. tAK KAK MNOVESTWO u2 f A] u ! Ag L{SOWMESTIMO, I u1 f A] u ! Ag u2 f A] u ! Ag TOIZTEOREMY 1 SLEDUET, ^TOMNOVESTWO u1 f A] u ! Ag (45) L{SOWMESTIMO. (44) SLEDUET IZ
2 1 2 2 2 2

17


L{SOWMESTIMOSTI (45), I IZ OPREDELENIQ \LEMENTA A] u1 tEOREMA 5. pUSTX u { L{SOWMESTIMOE MNOVESTWO FORMUL, I A B { PARA FORMUL, TAKIH, ^TO A!B 2L

(46) (47)

tOGDA

(47) \KWIWALENTNO L{SOWMESTIMOSTI MNOVESTWA u f A] u ! B g (48) T.E. UTWERVDENI@ O TOM, ^TODLQ KAVDOGOPODMNOVESTWA (32) MNOVESTWA (48), I KAVDOGO b 2 H IZ (33) SLEDUET (34). tAK KAK u PO PREDPOLOVENI@ L{SOWMESTIMO, TO DLQ DOKAZATELXSTWA IM-

dOKAZATELXSTWO.

A] u

B]

u

PLIKACII

(33) ) (34) DOSTATO^NO RASSMOTRETX SLU^AJ, KOGDA (32) IMEET SLEDU@]IJ WID: (a1 ! A1)=( A] u ! B ) DLQ KAVDOGO i =2 ::: n ai ! Ai 2 u

(49)

w\TOM SLU^AE (33) \KWIWALENTNOSOOTNO ENI@ 89 > A2 > <= B ! (> ::: > ! b) 2 L : An iZ (46) I (50) SLEDUET SOOTNO ENIE 89 > A2 > <= A ! (> ::: > ! b) 2 L : An
18

(50)

(51)


KOTOROE \KWIWALENTNOSOOTNO ENI@ 8A 9 >> >A > < 2= (52) > ::: > ! b 2 L : An tAK KAK MNOVESTWO u f A] u ! Ag L{SOWMESTIMO, TOIZ (49) I (52) SLEDUET NERAWENSTWO 8 A] 9 > u> >a > <2 = (53) > ::: > b > : an > KOTOROE \KWIWALENTNOSOOTNO ENI@ (34) DLQ RASSMATRIWAEMOGOSLU^AQ. dLQ KAVDOGO L{SOWMESTIMOGOMNOVESTWA u, I KAVDOJFORMULY A IMEET MESTONERAWENSTWO: A] L A] u

tEOREMA 6

.

dOKAZATELXSTWO

. (54) \KWIWALENTNO L{SOWMESTIMOSTI MNOVESTWA

(54) (55)

u

f

A]

L ! Ag

T.E. SLEDU@]EMU UTWERVDENI@: DLQ KAVDOGOPODMNOVESTWA (32) MNOVESTWA (55), I KAVDOGO b 2 H IZ (33) SLEDUET (34). tAK KAK u PO PREDPOLOVENI@ L{SOWMESTIMO, TO DLQ DOKAZATELXSTWA IMPLIKACII
(33) ) (34) DOSTATO^NO RASSMOTRETX SLU^AJ, KOGDA (32) IMEET SLEDU@]IJ WID: (a1 ! A1)=( A] L ! A) 19


DLQ KAVDOGO i =2 ::: n

a

i ! Ai

2

u

(56)

w\TOM SLU^AE (33) \KWIWALENTNO 8 > < A2 A ! (> ::: : An iZ SOOTNO ENIQ I (57) SLEDUET SOOTNO ENIE
A] L A] L

UTWERVDENI@ 9 > = > ! b) 2 L
A
2

(57)

!

L b) L
(58)

!

89 > A2 > <= (> ::: > : An

!

2

8 > A2 9 <> = ::: > ! ( A] L ! b) 2 L (59) >A :n tAK KAK u PO PREDPOLOVENI@ L{SOWMESTIMO, TO IZ (56) I (59) SLEDUET NERAWNSTWO 89 > a2 > <= (60) > ::: > A] L ! b : an iZ (60) SLEDUET (34).
4.4

iZ (58) SLEDUET, ^TO

pUSTX x { NEKOTOROE MNOVESTWO FORMUL. mNOVESTWO x NAZYWAETSQ L{POLNYM, ESLI xL{SOWMESTIMO, I DLQ KAVDOJFORMULY A A] x ! A 2 x:

L{POLNYE

MNOVESTWA FORMUL

(61)

20


pUSTX u { NEKOTOROE L{SOWMESTIMOE MNOVESTWO, I x { NEKOTOROE L{POLNOE MNOVESTWO. x NAZYWAETSQ POPOLNENIEM u, ESLI ux (62) tEOREMA 7. dLQ KAVDOGO L{SOWMESTIMOGOMNOVESTWA u SU]ESTWUET EGOPOPOLNENIE x. dOKAZATELXSTWO. nIVE IZLAGAETSQ DOKAZATELXSTWO DANNOJTEOREMY DLQ SLU^AQ, KOGDA MNOVESTWO FORMUL QWLQETSQ S^ETNYM. eSLI MNOVESTWO FORMUL NES^ETNO (^TO IMEET MESTOWTOM SLU^AE, KOGDA ALGEBRA gEJTINGA H NES^ETNA), DANNOE DOKAZATELXSTWO MODIFICIRUETSQ PUTEM WWEDENIQ OTNO ENIQ POLNOJ UPORQDO^ENNOSTI NA MNOVESTWE FORMUL I ISPOLXZOWANIQ TRANSFINITNOJINDUKCII. pUSTX POSLEDOWATELXNOSTX B1 B2 ::: (63) PREDSTAWLQET SOBOJSPISOK WSEHFORMUL. oPREDELIM POSLEDOWATELXNOSTX u1 u2 ::: MNOVESTW FORMULSLEDU@]IM OBRAZOM: u1 def u, = DLQ KAVDOGO k 1 uk+1 def uk f Bk] uk ! Bk g = iZ \TOGOOPREDELENIQ I IZ SOOTNO ENIQ (43) SLEDUET, ^TO DLQ KAVDOGO k 1 ESLI uk L{SOWMESTIMO, (64) TO uk+1 TOVE L{SOWMESTIMO. tAK KAK u1 POPREDPOLOVENI@ L{SOWMESTIMO, TOIZ (64) SLEDUET, ^TO 8k 1 uk L{SOWMESTIMO oPREDELIM MNOVESTWO x SLEDU@]IM OBRAZOM: x def uk =
k
1

4.5

pOPOLNENIE L{SOWMESTIMYH MNOVESTW

21


1. dOKAVEM, ^TO x QWLQETSQ L{POLNYM. (a) mNOVESTWO x QWLQETSQ L{SOWMESTIMYM, TAK KAK DLQ KAVDOGO EGO KONE^NOGOPODMNOVESTWA (32) SU]ESTWUET NOMER k 1, TAKOJ, ^TO (32) QWLQETSQ PODMNOVESTWOMMNOVESTWA uk (KOTOROE QWLQETSQ L{SOWMESTIMYM). (b) dOKAVEM, ^TO DLQ KAVDOJ FORMULY A WYPOLNQETSQ SOOTNO ENIE (61). pO OPREDELENI@ POSLEDOWATELXNOSTI (63), SU]ESTWUET NOMER k, TAKOJ, ^TO A = Bk .

tAK KAK

Bk] uk Bk] x: tAK KAK uk x, TOIZTEOREMY 4 SLEDUET, ^TO Bk ] x Bk ] uk : iZ (65) I (66) SLEDUET RAWENSTWO Bk] x = Bk] uk : sLEDOWATELXNO, Bk ] x ! Bk = Bk] uk ! Bk 2 uk+1 x: iZ (68) SLEDUET (61) (ESLI A = Bk ). tAKIM OBRAZOM, x QWLQETSQ L{POLNYM. 2. dOKAVEM, ^TO x QWLQETSQ POPOLNENIEM MNOVESTWA u, T.E. 8 (a ! A) 2 u a A] x:

TO

Bk]

uk ! Bk

2

x
(65) (66) (67) (68)

pO OPREDELENI@ MNOVESTWA x, 9k 1: A = Bk : tAK KAK TO
(a
!

Bk ) 2 u u

k

uk fa ! Bk g L{SOWMESTIMO. iZ (69) I (67) SLEDUET, ^TO a Bk] uk = Bk] x = Ax:
22

(69)


4.6

pUSTX x { L{POLNOE MNOVESTWO, I a 2 H. tOGDA a] x = a (70) dOKAZATELXSTWO. tAK KAK x L{SOWMESTIMO, TO KAVDOE EGO ODNO\LEMENTNOE PODMNOVESTWO f a] x ! ag OBLADAET SLEDU@]IM SWOJSTWOM: DLQ KAVDOGO b 2 H IZ SOOTNO ENIQ a!b 2L (71) SLEDUET NERAWENSTWO a] x b (72) tAK KAK (71) WERNO DLQ b = a, TO (72) TOVE WERNODLQ b = a, T.E. a] x a: (73) dLQ DOKAZATELXSTWA OBRATNOGONERAWENSTWA MY DOKAVEM L{SOWMESTIMOSTX MNOVESTWA x fa ! ag: (74) dLQ \TOGODOSTATO^NODOKAZATX, ^TODLQ KAVDOGOPODMNOVESTWA (32) MNOVESTWA (74), I KAVDOGO b 2 H IZ (33) SLEDUET (34). tAK KAK x PO PREDPOLOVENI@ L{SOWMESTIMO, TO DLQ DOKAZATELXSTWA IMPLIKACII

tEOREMA 8

sWOJSTWA L{POLNYH MNOVESTW FORMUL
.

(33) ) (34) DOSTATO^NO RASSMOTRETX SLU^AJ, KOGDA (32) UDOWLETWORQET SLEDU@]IM USLOWIQM: (a1 ! A1)=(a ! a) 8i =2 ::: n ai ! Ai 2 x (75)

w\TOM SLU^AE (33) \KWIWALENTNO SOOTNO ENI@ 8 >a > < A2 > ::: > : An I

9 > > = > >

!

b

2

L

(76)

23


(34) \KWIWALENTNONERAWENSTWU

8a 9 >> >a > < 2= > ::: > b >> : an

(77)

89 > A2 > <= > ::: > ! (a ! b) 2 L : An iZ (78) IIZ L{SOWMESTIMOSTI x SLEDUET NERAWENSTWO 89 > a2 > <= > ::: > a ! b : an
(77) SLEDUET IZ (79).

(76) \KWIWALENTNO SOOTNO ENI@

(78)

(79)

nIVE MY BUDEM PREDPOLAGATX, ^TO H UDOWLETWORQET DOPOLNITELXNOMU USLOWI@: 8 a 2 H (a ! 0) ! 0 = a: (80) oTMETIM, ^TO \TO USLOWIE \KWIWALENTNO TOMU, ^TO H QWLQETSQ BULEWOJ ALGEBROJOTNOSITELXNO OPERACIJ ^ _ :, GDE 8a 2 H :a def a ! 0: = pUSTX x { L{POLNOE MNOVESTWO, I A I B { FORMULY. tOGDA A ! B ] x = A] x ! B ] x dOKAZATELXSTWO. dLQ DOKAZATELXSTWA (81) DOSTATO^NO DOKAZATX, ^TO A ! B ] x A] x ! B ] x I A] x ! B ] x A ! B ] x
24

tEOREMA 9

.

(81) (82) (83)


dOKAVEM (82). dANNOE NERAWENSTWO \KWIWALENTNONERAWENSTWU ) ( A ! B] x B] x (84) A] x (84) \KWIWALENTNO L{SOWMESTIMOSTI MNOVESTWA ( ) A ! B] x ! Bg x f A] (85) x T.E. UTWERVDENI@ O TOM, ^TODLQ KAVDOGOPODMNOVESTWA (32) MNOVESTWA (85), I KAVDOGO b 2 H IZ (33) SLEDUET (34). tAK KAK x PO PREDPOLOVENI@ L{SOWMESTIMO, TO DLQ DOKAZATELXSTWA IMPLIKACII
(33) ) (34) DOSTATO^NO RASSMOTRETX SLU^AJ, KOGDA (32) IMEET SLEDU@]IJ WID: ( ) A ! B] x ! B a1 ! A1 = A] x DLQ KAVDOGO i =2 ::: n ai ! Ai 2 x

(86)

w\TOM SLU^AE (33) \KWIWALENTNO UTWERVDENI@ 8 > A2 < B ! (> ::: : An I
(34) \KWIWALENTNONERAWENSTWU

9 > = >

!

b)

2

L

(87)

8 > > > < > > > :

(

a2 ::: an

A ! B] A] x

x

)9 > > > = >b > >

(88)

25


tAK KAK FORMULA QWLQETSQ TAWTOLOGIEJ, TO
(87) IIZ (89) SLEDUET, ^TO

( (

A A
!

)
!

B

!

B
2

A A

)
B

!

B

L

(89)

(

A A

)
B
!

!

89 > A2 > <= (> ::: > : An

!

b)

2

L

(90)

(90) \KWIWALENTNO UTWERVDENI@

9 > A > > A!B = A2 >!b 2L > ::: > An tAK KAK x POPREDPOLOVENI@ L{POLNOE, TO
A]
x!

8 > > > < > > > :

(91)

A

2

x

(92)

I

A ! B ] x ! (A ! B ) 2 x (93) iZ (91), (92), (93), (86), ATAKVEIZ L{SOWMESTIMOSTI x WYTEKAET (88). tEPERX DOKAVEM NERAWENSTWO (83). dANNOE NERAWENSTWO \KWIWALENTNO L{SOWMESTIMOSTI MNOVESTWA x
f

( A]

x!

B ] x)

!

(A

!

B )g

(94)

T.E. UTWERVDENI@ O TOM, ^TODLQ KAVDOGOPODMNOVESTWA (32) MNOVESTWA (94), I KAVDOGO b 2 H IZ (33) SLEDUET (34). tAK KAK x PO PREDPOLOVENI@ L{SOWMESTIMO, TO DLQ DOKAZATELXSTWA IMPLIKACII
(33) ) (34) DOSTATO^NO RASSMOTRETX SLU^AJ, KOGDA (32) IMEET SLEDU@]IJ WID: 26


a1 ! A1 = ( A] x ! B ] x) ! (A ! DLQ KAVDOGO i =2 ::: n ai ! Ai w\TOM SLU^AE (33) \KWIWALENTNO UTWERVDENI@ 8 > A2 < (A ! B ) ! (> ::: : An I (34) \KWIWALENTNONERAWENSTWU 8 A] ! B >x >a <2 > ::: > : an

B)
2

x

(95)

9 > = >

!

b)

2

L

(96)

]x 9 > >

= >b >

(97)

dLQ DOKAZATELXSTWA NERAWENSTWA (97) DOSTATO^NODOKAZATX \KWIWALENTNOE NERAWENSTWO 8 b!0 9 > > ) >a < 2 > ( A] x = (98) > ::: > B] x ! 0 > : an > dLQ DOKAZATELXSTWA (98) DOSTATO^NO DOKAZATX, ^TO 8 b!0 9 > > >a <2 > = (99) > ::: > A] x > > : an I 8 b!0 9 > > >a <2 > = (100) > ::: > B ] x ! 0 > : an > dOKAVEM NERAWENSTWO (99). dANNOE NERAWENSTWO \KWIWALENTNO L{SOWMESTIMOSTI MNOVESTWA 8 b!0 9 > > >a <2 > = x f> ::: > ! Ag (101) > : an > T.E. UTWERVDENI@ O TOM, ^TODLQ
27


KAVDOGOKONE^NOGOPODMNOVESTWA (101) WIDA fc1 ! C1 ::: cm ! Cm g TAKOGO, ^TO 8 b!0 9 > >a > <2 > = c1 ! C1 = > ::: > ! A > : an > 8i =2 ::: m ci ! Ci 2 x (102) I KAVDOGO d 2 H IZ SOOTNO ENIQ 8A 9 >> >C > < 2= (103) > ::: > ! d 2 L >> : Cm SLEDUET NERAWENSTWO 88 9 > > b!0 9 > >> >> = > < a2 > > >> > > ::: > > <: = >> an (104) >c >d >2 > > > > ::: > > > >c > :m dLQ DOKAZATELXSTWA NERAWENSTWA (104) DOSTATO^NO DOKAZATX \KWIWALENTNOE NERAWENSTWO ( ) a2 ^ ::: ^ an (b ! 0) ! d (105) c2 ^ ::: ^ cm iZ (103) SLEDUET, ^TO 89 > C2 > <= A ! (> ::: > ! d) 2 L (106) : Cm iZ (106) SLEDUET, ^TO 89 > C2 > <= ((> ::: > : Cm
d) B)
28 (A

!

!

!

!

B)

2

L

(107)


iZ (107) I (96) 8 > < ((> :

SLEDUET, ^TO 9 C2 > = ::: > ! d) ! B ) C
m

!

89 > A2 > <= (> ::: > : An

!

b)

2

L

(108)

8 99 89 > C2 > > < => > C2 > = <= > ::: > > ! ((> ::: > ! d) ! B ) : Cm : Cm > d!B QWLQETSQ TAWTOLOGIEJ, TO\TA FORMULA PRINADLEVIT L. iZ \TOGO UTWERVDENIQ IIZ (108) SLEDUET, ^TO 8 9 > d!B > < = A2 ^ ::: ^ An > ! b 2 L (109) > C ^ ::: ^ C :2 m iZ (109), (95), (102), IIZ L{SOWMESTIMOSTI MNOVESTWA x SLEDUET NERAWENSTWO 8 9 > d ! B] x > < = a2 ^ ::: ^ an > b > c ^ ::: ^ c :2 m KOTOROE \KWIWALENTNONERAWENSTWU ( ) a2 ^ ::: ^ an d ! B] x ! b (110) c2 ^ ::: ^ cm dOKAVEM, ^TO d ! B ] x ! b (b ! 0) ! d (111) (111) \KWIWALENTNONERAWENSTWU ) ( d ! B] x ! b d (112) b!0 tAK KAK ( ) d ! B] x ! b d ! B] x ! 0 b!0 TO DLQ DOKAZATELXSTWA SOOTNO ENIQ (112) DOSTATO^NO DOKAZATX NERAWENSTWO d ! B] x ! 0 d (113) (113) \KWIWALENTNONERAWENSTWU d ! 0 d ! B] x (114)
29

tAK KAK FORMULA 8 > > < > > :


dOKAVEM (114). tAK KAK FORMULA (d ! 0) ! (d ! B ) QWLQETSQ TAWTOLOGIEJ, TO (d ! 0) ! (d ! B ) 2 L (115) (115) IIZ TEOREMY 5 SLEDUET NERAWENSTWO d ! 0]]x d ! B ] x (116) iZ (116) IIZ TEOREMY 8 SLEDUET (114). iZ (114) SLEDUET (111). iZ (110) I (111) SLEDUET (105). tAKIM OBRAZOM, L{SOWMESTIMOSTX MNOVESTWA (101) DOKAZANA, I, SLEDOWATELXNO, DOKAZANO (99). dOKAVEM NERAWENSTWO (100). dANNOE NERAWENSTWO \KWIWALENTNO NERAWENSTWU 8 B] 9 > x> < a2 = (117) > ::: > b > : an > (117) IMEET MESTO, T.K. 1. IZ (96) IIZ SOOTNO ENIQ B ! (A ! B ) 2 L SLEDUET SOOTNO ENIE 89 > A2 > <= B ! (> ::: > ! b) 2 L : An KOTOROE \KWIWALENTNO SOOTNO ENI@ 89 >B > >A > < 2= > ::: > ! b 2 L >> : An
2. f( B ] x ! B ) (a2 3. xL{SOWMESTIMO. tEOREMA 10.
!

A2) ::: (an

!

An)

g

x, I

pUSTX

30


x { L{POLNOE MNOVESTWO, I A B { NEKOTORYE FORMULY. tOGDA A ^ B ] x = A] x

dOKAZATELXSTWO.
(118) SLEDUET IZ

^

B]

x

(118)

A ^ B]

x

A]
x^

x

A ^ B]

x x

B]

x

(119) (120)

I
(119) SLEDUET IZ

A]

B] x
! !

A ^ B] A B
2 2

IIZ TEOREMY 5. (120) SLEDUET IZ L{SOWMESTIMOSTI MNOVESTWA x f( A] x ^ B ] x) ! (A ^ B ) tEOREMA 11. pUSTX x { L{POLNOE MNOVESTWO, I A B { NEKOTORYE FORMULY. tOGDA A _ B ] x = A] x _ B ] x dOKAZATELXSTWO. (121) \KWIWALENTNONERAWENSTWU
(122) SLEDUET IZ ( A]
x_

(A ^ B ) (A ^ B )

L L

g

(121)

B ] x)

!

0= A _ B ]

x!

0 = = =

(122)

) A] x ! 0 ( A] x _ B ] x) ! 0 = B] x ! 0 ( ) ( ) A] x ! 0]]x = A ! 0]]x = B ] x ! 0]]x B ! 0]]x ( ) A!0 ] = = (A _ B ) ! 0]]x B!0 x = A _ B ] x ! 0]]x = A _ B ] x ! 0
31

(


pUSTX x { L{POLNOE MNOVESTWO. tOGDA DLQ KAVDOJFORMULY A IKAVDOGO a 2 H 2aA] x a: dOKAZATELXSTWO. iZ (5) SLEDUET (a ! 0) ! (2aA ! 0) 2 L iZ (124), IIZ TEOREM 5 I 8 SLEDUET a!0 2aA ! 0]]x iZ TEOREM 9 I 8 SLEDUET 2aA ! 0]]x = 2aA] x ! 0]]x = 2aA] x iZ (125) I (126) SLEDUET a!0 2aA] x ! 0 (127) \KWIWALENTNO SOOTNO ENI@ (123).
4.7

tEOREMA 12.

(123) (124) (125)
!

0

(126) (127)

kANONI^ESKAQMODELX nml L { \TOnmk

kANONI^ESKAQMODELX nml

ML def (WL fRLa j a 2 Hg L) = KOMPONENTY KOTOROJOPREDELQ@TSQ SLEDU@]IM OBRAZOM. 1. WL SOSTOIT IZ WSEH L{POLNYH MNOVESTW. dLQ KAVDOJ PARY x y 2 WL WL(x y) def Ainf ( A] x $ A] y) = 2Fm

(128) (129)

zAMETIM, ^TOIZ\TOGOOPREDELENIQ SLEDUET, ^TO 8x 2 WL WL(x)=1:
2H

2. dLQ KAVDOGO a

RLa { go NA WL RLa : WL W
8
def

L!H

GDE

x y 2 WL RLa(x y) = Ainf ( 2aA] x 2Fm
32

!

A] y)

(130)


3.

L

{ \TOOTOBRAVENIE WIDA
L

: PV
L

!

Sub(WL)
!H

GDE DLQ KAVDOGO p 2 PV gp
(p): WL OPREDELQETSQ SLEDU@]IM OBRAZOM:
8x 2

W

L

L

(p)(x) def p] x: =

(131)

nESLOVNODOKAZATX, ^TO 1. WL UDOWLETWORQET USLOWIQM (13) I (14), 2. RLa UDOWLETWORQET USLOWIQM (16) I (17), I 3. L(p) UDOWLETWORQET USLOWIQM (19) I (20).
4.8

tEOREMA 13

oSNOWNOE SWOJSTWO KANONI^ESKOJMODELI
. (132)

dLQ KAVDOJFORMULY A IKAVDOGO x 2 WL A]](x)= A] x dOKAZATELXSTWO. iNDUKCIQ PO STRUKTURE FORMULY A. A = p 2 PV w\TOM SLU^AE (132) SLEDUET IZ (131). A=a2H iZ (24), (129) I (70) SLEDUET, ^TO ( )() a a]](x)= W (x) = a = a = a] 1 L

x

A=B^C A=B_C pO INDUKTIWNOMU 8x 2 iZ TEOREMY 10 IZ

A=B !C PREDPOLOVENI@, WL B ]](x)= B ] x C ]](x)= C ] x: L{POLNOTY x SLEDUET, ^TO B] x ^ C ] x = B ^ C ] x
33


A]](x)= B ^ C ]](x) def = def = B ]](x) ^ C ]](x)= B ] x ^ C ] x = = B ^ C ] x = A] x: sLU^AI A = B _ C I A = B ! C RAZBIRA@TSQ ANALOGI^NO. A = 2aB pO INDUKTIWNOMU PREDPOLOVENI@, B ]](y)= B ] y: 8y 2 WL

pO\TOMU

(133) (134) (135) (136) (137) (138)

dOKAVEM, ^TO\LEMENT SOWPADAET S \LEMENTOM

2aB ]](x)

2aB ] x: iZ (133), (129), I (28) SLEDUET, ^TO (134) SOWPADAET S 8 9
rAWENSTWO (135) = (136) SLEDUET
(135) (136)

I
(137) SLEDUET IZ (123) IIZ 2a B ] x

(135) (136)
y2WL

inf (RLa(x y)

!

B ] y)

(139)

^TO

) a 2aB ] x RLa(x y) ! B ] y pUSTX SIMWOL u OBOZNA^AET MNOVESTWO, KOTOROE SOSTOIT IZ
34

(139) SLEDUET IZ SLEDU@]EGO UTWERVDENIQ: DLQ KAVDOGO y 2 WL ( ) RLa(x y) B] y (140) 2aB ] x (140) SLEDUET IZ (130). dLQ DOKAZATELXSTWA (138) DOSTATO^NOPOSTROITX \LEMENT y 2 WL, TAKOJ,

(

(141)


WSEHFORMUL WIDA I FORMULY

(

2aA] x 2aB ] x
x!

)
!

0

!

A
0)

(142)

( 2aB ]

0)

!

(B

!

(143)

lEMMA.

mNOVESTWO uL{SOWMESTIMO. dOKAZATELXSTWO. dOKAVEM, ^TODLQ KAVDOGOKONE^NOGOPODMNOVESTWA (32) KAVDOGO b 2 H IZ (33) SLEDUET (34). sNA^ALA RASSMOTRIM SLU^AJ (143) 2 (32): pUSTX (32) IMEET WID a1 ! A1 = (143) DLQ KAVDOGO i =2 ::: n ( ai = 2aAi]] x ! 2aB x w\TOM SLU^AE (33) IMEET WID 8 B!0 9 > >A > <2 > = > ::: > ! b 2 > : An >

MNOVESTWA u, I

)
0

(144)

L

(145)

35


8 B !0 9 > >A > <2 > = (b ! 0) ! (> ::: > ! 0) 2 L > : An > 89 > A2 > <= (b ! 0) ! (> ::: > ! B ) 2 L : An 8 > 2aA2 9 > < = (b ! 0) ! (> ::: > ! 2aB ) 2 L : 2aAn 8 > 2aA2] x 9 > < = ! 2aB ] x b ! 0 > ::: : 2aAn] x > pOSLEDNEE NERAWENSTWO \KWIWALENTNOSOOTNO ENI@ 8 b!0 9 > > 2A] > < a 2x> = > ::: > 2aB ] x: > : 2aAn] x >

iZ (145) SLEDUET

)

)

)

(146)

8 2 B] ! 0 9 > ax > > 2A] < a 2x > = > ::: > b: > : 2aAn] x > (147) \KWIWALENTNO (34) W RASSMATRIWAEMOM SLU^AE. tEPERX RASSMOTRIM SLU^AJ, KOGDA (143) 62 (32). tAK KAK FORMULA 8 9 > B ! 0 > 8 A1 9 >A <1 > > > =< = > ::: > ! > ::: > > > : An :A

iZ (146) SLEDUET

(147)

QWLQETSQ TAWTOLOGIEJ, TOIZ (33) SLEDUET 8 B!0 9 > >A > <1 > = > ::: > ! b 2 L > : An >
36

n

(148)


IZ (148) SLEDUET 2aB ] x ! 0 9 > = 2aA1] x > b: > ::: > 2aAn] x (149) \KWIWALENTNO (34) W RASSMATRIWAEMOM SLU^AE. oBOZNA^IM SIMWOLOM y L{POPOLNENIE u. iZ OPREDELENIQ u I y SLEDUET, ^TO 2aB ] x ! 0 B ! 0]]y = B ] y ! 0 I DLQ KAVDOJFORMULY A ( ) 2aA] x A] y: 2aB ] x ! 0 iZ (150) SLEDUET NERAWENSTWO B ] y 2aB ] x: iZ (151) SLEDUET, ^TO DLQ KAVDOJFORMULY A 2aB ] x ! 0 2aA] x ! A] y iZ (153) I (130) SLEDUET, ^TO ( ) a RLa(x y): 2a B ] x ! 0 (141) SLEDUET IZ (152), (154), IIZ 8a 9 >( > < = ) a > c!0 !c > c : GDE c def 2aB ] x. = dOKAVEM NERAWENSTWO (155). dANNOE NERAWENSTWO \KWIWALENTNOS ENI@ 8a 9 >( > < = ) a c!0 > : c!0 !c >!0 T.E. NERAWENSTWU 8 c!0 9 > > a > > : c!0 !c > KOTOROE, O^EWIDNO, WERNO.
37

kAK BYLO SKAZANOWY E, 8 > > < > > :

(149)

(150) (151) (152) (153) (154)

(155)

OOTNO(156)

(157)


5

pUSTX H UDOWLETWORQET USLOWI@ (80). tOGDA, ESLI FORMULA A ISTINNA W KAVDOJnmk NAD H, TO A 2 FK . dOKAZATELXSTWO. pREDPOLOVIM, ^TO A 62 FK . dOKAVEM, ^TO A NE QWLQETSQ ISTINNOJ W NEKOTOROJTO^KE KANONI^ESKOJMODELI LOGIKI FK . zAMETIM, ^TOMNOVESTWO (158) f( A] FK ! 0) ! (A ! 0)g QWLQETSQ FK {SOWMESTIMYM, T.K. DLQ KAVDOGO b 2 H IZ SOOTNO ENIQ (A ! 0) ! b 2 FK (159) SLEDUET NERAWENSTWO A] FK ! 0 b (160) dEJSTWITELXNO, IZ (159) SLEDUET, ^TO (b ! 0) ! A 2 FK ) b!0 A] FK ) (160) iZ TEOREMY 7 IIZ FK {SOWMESTIMOSTI MNOVESTWA (158) SLEDUET, ^TO 9x 2 WFK : A] FK ! 0 A ! 0]]x (161) tAK KAK MNOVESTWO x QWLQETSQ FK {POLNYM, TOIZTEOREMY 9 I SOOTNO ENIQ (161) SLEDUET, ^TO A ! 0]]x = A] x ! 0]]x = A] x ! 0 (162) iZ (132), (161) I (162) SLEDUET NERAWENSTWO A]](x) ! 0 (163) A] FK ! 0 KOTOROE \KWIWALENTNONERAWENSTWU A]](x) A] FK (164) dOKAVEM, ^TOFORMULA A NE QWLQETSQ ISTINNOJW x. eSLI FORMULA A ISTINNA W x, TOIZ (29) I (129) SLEDUET, ^TO A]](x)= 1 (165) iZ (164) I (165) SLEDUET RAWENSTWO A] FK = 1, OTKUDA SLEDUET, ^TO A 2 FK . |TO PROTIWORE^IT PREDPOLOVENI@ O TOM, ^TO A 62 FK .
38

tEOREMA 14

pOLNOTA LOGIKI
.

FK


6

wNASTOQ]EJ RABOTE MY WWELI NOWYJ FORMALXNYJ APPARAT DLQ PREDSTAWLENIQ UTWERVDENIJ, W KOTORYH MOGUT PRISUTSTWOWATX NE^ETKIE MODALXNOSTI. mY OPREDELILI PONQTIE NE^ETKOJ MODALXNOJ LOGIKI I DOKAZALI TEOREMU O POLNOTE DLQ MINIMALXNOJNE^ETKOJMODALXNOJLOGIKI. nAPRAWLENIQ DALXNEJ IH ISSLEDOWANIJ, OTNOSQ]IHSQ K WWEDENNYM PONQTIQM I REZULXTATAM, MOGUT BYTX, NAPRIMER, SLEDU]IMI. 1. dOKAZATX TEOREMU O POLNOTE BEZ PREDPOLOVENIQ O TOM, ^TO DLQ KAVDOGO a 2 H IMEET MESTO UTWERVDENIE (a ! 0) ! 0= a. 2. iSSLEDOWATX PROBLEMY FINITNOJ APPROKSIMIRUEMOSTI I RAZRE IMOSTI MINIMALXNOJ nml I DRUGIH nml, PREDSTAWLQ@]IH PRAKTI^ESKIJ INTERES. 3. pOSTROITX NE^ETKIE ANALOGI IZWESTNYH PROPOZICIONALXNYH MODALXNYH LOGIK (K4, S4, IT.D.), ISSLEDOWATX IH POLNOTU, RAZRE IMOSTX, FINITNU@ APPROKSIMIRUEMOSTX. 4. oPREDELITX PONQTIQ NE^ETKOGO DOKAZATELXSTWA DLQ PERWOPORQDKOWYH LOGIK, WWESTI NE^ETKIE LOGIKI DOKAZUMOSTI, SWQZANNYE S PONQTIEM NE^ETKOGO DOKAZATELXSTWA I IZU^ITX IH SWOJSTWA (RAZRE IMOSTX I T.P.). 5. rAZRABOTATX QZYK NE^ETKIH SPECIFIKACIJ PROGRAMMYH SISTEM I ALGORITMY WERIFIKACII (model checking) DLQ NE^ETKIH SISTEM PEREHODOW.

zAKL@^ENIE

lITERATURA

1] Goldblatt R.: Topoi. The categorial analysis of logic, Studies in Logic and the Foundation of Mathematics, volume 98, North-Holland Publishing Company, Amsterdam, New York, Oxford, (1979). 2] Clarke, E.M., Grumberg, O., and Peled, D.: Model Checking, MIT Press, 1999. 3] K. Bendova, P.Hajek: Possibilistic logic as a tense logic, Proceedings of QUARDET'93, Barcelona, 1993. 4] C. Boutilier: Modal logics for qualitative possibility and beliefs, Uncertainty in Arti cial Intelligence VIII (D. Dubois et al., Eds.), Morgan Kaufmann, 17{24, 1992. 5] D. Dubois, J. Lang, H. Prade: Possibilistic logic, in: Handbook of Logic in Arti cial Intelligence and Logic Programming, vol. 3: Nonmonotonic 39


6]

7] 8] 9] 10] 11] 12]

13] 14] 15] 16]

Reasoning and Uncertain Reasoning (D. M. Gabbay, C. J. Hogger, and J. A. Robinson, Eds.), Oxford U. P., 439{513, 1994. L. Farinas del Cerro, A. Herzig: A modal analysis of possibility theory, in: Symbolic and Qualitative Approaches to Uncertainty, Lecture Notes in Comput. Sci. 548 (R. Kruse and P. Siegel, Eds.), Springer{Verlag, 58{62, 1991. M. Fitting: Many{valued modal logics, Fund. Inform. 15, 235{254, 1992. M. Fitting: Many{valued modal logics II, Fund. Inform. 17, 55{73, 1992. L. Godo, R. Lopez de Mantaras: Fuzzy logic, in: Encyclopaedia of Computer Science, 1993. P. Hajek: On logics of approximate reasoning, Neural Network Word 6, 733{744, 1993. P. Hajek, D. Harmancova: A comparative fuzzy modal logic, in: Fuzzy Logic in Arti cial Intelligence (E. P. Klement and W. Slany, Eds.), Springer{ Verlag 27{34, 1993. P.Hajek, D. Harmancova, F. Esteva, P. Garcia, L. Godo: On modal logics for qualitative possibility in a fuzzy setting, in: Uncertainty in Arti cial Intelligence: Proceedings of the Tenth Conference (R. Lopez de Mantaras and D. Poole, Eds.), Seattle, WA, 1994. P. Hajek, D. Harmancova, R. Verbrugge: A qualitative fuzzy possibilistic logic, International Journal of Approximate Reasoning, North{ Holland, 1995 12:1-19. P. Ostermann: Many{valued modal propositional calculi, Z. Math. Logik Grundlag. Math. 34, 343{354, 1988. Z. Zhang, Y. Sui, C. Cao, G. Wu: A formal fuzzy reasoning system and reasoning mechanism based on propositional modal logic. Theoretical Computer Science 368 (2006) 149-160. F. Bou, F. Esteva, L. Godo, R. Rodriguez: On many-valued modal logics over nite residuated lattices. In: Proc. of EUSFLAT conference (2007),
http://www.eusflat2007.cz

17] M. S. Ying: On standard models of fuzzy modal logics. Fuzzy Sets and Systems, 26 (1988) 357-363. 40


18] P. Chatalic, C. Froidevaux: Lattice-based graded logic: a multimodal approach. In Proceedings of the eighth conference on Uncertainty in Arti cial Intelligence, pages 33-40, San Francisco, CA, USA, 1992, Morgan Kaufmann Publishers Inc. 19] A. Ciabattoni, G. Metcalfe, F. Montagna: Adding modalities to MTL and its extensions. Proc. of the Linz Symposium 2005. 20] X. Caicedo, R. Rodriguez:A Godel similarity-based modal logic. Proc. of Logic, Computability and Randomness 2004. Cordoba, Argentina, 2007 21] F. Esteva, P. Garcia, L. Godo, R. Rodriguez: A modal account of similarity-based reasoning. International Journal of Approximate Reasoning, 16 (3-4): 235-260, 1997. 22] S. Frankowski: De nable classes of many valued Kripke frames. Bulletin of the Section of Logic, 35 (1): 27-36, 2006. 23] S. Frankowski: General approach to manyvalued Kripke models. Bulletin of the Section of Logic, 35 (1): 11-26, 2006. 24] P. Hajek: Metamathematics of fuzzy logic. Volume 4 of Trends in Logic Studia Logica Library.Kluwer Academic Publishers, Dordrecht, 1998. 25] P. Hajek, D. Harmancova: A many-valued modal logic. In Proceedings IPMU'96. Information Processing and Management of Uncertainty in Knowledge-Based Systems, pages 1021-1024, Granada, 1996. Universidad de Granada, The IEEE Computer Society Press. 26] G. Hansoul, B. Teheux: Completeness results for many-valued Lukasiewicz modal systems and relational semantics, 2006.
http://arxiv.org/abs/math/0612542

27] C. D. Koutras, C. Nomikos: The computational complexisy of satisfability in many-valued modal logic. In Proceedings of the 3rd Panhellenic Logic Symposium, Anogia, Greece, July 2001. 28] C. D. Koutras, C. Nomikos, P. Peppas: Canonicity and completeness results for many-valued modal logics. Journal of Applied Non-Classical Logics, 12 (1): 7-41, 2002. 29] C. D. Koutras: A catalog of weak many-valued modal axioms and their corresponding frame classes. Journal of Applied Non-classical Logics, 13 (1): 47-72, 2003. 30] C.-J. Liau, B. I-P. Lin: A theoretical investigation into quantitativemodal logic. Fuzzy Sets and Systems, 75 (3): 355-363, 1995. 41


31] N. Y. Suzuki: Kripke frame with graded accessibility and fuzzy possible world semantics. Studia Logica, 59 (2): 249-269, 1997. 32] U. Straccia: A fuzzy description logic. In Proc. of AAAI'98, 15th National Conf. on Arti cial Intelligence, Wisconsin, Madison, 1998, pp. 594-599. 33] Z. Zhang, Y. Sui, C. Cao:Fuzzy reasoning based on propositional modal logic. In Proc. of the Fourth Internat. Conf. on Rough Sets and Current Trends in Computing (RSCTC2004), Lecture Notes in Computer Science, Vol. 3066, Springer, Berlin, 2004, pp. 109-115. 34] Brachman, R.J., Schmolze, J.G.: An overview of the KL-ONE knowledge representation system, Cognitive Science, 9 (2): 171-216, (1985). 35] Baader, F., Hollunder, B.: A terminological knowledge representation system with complete inference algorithms, in: Richter,M., Boley,H., editors, Proceedings of the First International Workshop on Processing Declarative Knowledge (PDK-91), volume 567 of Lecture Notes in Computer Science, pages 67-85, Kaiserslautern (Germany), Springer-Verlag, (1991). 36] Woods, W.A., Schmolze, J.G.: The KL-ONE family, Computers and Mathematics with Applications, 23 (2-5): 133-177, (1992). 37] F. Baader, P. Narendran: Uni cation of Concept Terms in Description Logics. J. Symb. Comput. 31(3): 277-305 (2001).

42