Лекционный курс (1109962), страница 7
Текст из файла (страница 7)
T0 REALIZUEMA TOGDAI TOLXKO TOGDA, KOGDA REALIZUEMA ODNA IZ TABLIC Ti PRI i 2 f1; 2g.tEOREMA 2.5dOKAZATELXSTWOrASSMOTRETX (8L) I (8R).2iZ \TOJ TEOREMY WYTEKAET, W ^ASTNOSTI, ^TO ESLI MY NA^NEM S KAKOJ-TO TABLICY TI, PRIMENQQ PRAWILA NASY]ENIQ, PO WSEM PUTQM PRIDEM K TABLICAM, NE QWLQ@]IMSQDIZ_@NKTNYMI (W NIH LIBO ? PRINADLEVIT LEWOJ ^ASTI, LIBO IMEETSQ FORMULA,PRINADLEVA]AQ OBEIM ^ASTQM), TO TEM SAMYM MY POKAVEM, ^TO T NEREALIZUEMA.nEDIZ_@NKTNYE TABLICY MY BUDEM NAZYWATX TERMINALXNYMI.dOKAZATELXSTWOM (NEREALIZUEMOSTI) TABLICY T NAZYWAETSQ WSQKOE RASTU]EE WNIZ KONE^NOE DEREWO TABLIC, W KOTOROM T | KORENX, LISTXQ | TERMINALXNYE TABLICY IoPREDELENIE 2.6semanti~eskie tablicy39 ESLI T0 | NELISTOWAQ TABLICA, TO NEPOSREDSTWENNO NIVE NEE RASPOLOVENY TABLICY T1; T2 (ILI ODNA TABLICA T1), POLU^A@]IESQ IZ T0 PO ODNOMU IZ PRAWILNASY]ENIQ.2.1.pRIMER 2.78x(P (x) ! Q(x)) ! (9xP (x) ! 9xQ(x))pUSTX T | KONE^NAQ TABLICA.
tOGDA LIBO T REALIZUETSQ W KONE^NOJILI S^ETNOJ INTERPRETACII, LIBO SU]ESTWUET DOKAZATELXSTWO NEREALIZUEMOSTIT.dOKAZATELXSTWO mY RASSMOTRIM TOLXKO SLU^AJ, KOGDA T NE SODERVIT FUNKCIONALXNYH SIMWOLOW. iDEQ DOKAZATELXSTWA SOSTOIT W SISTEMATI^ESKOM PRIMENENII PRAWIL NASY]ENIQ S TEM, ^TOBY LIBO POSTROITX REALIZU@]U@ MODELX, LIBO NAJTI DOKAZATELXSTWO NEREALIZUEMOSTI. oBLASTX INTERPRETACII BUDET STROITXSQ IZ PEREMENNYH I KONSTANT.pUSTX u1; : : : ; uk | WSE SWOBODNYE PEREMENNYE I KONSTANTY IZ T , A uk+1 ; uk+2; : : : |BESKONE^NYJ ZAPAS NOWYH PEREMENNYH, NE IME@]IH WHOVDENIJ W T . u^ITYWAQ OGRANI^ENIQ W PRAWILAH (8R) I (9L), MY DOLVNY WSE WREMQ POMNITX, KAKIE PEREMENNYEUVE BYLI UVE ISPOLXZOWANY (AKTIWIROWANY), A KAKIE NET. w NA^ALXNYJ MOMENT MYS^ITAEM AKTIWIROWANNYMI TOLXKO u1; : : :; uk (ESLI k = 0, TO TOLXKO PEREMENNU@ u1| W T ONA NE WHODIT).
|TO | NA^ALXNYE \LEMENTY NA[EJ OBLASTI INTERPRETACII.iTAK, ISHODNAQ POZICIQ: T , D SODERVIT u1; : : :; uk (k 1) | AKTIWIROWANNYE PEREMENNYE I KONSTANTY, I IMEETSQ ZAPAS uk+1; uk+2; : : : NEAKTIWIROWANNYH PEREMENNYH,^ASTX IZ KOTORYH MY WPOSLEDSTWII POMESTIM W D.dEREWO TABLIC, KOTOROE W KONE^NOM S^ETE LIBO BUDET DOKAZATELXSTWOM NEREALIZUEMOSTI, LIBO DAST KONE^NU@ ILI S^ETNU@ REALIZU@]U@ MODELX, MY BUDEM STROITXPO \TAPAM.|TAP 0. pOME]AEM T W KORENX STROQ]EGOSQ DEREWA.|TAP N (N > 0).
sLU^AJ 1. wSE LISTXQ POSTROENNOGO NA PREDYDU]EM \TAPE DEREWA | AKSIOMY. tOGDA \TO DEREWO QWLQETSQ DOKAZATELXSTWOM NEREALIZUEMOSTI T .pOSTROENIE DEREWA NA \TOM ZAWER[AETSQ.sLU^AJ 2. eSLI SLU^AJ 1 NE IMEET MESTA, TO PUSTX T1; : : : ; Tr | WSE NETERMINALXNYE LISTXQ UVK POSTROENNOJ ^ASTI DEREWA G (NA PERWOM \TAPE LISTOM QWLQETSQ T ).pROSMATRIWAEM IH PO O^EREDI. nA^INAEM S T1 = 1 j1.
wSE FORMULY IZ 1 I 1,OTLI^NYE OT ATOMOW, OB_QWLQEM DOSTUPNYMI W T1; ESLI DOSTUPNYH FORMUL NET, TOPROCESS POSTROENIQ ZAWER[AETSQ. tEPERX MY RAS[IRQEM G DO TEH POR, POKA W EGOLISTXQH NE OSTANETSQ DOSTUPNYH FORMUL. {AG POSTROENIQ TAKOW. bEREM UVE IME@]U@SQ LISTOWU@ TABLICU T 0 = 0 j0 (NA PERWOM [AGE T 0 = T1) I PUSTX ' | ODNA IZ EEDOSTUPNYH FORMUL. wOZMOVNO NESKOLXKO SLU^AEW. pUSTX, K PRIMERU, ' = ! 2 0.tOGDA POME]AEM POD T 0 DWE TABLICY W SOOTWETSTWII S PRAWILOM (! L):T 0 = ! ; jT 00 = ; ! ; j! ; j; = T 000tEOREMA 2.840 glawa 2. klassi~eskaq logika predikatow perwogo porqdkaI OB_QWLQEM DOSTUPNYMI W T 00 I T 000 WSE TE I TOLXKO TE FORMULY IZ I , KOTORYEBYLI DOSTUPNY W T 0.
(aNALIZ I OSTAWLQEM DO SLEDU@]EGO \TAPA). dRUGIE GLAWNYESWQZKI ' SLEWA I SPRAWA RASSMATRIWA@TSQ ANALOGI^NO. pUSTX TEPERX ' = 8x (x) DOSTUPNA W T 0 I WHODIT W 0, ul (l > 1) | PERWAQ IZ PEREMENNYH NA[EGO SPISKA, NE WSTRE^A@]AQSQ W T 0 ILI WY[E (T.E. PERWAQ NE AKTIWIROWANNAQ W DANNOJ WETWI PEREMENNAQ).tOGDA W SOOTWETSTWII S (8R) MY POME]AEM POD T 0 TABLICU T 00 = j; 8x (x); (ul)I OB_QWLQEM DOSTUPNYMI W T 00 TE I TOLXKO TE FORMULY IZ I , KOTORYE DOSTUPNYW T 0.
eSLI VE ' = 8x (x) WHODIT W LEWU@ ^ASTX, A v1; : : :; vl | WSE AKTIWIROWANNYEW DANNOJ WETWI PEREMENNYE I KONSTANTY, TAKIE ^TO (vi) 2= 0, TO POME]AEM POD T 0TABLICU (v1); : : : ; (vl); 8x (x); j I OB_QWLQEM W NEJ DOSTUPNYMI TE I TOLXKO TEFORMULY IZ I , KOTORYE DOSTUPNY W T 0. oSTALXNYE TIPY FORMUL RASSMATRIWA@TSQ ANALOGI^NO.nA KAVDOM [AGE ^ISLO DOSTUPNYH FORMUL UMENX[AETSQ NA 1, I W KONCE KONCOWWO WSEH WETWQH, IDU]IH OT T1, MY PRIDEM K TABLICAM BEZ DOSTUPNYH FORMUL. tOGDA PEREHODIM K RASSMOTRENI@ T2 I T.D.
pOSLE ANALIZA Tr \TAP N ZAKAN^IWAETSQ INA^INAETSQ \TAP N + 1.pUSTX MY UVE POSTROILI (BYTX MOVET BESKONE^NOE) DEREWO TABLIC, I PUSTX WNEM IMEETSQ (KONE^NAQ ILI BESKONE^NAQ) WETWX, NE ZAKAN^IWA@]AQSQ TERMINALXNOJTABLICEJ:T = 0j0; T1 = 1j1; T2 = 2j2; : : :SS1pOLOVIM = i=0 i , S = S1i=0 i. o^EWIDNO, ^TO TABLICA S j S | DIZ_@NKTNA. w SAMOM DELE, ESLI \TO NE TAK, TO PUSTX 2 i I 2 j .
nO TOGDA 2 k \ k ,GDE k = maxfi; j g, I ZNA^IT k jk | TERMINALXNAQ TABLICA. sTROIM PO WETWI KONTRMODELX T . oBLASTX@ INTERPRETACII BUDET MNOVESTWO D = fu1; u2; : : :g WSEH AKTIWIROWANNYH W DANNOJ WETWI PEREMENNYH I KONSTANT. pREDIKATNYJ SIMWOL Pi(n) INTERPRETIRUEM OTNO[ENIEM[Pi (t1; : : :; tn) = i () Pi(t1; : : : ; tn) 2[Pi(t1; : : : ; tn) = l () Pi (t1; : : :; tn) 2=kONSTANTY INTERPRETIRUEM SAMI SOBO@.
w REZULXTATE POLU^AEM KONE^NU@ ILI S^ETNU@ INTERPRETACI@ A.iNDUKCIEJ PO ^ISLU SWQZOK I KWANTOROW W FORMULE ' POKAVEM, ^TO ESLI u1; : : :; ul| WSE SWOBODNYE PEREMENNYE IZ ', TO['2=) A j= '[u1; : : :; ul];[' 2 =) A 6j= '[u1; : : :; ul]eSLI ' | ATOM, STO \TO WYTEKAET IZ OPREDELENIQ A I DIZ_@NKTNOSTI S j S . pUSTX' = _ I ' 2 . tOGDA W WETWI ESTX PRAWILOTi = _ ; 0iji; _ ; 0iji ; _ ; 0ijisemanti~eskie tablicy41dOPUSTIM, ^TO NA[A WETWX | LEWAQ.
pO ig A j= [u1; : : :; ul], NO TOGDA MY IMEEM IA j= '[u1; : : :; ul].pUSTX ' = 8x (x) 2 S . tOGDA 8u 2 D (u) 2 S . (eSLI u | PEREMENNAQ, TO ONAWHODIT W (u) SWOBODNO.)SpO ig 8u 2 D A j= [u; u1; : : : ; ul], OTKUDA A j= '[u1; : : :; ul].pUSTX ' = 9x (x) 2 . tOGDA W WETWI IMEETSQ PRAWILOTi = 9x (x); 0iji(u); 9x (x); 0ijiPRI^EM u | SWOBODNAQ PEREMENNAQ FORMULY (u), OTLI^NAQ OT u1; : : :; ul. pO igA j= [u; u1; : : : ; ul] I, SLEDOWATELXNO, A j= 9x (x)[u1; : : :; ul]. oSTALXNYE SLU^AI RASSMATRIWA@TSQ ANALOGI^NO.eSLI u1; : : : ; un | WSE SWOBODNYE PEREMENNYE TABLICY T (ONA STOIT W KORNE DEREWA), TO IZ DOKAZANNOGO WYTEKAET, ^TO A REALIZUET T NA u1; : : :; un.rASSMOTRIM, NAKONEC, STRUKTURU POSTROENNOGO DEREWA G.
wOZMOVNY TRI SLU^AQ:1. G KONE^NO I WSE EGO LISTXQ TERMINALXNY. tOGDA, SOGLASNO POSTROENII@, G |DOKAZATELXSTWO NEREALIZUEMOSTI T .2. w G ESTX KONE^NYJ PUTX, ZAKAN^IWA@]IJSQ NETERMINALXNOJ TABLICEJ. tOGDAA | KONE^NAQ MODELX, REALIZU@]AQ T .3. sLU^AI 1 I 2 NE IME@T MESTA. sLEDOWATELXNO, DEREWO G BESKONE^NO. pO DOKAZYWAEMOJ NIVE LEMME kENIGA W G ESTX BESKONE^NAQ WETWX, I POTOMU A | S^ETNAQINTERPRETACIQ, REALIZU@]AQ T .2.1.2pUSTX G | BESKONE^NOE DEREWO S KORNEM, PRI^EM IZ KAVDOJEGO WER[INY WYHODIT LI[X KONE^NOE ^ISLO REBER.
tOGDA W G IMEETSQ BESKONE^NYJPUTX, NA^INA@]IJSQ IZ KORNQ.lEMMA 2.9 (kENIGA)dOKAZATELXSTWOdOKAZATX.2lEMMA PERESTAET BYTX SPRAWEDLIWOJ, ESLI MY OTBROSIM USLOWIE,SOGLASNO KOTOROMU IZ KAVDOJ WER[INY WYHODIT TOLXKO KONE^NOE ^ISLO REBER. pRIWESTI PRIMER.zAME^ANIE 2.10dLQ FORMUL S FUNKCIONALXNYMI SIMWOLAMI DOKAZATELXSTWO W PRINCIPE TAKOE VE; NADO LI[X AKKURATNO ORGANIZOWATX PEREBOR TERMOW PRI RASSMOTRENIIPRAWIL (8R) I (9L). dETALI W kLINI, PARAGRAF 50.zAME^ANIE 2.1142 glawa 2. klassi~eskaq logika predikatow perwogo porqdkapRINCIP DOKAZATELXSTWA TEOREMY NE IZMENITSQ, ESLI MY BUDEMRASSMATRIWATX BESKONE^NYE TABLICY : : : ; '2; '1j 1; 2; : : :.
(nA \TAPE N NADO RASSMATRIWATX LI[X PERWYE N FORMUL, NE U^ITYWAQ DOBAWLENNYE PRI PRIMENENII PRAWIL,A OSTALXNYE NE TROGATX.)zAME^ANIE 2.12sLEDSTWIE 2.13 (tEOREMA lEWENGEJMA{sKULEMA) eSLI MNOVESTWO PREDLOVENIJ (T.E. ZAMKNUTYH FORMUL) IMEET MODELX, TO ONO IMEET KONE^NU@ ILI S^ETNU@MODELX.dOKAZATELXSTWOrASSMOTRETX TABLICU j , KOTORAQ PO USLOWI@ REALIZUEMA.2pARADOKS sKULEMA.mNOVESTWO PREDLOVENIJ IMEET MODELX TOGDA I TOLXKO TOGDA, KOGDA KAVDOE EGO KONE^NOE PODMNOVESTWO IMEET MODELX.sLEDSTWIE 2.14 (tEOREMA KOMPAKTNOSTI)(() eSLI NE IMEET MODELI, TO TABLICA j NEREALIZUEMA, A ZNA^IT IMEETSQ DOKAZATELXSTWO EE NEREALIZUEMOSTI. pOSKOLXKU ONO KONE^NO, SU]ESTWUETDOKAZATELXSTWO NEREALIZUEMOSTI DLQ EE KONE^NOJ PODTABLICY 0j , I PO\TOMU U 0MODELI NET.2dOKAZATELXSTWO2.1.1iS^ISLENIE PREDIKATOW 1-GO PORQDKAcl1 | \TO cl PL@S DWE SHEMY AKSIOM:8x'(x) ! '(t);'(t) ! 9x'(x);GDE t SWOBODEN DLQ x W '(x), I DWA PRAWILA WYWODA' ! (x)' ! 8x (x)(x) ! '9x (x) ! 'GDE x NE WHODIT SWOBODNO W '.8' `cl1 ' ()j= ':NB: aLGORITMA RASPOZNAWANIQ OB]EZNA^IMOSTI MY TAK I NE NA[LI! ~TO ME[AET?.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
