Лекционный курс (1109962), страница 6
Текст из файла (страница 6)
wSE \TI [AGI POKAZANY NA RISUNKE 1.7 (a), A NA RISUNKE 1.7 (b) POKAZANASOOTWETSTWU@]AQ REFLEKSIWNAQ NETRANZITIWNAQ KONTRMODELX DLQ grz.tEPERX PREDPOLOVIM, ^TO NAM PONADOBILASX REFLEKSIWNAQ I TRANZITIWNAQ (T.E. KWAZIUPORQDO^ENNAQ) KONTRMODELX DLQ grz. tOGDA MY DOLVNY WZQTXpRIMER 1.40glawa301.logika wyskazywanijt02(2(p ! 2p) ! p) 2(2(p ! 2p) ! p) ! p2(p ! 2p) ! p p2(p ! 2p)t1?p ! 2pp 2p2(p ! 2p) ! p?t2p(a)p6p6p(b)rIS.
1.7:TRANZITIWNOE ZAMYKANIE OTNO[ENIQ DOSTIVIMOSTI MEVDU t0, t1 I t2 NA RISUNKE 1.7,A POTOMU SKOPIROWATX SODERVIMOE LEWOJ ^ASTI t0 (TAM WSE FORMULY IME@T WID 2')W LEWYE ^ASTI t1 I t2. nO W \TOM SLU^AE PO (SR5) FORMULA 2(p ! 2p) DOLVNA BYTXZAPISANA W PRAWU@ ^ASTX t2, ^TO WOZWRA]AET NAS W SITUACI@, S KOTOROJ MY NA^INALI W t0, TOLXKO TEPERX \TA SITUACIQ SLOVILASX W t2. tAK MY POLU^AEM BESKONE^NU@POSLEDOWATELXNOSTX TABLIC t0 ! t1 ! t2 ! : : :, W KOTOROJ PRI i = 1; 2; : : : TABLICA t2iQWLQETSQ KOPIEJ t0, A t2i+1 | KOPIEJ t1.
rEFLEKSIWNAQ I TRANZITIWNAQ KONTRMODELX,SOOTWETSTWU@]AQ \TOJ SISTEME TABLIC, IZOBRAVENA NA RISUNKE 1.8 (a).mOVNO IZBEVATX BESKONE^NOJ CEPI TABLIC, ESLI STROQ t2 PROSTO NARISOWATX STRELKU IZ t1 W t0, POLOVIW TEM SAMYM, ^TO W \TOJ SISTEME TABLIC ONI WIDQT DRUG DRUGA.sOOTWETSTWU@]AQ KONTRMODELX POKAZANA NA RISUNKE 1.8 (b).1.3.2pRIMERY MODALXNYH LOGIKw \TOM PARAGRAFE MY OPREDELIM NESKOLXKO KONKRETNYH MODALXNYH LOGIK. bOLX[INSTWO PREDSTAWLQEMYH ZDESX LOGIK BUDUT OPREDELQTXSQ, PODOBNO Cl I Int, SEMANTI^ESKI, T.E.
KAK MNOVESTWA FORMUL ISTINNYH W NEKOTORYH [KALAH. nO INOGDA PREDPO^TITELXNEE SINTAKSI^ESKOE OPREDELENIE LOGIKI W WIDE IS^ISLENIQ. sLEDU@]IE PONQTIQUSTANAWLIWA@T SWQZX MEVDU \TIMI METODAMI.iS^ISLENIE C NAZYWAETSQ KORREKTNYM OTNOSITELXNO KLASSA [KAL K, ESLI DLQL@BOJ FORMULY ' IZ `C ' SLEDUET F j= ' DLQ L@BOJ [KALY F 2 K. iS^ISLENIE C1.3.modalxnaq logika31...p6p6p6pp p (b) (a)rIS.
1.8:NAZYWAETSQ POLNYM OTNOSITELXNO K, ESLI ' WYWODIMA W C , KAK TOLXKO ONA ISTINNAWO WSQKOJ [KALE IZ K.gOWORIM, ^TO LOGIKA L HARAKTERIZUETSQ KLASSOM [KAL K, ESLIL = f' 2 ForML : 8F 2 K F j= 'g:lOGIKA S4 HARAKTERIZUETSQ KLASSOM WSEH KWAZIUPORQDO^ENNYH [KAL, T.E.S4 = f' 2 ForML : F j= ' DLQ L@BOJ REFLEKSIWNOJ I TRANZITIWNOJ Fg:iS^ISLENIE S 4 IMEET SWOIMI AKSIOMAMI WSE AKSIOMY cl, A TAKVE WSE FORMULY WIDA(A11) 2(' ! ) ! (2' ! 2 ,(A12) 2' ! ',(A13) 2' ! 22';PRAWILA WYWODA DWA: ZNAKOMOE NAM modus ponens I PRAWILO(RN): IZ ' POLU^AEM 2'.iS^ISLENIE S 4 KORREKTNO I POLNO OTNOSITELXNO KLASSA KWAZIUPORQDO^ENNYH [KAL. lOGIKA S4 HARAKTERIZUETSQ KLASSOM WSEH KONE^NYH KWAZIUPORQDO^ENNYH [KAL.pREDLOVENIE 1.41iS^ISLENIE S 4 BYLO POSTROENO S CELX@ WYQSNENIQ SWOJSTW MODALXNOSTI DOKAZUEMO; W ISKUSSTWENNO INTELLEKTE S 4 PRIMENQETSQ TAKVE KAK LOGIKA ZNANIQ, W KOTOROJ2 INTERPRETIRUETSQ KAK IZWESTNO.lOGIKU S5, OPREDELQEMU@ KLASSOM [KAL S UNIWERSALXNYMI OTNO[ENIQMI DOSTIVIMOSTI (WSE TO^KI WIDQT DRUG DRUGA), MOVNO PONIMATX KAK LOGIKU LOGI^ESKOJNEOBHODIMOSTI.
sOOTWETSTWU@]EE IS^ISLENIE S 5 POLU^AETSQ DOBAWLENIEM K S 4 SHEMY AKSIOM(A14) :2' ! 2:2',KOTORU@ NAZYWA@T NEGATIWNOJ INTROSPEKCIEJ. (A13) | POZITIWNAQ INTROSPEKCIQ.glawa logika wyskazywanijpREDLOVENIE 1.42 iS^ISLENIE S 5 KORREKTNO POLNO OTNOSITELXNO KLASSA [KALS UNIWERSALXNYMI OTNO[ENIQMI DOSTIVIMOSTI. S5 HARAKTERIZUETSQ KLASSOM KONE^NYH UNIWERSALXNYH [KAL.321.rEKOMENDUEM ^ITATEL@ POKAZATX, ^TO S4 S5.lOGIKA D. dEONTI^ESKU@ LOGIKU D (TO^NEE, MINIMALXNU@ DEONTI^ESKU@ LOGIKU) MOVNO OPREDELITX IS^ISLENIEM D, KOTOROE ZADAETSQ AKSIOMAMI (A1){(A11) I(A15) 2' ! 3',KOTORU@ MOVNO PRO^ITATX KAK WSE OBQZATELXNOE RAZRE[ENO.iS^ISLENIE D KORREKTNO I POLNO OTNOSITELXNO KLASSA [KALBEZ TUPIKOWYH TO^EK.pREDLOVENIE 1.43lOGIKA S4.3.
eSLI MY PONIMAEM 2 KAK ISTINNO SEJ^AS I WSEGDA BUDET ISTINNO,A WREMQ POLAGAEM LINEJNYM, TO LOGIKUS4:3 = f' 2 ForML : F j= ' DLQ WSQKOJ LINEJNO UPORQDO^ENNOJ [KALY FgMOVNO PONIMATX KAK LOGIKU TAKOJ WREMENNOJ MODALXNOSTI. sOOTWETSTWU@]EE IS^ISLENIE S 4:3 POLU^AETSQ DOBAWLENIEM K S 4 AKSIOMY(A16) 2(2' ! ) _ 2(2 ! ').pREDLOVENIE 1.44 iS^ISLENIE S 4:3 KORREKTNO I POLNO OTNOSITELXNO LINEJNOUPORQDO^ENNYH [KAL.mOVNO AKSIOMATIZIROWATX LOGIKU LINEJNOGO DISKRETNOGO WREMENI, LOGIKU PLOTNOGO NEPRERYWNOGO WREMENI I T.D.
mOVNO WWESTI E]E ODIN MODALXNYJ OPERATOR 2WSEGDA W PRO[LOM:(M; x) j= 2 ' () 8y (yRx ) (M; y) j= '):dLQ OPISANIQ POWEDENIQ PROGRAMM ISPOLXZU@TSQ WREMENNYE LOGIKI S OPERATORAMI | W SLEDU@]IJ MOMENT WREMENI:(M; i) j= ' () (M; i + 1) j= 'U | until:(M; i) j= 'U () 9k i ((M; k) j= & 8j 2 fi; : : :; k 1g (M; k) j= '):wOT MODALXNYE AKSIOMY ODNOJ LOGIKI S WWEDENNYMI OPERATORAMI:2(' ! ) ! (2' ! 2 )modalxnaq logika(' ! ) ! (' ! ):' $ : '2' ! ' ^ 2'2(' ! ') ! (' ! 2')'U ! 3'U $ _ (' ^ ('U ))pRAWILA WYWODA | '=2' I '= '.1.3.33pROPOZICIONALXNAQ DINAMI^ESKAQ LOGIKA PDL.
s KAVDOJ KOMANDOJ a NE-KOTOROGO QZYKA PROGRAMMIROWANIQ MOVNO ASSOCIIROWATX MODALXNYJ OPERATOR [a] |[a]' IMEET MESTO, KOGDA ' WYPOLNQETSQ WSQKIJ RAZ POSLE ISPOLNENIQ a. pOLU^A@]IJSQ POLIMODALXNYJ QZYK MOVNO ISPOLXZOWATX DLQ WYRAVENIQ SWOJSTW SLOVNYHPROGRAMM W TERMINAH SOSTAWLQ@]IH IH ATOMARNYH PROGRAMM.aLFAWIT PDL: SODERVIT PROPOZICIONALXNYE PEREMENNYE pi , KONSTANTU ? I PROGRAMMNYE PEREMENNYE 2 . iZ NIH STROQTSQ SOSTAWNYE PROGRAMMY I FORMULY: KAVDAQ PROPOZICIONALXNAQ PEREMENNAQ I ? | FORMULA, A KAVDAQ PROGRAMMNAQPEREMENNAQ | PROGRAMMA; ESLI a, b | PROGRAMMY, A ', | FORMULY, TO{ a [ b (WYPOLNITX (NEDETERMINIROWANNO) LIBO a, LIBO b){ a; b (WYPOLNITX SNA^ALA a, A ZATEM b){ a (WYPOLNITX a NEKOTOROE (KONE^NOE) ^ISLO RAZ){ '? (PRODOLVITX, ESLI ' ISTINNA, INA^E OSTANOWITXSQ)SUTX PROGRAMMY, A ' ! , ' _ , ' ^ I [a]' | FORMULY.dRUGIE PROGRAMMNYE KONSTRUKCII MOVNO WWESTI SLEDU@]IM OBRAZOM:if ' then a else b | ('?; a) [ (:'?; b)while ' do a | ('?; a); :'?I T.D.sEMANTIKA PDL.
mODELI PDL | STRUKTURY WIDAM = hS; fRa : a | PAROGRAMMAg; Vi ;W KOTORYH V : Var ! 2S , R PRI 2 | PROIZWOLXNYE BINARNYE OTNO[ENIQ,Ra;b = Ra RbRa[b = Ra [ RbRa = Ra (REFLEKSIWNOE I TRANZITIWNOE ZAMYKANIE)glawa341.logika wyskazywanijR'? = fhs; si : (M; s j= 'g, GDE(M; s) j= [a] () 8t 2 S (sRat ) (M; t) j= ):iS^ISLENIE PDL SODERVIT POMIMO (A1){(A10) SLEDU@]IE AKSIOMY:[a; b]' $ [a][b]'[a [ b]' $ [a]' ^ [b]'[a]' ! ' ^ [a][a]'[a](' ! [a]') ! (' ! [a]'['?] $ (' ! )pRAWILA WYWODA | modus ponens I '=[a]' DLQ L@BOJ a.pREDLOVENIE 1.45LQH.`PDL ' TOGDA I TOLXKO TOGDA, KOGDA ' ISTINNA WO WSEH MODE-pRIMENENIQ: PROBLEMA WERIFIKACII PROGRAMM. pUSTX IMEETSQ PROGRAMMA a; (x)| SWOJSTWO, HARAKTERIZU@]EE DOPUSTIMYE NABORY ISHODNYH DANNYH x, A (y) |USLOWIE, KOTOROMU DOLVNY UDOWLETWORQTX REZULXTIRU@]IE DANNYE y. tOGDA USLOWIEPRAWILXNOSTI a MOVNO PREDSTAWITX KAK8x8y ((x) ! [a](y)):gLAWA 2kLASSI^ESKAQ LOGIKA PREDIKATOWPERWOGO PORQDKApREDSTAWIM SEBE TEPERX, ^TO NAM TREBUETSQ QZYK, W KOTOROM MOVNO OPERIROWATX SPONQTIQMI, TAKIMI KAK PONQTIE NEPRERYWNOJ FUNKCII.
wSPOMNIM, ^TO FUNKCIQ f (x)NEPRERYWNA W TO^KE y, ESLI DLQ L@BOGO > 0 SU]ESTWUET > 0 TAKOE, ^TO DLQWSQKOGO x, ESLI jx yj < , TO jf (x) f (y)j < . (qSNO, ^TO NI QZYKA L, NI ML DLQPREDSTAWLENIQ DANNOGO OPREDELENIQ NE HWATAET: U NAS NET IMENI y, PREDSTAWLQ@]EGOPROIZWOLXNOE ^ISLO, NET IMENI f , PREDSTAWLQ@]EGO PROIZWOLXNU@ FUNKCI@, NET ISREDSTW DLQ WYRAVENIQ TOGO, ^TO NE^TO SPRAWEDLIWO DLQ WSEH ^ISEL ILI DLQ KAKOGOTO ^ISLA.) zAMENQQ SLOWA DLQ L@BOGO ZNAKOM 8, SLOWO SU]ESTWUET ZNAKOM 9 IPOLXZUQSX LOGI^ESKIMI SWQZKAMI QZYKA L, MY POLU^IM WYRAVENIE8 ( > 0 ! 9 ( > 0 ^ 8x (jx yj < ! jf (x) f (y)j < ))):w \TOJ ZAPISI PRISUTSTWU@T PRAKTI^ESKI WSE \LEMENTY QZYKA LOGIKI PREDIKATOW1-GO PORQDKA.
|TO | SIMWOLY PEREMENNYH (, , x, y), KOTORYE (W DANNOM PRIMERE) MYSLQTSQ PRO-BEGA@]IMI OBLASTX WE]ESTWENNYH ^ISEL; ONI NAZYWA@TSQ PREDMETNYMI PEREMENNYMI; SIMWOLY, OBOZNA^A@]IE FIKSIROWANNYE ^ISLA | 0; ONI NAZYWA@TSQ PREDMETNYMI KONSTANTAMI; SIMWOLY, OBOZNA^A@]IE FUNKCII; \TO | DWUHMESTNAQ FUNKCIQ f I ODNOMESTNAQFUNKCIQ j j; ONI NAZYWA@TSQ FUNKCIONALXNYMI SIMWOLAMI; SIMWOLY, OBOZNA^A@]IE OTNO[ENIQ (ILI PREDIKATY); \TO | < I >; ONI NAZYWA@TSQ PREDIKATNYMI SIMWOLAMI;3536 glawa 2.
klassi~eskaq logika predikatow perwogo porqdka SIMWOLY 8 I 9; ONI ^ITA@TSQ DLQ L@BOGO I SU]ESTWUET; IH, A TAKVE WYRAVENIQ 8x I 9x NAZYWA@T KWANTORAMI OB]NOSTI I SU]ESTWOWANIQ, SOOTWET-STWENNO; LOGI^ESKIE SWQZKI.(wSPOMNIM, ^TO n-MESTNYM OTNO[ENIEM ILI PREDIKATOM P NA MNOVESTWE X NAZYWA@TWSQKOE MNOVESTWO n-OK \LEMENTOW IZ X (T.E. P X n ), SKAVEM < = fh0; 2i ; h; 7i ; : : :g.pREDIKAT P MOVNO RASSMATRIWATX KAK PROPOZICIONALXNU@ FUNKCI@ IZ X n W fi,lg:(, ESLI ha1; : : : ; ani 2 PP (a1; : : : ; an) = il, ESLI ha1; : : : ; ani 2= PoDNOMESTNOE OTNO[ENIE NAZYWAETSQ SWOJSTWOM.)a TEPERX FORMALXNOE OPREDELENIE. aLFAWIT QZYKA PL LOGIKI PREDIKATOW PERWOGOPORQDKA SODERVIT1.
S^ETNOE MNOVESTWO PREDMETNYH PEREMENNYH x1; x2; : : :2. NE BOLEE ^EM S^ETNOE (BYTX MOVET PUSTOE) MNOVESTWO PREDMETNYH KONSTANTa1; a2; : : :3. NE BOLEE ^EM S^ETNOE (BYTX MOVET PUSTOE) MNOVESTWO FUNKCIONALXNYH SIMWOLOWf1(n ); f2(n ); : : : (ni | ^ISLO ARGUMENTOW U fi(n ))4. NE BOLEE ^EM S^ETNOE NEPUSTOE MNOVESTWO PREDIKATNYH SIMWOLOW P1(m ); P2(m ); : : :5. KWANTOROW I SWQZOK 8, 9, !, ^, _ I KOSTANTY ?6. ZNAKOW PUNKTUACII :, ( I ).12i12tERM QZYKA PL: pEREMENNYE I KONSTANTY | TERMY; ESLI fi(n) | n-MESTNYJ FUNKCIONALXNYJ SIMWOL, A t1; : : :; tn | TERMY, TO fi(n)(t1; : : : ; tn)| TERM; DRUGIH TERMOW NET.oPREDELENIE 2.1w NA[EM PRIMERE TERMAMI BYLI 0, y, f (x), jx yj, HOTQ POSLEDNIJ MY ZAPISALIBY TEPERX W PREFIKSNOM WIDE, NAPODOBIE g(h(x; y)).tERMY PREDNAZNA^A@TSQ DLQ PREDSTAWLENIQ OB_EKTOW IZ PREDMETNOJ OBLASTI (NAPRIMER, ^ISEL).
rAZNOOBRAZNYE WYSKAZYWANIQ OB OB_EKTAH PREDSTAWLQ@TSQ FORMULAMI.semanti~eskie tablicy37oPREDELENIE 2.2 fORMULA QZYKA PL: ESLI t1; : : :; tn | TERMY, A Pi(n) | n-MESTNYJ PREDIKATNYJ SIMWOL, TO Pi(n)(t1; : : :; tn)| (ATOMARNAQ) FORMULA; ? | TAKVE (ATOMARNAQ) FORMULA; ESLI ' I | FORMULY, A x | PEREMENNAQ, TO (' ! ), (' ^ ), (' _ ), (8x ')I (9x ') | FORMULY; DRUGIH FORMUL NET.2.1.w NA[EM PRIMERE > 0 I jx yj < | ATOMARNYE FORMULY.mY BUDEM S^ITATX, ^TO 8 I 9 SWQZYWA@T FORMULY SILXNEE, ^EM !, ^ I _.2.1sEMANTI^ESKIE TABLICYpRINADLEVNOSTX FORMULY ' L@BOJ IZ RASSMATRIWAW[IHSQ NAMI PROPOZICIONALXNYHLOGIK MOVNO OPREDELQTX, PYTAQSX OPROWERGNUTX ' NA KONE^NOJ MODELI NEKOTOROGOFIKSIROWANNOGO RAZMERA.
w SLU^AE LOGIKI PREDIKATOW \TO NE TAK.pRIMER 2.3rASSMOTRIM FORMULU' = 8x:x < x ^ 8x8y8z (x < y ^ y < z ! x < z) ^ 8x9y x < yI POKAVEM, ^TO WSE MODELI \TOJ FORMULY BESKONE^NY. dEJSTWITELXNO, DOPUSTIW PROTIWNOE, MY IMELI BY KONE^NU@ MODELX A = hD; <i, W KOTOROJ IMEETSQ BESKONE^NAQCEPO^KA b1 < b2 < b3 : : :. tAK KAK OBLASTX D KONE^NA, W \TOJ CEPO^KE NAJDUTSQ bi = bjPRI i 6= j . nO TOGDA bi < bi I POTOMU A 6j= 8x:x < x | PROTIWORE^IE. eSLI VE MYWOZXMEM FORMULU :', TO U NEE, NAOBOROT, NE SU]ESTWUET KONE^NYH KOTRMODELEJ (IBOWSQKAQ KONTRMODELX :' QWLQETSQ MODELX@ ').e]E ODNA TRUDNOSTX PRI RASPROSTRANENII METODA SEMANTI^ESKIH TABLIC NA LOGIKU PREDIKATOW | \TO POSTROENIE OBLASTI INTERPRETACII.
iZ KAKIH \LEMENTOW EESTROITX? pOSKOLXKU W SU]NOSTI \TO BEZRAZLI^NO, DAWAJTE STROITX EE IZ TOGO, ^TO UNAS IMEETSQ | PEREMENNYH, KONSTANT I TERMOW.pRIMER 2.4oB]EZNA^IMA LI FORMULA' = 9x(P (a) ! Q(x)) ! (P (a) ! 8xQ(x))?pOSTROITX KONTRMODELX A = hD; P; Qi, W KOTOROJ D = fx1; x2; ag, Q(x1) = i, Q(x2) =l, P (a) = i, A OSTALXNYE ZNA^ENIQ PROIZWOLXNY.38 glawa 2. klassi~eskaq logika predikatow perwogo porqdkapRIMER 2.3 POKAZYWAET, ODNAKO, ^TO W OB]EM SLU^AE ZA KONE^NOE ^ISLO [AGOWKOTRMODELI MY MOVEM I NE POSTROITX. s TABLICAMI W LOGIKE PREDIKATOW OBRA]ATXSQNAMNOGO TRUDNEE. w DALXNEJ[EM NAM BUDET UDOBNEE PREDSTAWLQTX TABLICY W WIDE j,GDE j OTDELQET LEWU@ ^ASTX ( ) TABLICY OT PRAWOJ ()).pRAWILA NASY]ENIQ:(^L) : '; ';^' ^; j;j (^R) : j; ' ^ j;'; ' ^j; ' ^ ;j; ' _' _ ; j(_R) :(_L) :'; ' _ ; j ; ' _ ; jj; ' _ ; ';j; ' !; j(! L) : ; ' ! '; !(!R):j ' ! ; j; ''; j; ' ! ;(x); jj; 8x'(x)(8L) : '(t8)x'(8R):; 8x'(x); jj; 8x'(x); '(y)j; 9x'(x)9x'(x); j(9R) :(9L) :'(y); 9x'(x); jj; 9x'(x); '(t)zDESX W PRAWILAH (8R) I (9L) PEREMENNAQ y NE WHODIT SWOBODNO W FORMULY WERHNEJTABLICY, A W PRAWILAH (8L) I (9R) t | PROIZWOLXNYJ TERM, SWOBODNYJ DLQ x W '(x).pUSTX x1; x2; : : : | WSE SWOBODNYE PEREMENNYE, WHODQ]IE W TABLICU T = j.
nAZOWEM T REALIZUEMOJ W INTERPRETACII A NA \LEMENTAH b1; b2; : : :, ESLI A j= '[b1; b2; : : :]DLQ WSEH ' 2 I A 6j= [b1; b2; : : :] DLQ WSEH 2 . tABLICA NAZYWAETSQ REALIZUEMOJ,ESLI ONA REALIZUEMA W NEKOTOROJ INTERPRETACII NA NEKOTORYH \LEMENTAH.pUSTX T0=T1(T2) | ODNO IZ PRAWIL NASY]ENIQ.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
