Päätöslauselma

Erottelusääntö on päättelysääntö , joka nousee lauseiden todistamismenetelmään ristiriitaisuuksia etsimällä; käytetään lauselogiikassa ja ensimmäisen asteen logiikassa . Resoluutiosäännön, jota sovelletaan peräkkäin liuottimien luetteloon, avulla voimme vastata kysymykseen, onko alkuperäisessä loogisten lausekkeiden joukossa ristiriitaa. Erottelusääntöä ehdotettiin vuonna 1930 Jacques Herbrandin väitöskirjassa lauseiden todistamiseksi ensimmäisen asteen muodollisissa järjestelmissä. Säännön kehitti John Alan Robinson vuonna 1965.

Tämän menetelmän pohjalta rakennettuja johdettavuusvarmennusalgoritmeja käytetään monissa tekoälyjärjestelmissä, ja ne ovat myös perusta, jolle Prolog -logiikka-ohjelmointikieli on rakennettu . $A \vdash B$

Propositiolaskenta

Olkoon ja kaksi lausetta lauselaskussa , ja anna , ja , jossa on lausemuuttuja, ja ja ovat mitä tahansa lauseita (etenkin, ehkä tyhjiä tai koostuvat vain yhdestä literaalista). $C_{1}$ $C_{2}$ ${\displaystyle C_{1}=P\tai C'_{1))$ ${\displaystyle C_{2}=\lnot P\lor C'_{2))$ $P$ $C'_1$ $C'_2$

Päätelmäsääntö

{\frac {C_{1},C_{2}}{C'_{1}\lor C'_{2}}}

kutsutaan resoluutiosäännöksi . [yksi]

Lauseita C 1 ja C 2 kutsutaan erotettaviksi (tai vanhempi ), lause on resoluutio , ja kaavat ja ovat vastaliteraaaleja . Yleensä erottelusäännössä otetaan kaksi lauseketta ja luodaan uusi lauseke, joka sisältää kaikki kahden alkuperäisen lausekkeen literaalit kahta keskenään käänteistä literaalia lukuun ottamatta. ${\displaystyle C'_{1}\lor C'_{2))$ $P$ $\l ei P$

Resoluutiomenetelmä

Lauseiden todistaminen rajoittuu sen todistamiseen, että jokin kaava (lauseen hypoteesi) on looginen seuraus kaavojen (oletusten) joukosta. Eli itse lause voidaan muotoilla seuraavasti: "jos totta, niin totta ja ". $G$ ${\displaystyle F_{1},\dots ,F_{k))$ ${\displaystyle F_{1},\dots ,F_{k))$ $G$

Sen todistamiseksi, että kaava on looginen seuraus kaavojen joukosta , käytetään resoluutiomenetelmää seuraavasti. Ensin kootaan joukko kaavoja . Sitten jokainen näistä kaavoista pelkistetään CNF :ksi (disjunkttien konjunktio) ja konjunktiomerkit yliviivataan tuloksena olevissa kaavoissa. Osoittautuu paljon disjunktioita . Ja lopuksi tyhjän lauseen tulos kohteesta . Jos tyhjä lause on johdettu lauseesta , niin kaava on looginen seuraus kaavoista . Jos numerosta ei voida päätellä, se ei ole looginen seuraus kaavoista . Tätä lauseiden todistamismenetelmää kutsutaan resoluutiomenetelmäksi . $G$ ${\displaystyle F_{1},\dots ,F_{k))$ ${\displaystyle \{F_{1},\dots ,F_{k},\neg G\))$ $S$ $S$ $S$ $G$ ${\displaystyle F_{1},\dots ,F_{k))$ $S$ $G$ ${\displaystyle F_{1},\dots ,F_{k))$

Harkitse esimerkkiä resoluutiolla todistetusta menetelmästä. Oletetaan, että meillä on seuraavat lausunnot:

"Omena on punainen ja tuoksuva." "Jos omena on punainen, omena on maukasta."

Todistakaamme väite "omena on maukasta". Otetaan käyttöön joukko kaavoja, jotka kuvaavat yllä olevia lauseita vastaavia yksinkertaisia lauseita. Päästää

X_{1}

- Punainen omena

X_{2}

- "Aromaattinen omena",

X_3

- Herkullinen omena.

Sitten itse lausunnot voidaan kirjoittaa monimutkaisten kaavojen muodossa:

X_{1}\land X_{2}

- "Omena on punainen ja tuoksuva."

{\displaystyle X_{1}\rightarrow X_{3))

"Jos omena on punainen, omena on maukasta."

Sitten todistettava väite ilmaistaan kaavalla . $X_3$

Todistetaan siis, että se on looginen seuraus ja . Ensin laadimme joukon kaavoja, joissa väitteen negaatio todistetaan; saamme $X_3$ $(X_{1}\land X_{2})$ $(X_{1}\to X_{3})$

\{(X_{1}\land X_{2}),(X_{1}\rightarrow X_{3}),\neg X_{3}\}.

Nyt viedään kaikki kaavat konjunktiiviseen normaalimuotoon ja yliviivataan konjunktiot. Saamme seuraavan lausejoukon:

\{X_{1},X_{2},(\neg X_{1}\vee X_{3}),\neg X_{3}\}.

Seuraavaksi etsimme tyhjän lauseen johdannaista. Käytämme resoluutiosääntöä ensimmäiseen ja kolmanteen lausekkeeseen:

\{X_{1},X_{2},(\neg X_{1}\vee X_{3}),\neg X_{3},X_{3}\}.

Käytämme resoluutiosääntöä neljänteen ja viidenteen lausekkeeseen:

\{X_{1},X_{2},(\neg X_{1}\vee X_{3}),\neg X_{3},X_{3},\#\}.

Siten johdetaan tyhjä lause, joten lauseke lauseen negaatiolla kumotaan, joten itse väite todistetaan.

Menetelmän täydellisyys ja tiiviys

Resoluutiosäännöllä on täydellisyysominaisuus siinä mielessä, että sen avulla voidaan aina päätellä tyhjästä lauseesta #, jos alkuperäinen lausejoukko on epäjohdonmukainen. $S$ $S$

Johdatettavuussuhde (johtuen johdannaisen äärellisyydestä) on kompakti: jos , niin on olemassa äärellinen osajoukko , niin että . Siksi meidän on ensin todistettava, että mahdottomuussuhde on kompakti. $S\vdash\#$ $S'\subseteq S$ $S'\vdash\#$

Lemma. Jos jokaisella äärellisellä osajoukolla on tyydyttävä estimaatti, niin koko lausejoukolle on olemassa tyydyttävä estimaatti . $S'\subseteq S$ $S$

Todiste. Oletetaan, että lauseissa on lauseita, jotka käyttävät laskettavaa lausemuuttujien joukkoa . Rakennetaan ääretön binääripuu, jossa kustakin kärjestä nousee kaksi reunaa korkeudella , merkittynä literaaleilla ja vastaavasti. Poistamme tästä puusta ne kärjet, polun varrella olevat literaalit muodostavat arvion, joka on ristiriidassa ainakin yhden disjunktin kanssa . $S$ $p_{1},\ldots ,p_{k},\ldots$ $k$ $\neg p_{k+1}$ $p_{k+1}$ $S$

Tarkastellaan jokaiselle rajallista osajoukkoa , joka koostuu lauseista, jotka eivät sisällä muuttujia . Lemman ehdon mukaan muuttujista on sellainen estimaatti (tai polku karsitun puun tasolla olevaan kärkeen ), että se täyttää kaikki disjunktiot . Tämä tarkoittaa, että katkaistu puu on ääretön (eli se sisältää äärettömän määrän pisteitä). Koenigin äärettömän polun lemman mukaan karsittu puu sisältää äärettömän oksan. Tämä haara vastaa kaikkien muuttujien arviointia , joka tekee kaikki lauseet . Mitä vaadittiin. $k$ $S_{k}\subseteq S$ $p_{k+1}, p_{k+2}, \ldots$ ${\displaystyle p_{1},\ldots ,p_{k))$ $k+1$ $S_k$ $p_{1},\ldots ,p_{k},\ldots$ $S$

Täydellisyyslause lauselogiikan resoluutiomenetelmälle

Lause . Lauseiden joukko S on epäjohdonmukainen silloin ja vain, jos S :ssä (tai S :stä ) on kumoaminen.

Todiste. Tarve (päätöslauselmien menetelmän oikeellisuus) on ilmeinen, koska tyhjä lause ei voi olla tosi missään arvioinnissa. Todistakaamme riittävyys. Kompaktiteettilemman mukaan riittää, kun rajoittumme rajallisen määrän lausemuuttujia tapaukseen. Suoritamme induktion niiden lausemuuttujien lukumäärälle, jotka esiintyvät vähintään yhdessä lauseessa alkaen . Olkoon täydellisyyslause totta , todistakaamme sen totuus . Toisin sanoen näytämme, että mistä tahansa ristiriitaisesta lausejoukosta, jossa esiintyy lausemuuttujia , voidaan johtaa tyhjä lause. $n$ $S$ $n=k$ ${\näyttötyyli n=k+1}$ $S$ $p_{1},\ldots ,p_{k+1}$

Valitaan mikä tahansa lausemuuttuja, esimerkiksi . Tehdään kaksi lausetta ja . Laitamme joukkoon ne lauseet , joista literaalia ei esiinny , ja jokaisesta tällaisesta lauseesta poistamme literaalin (jos se esiintyy siellä). Samalla tavalla joukko sisältää loput lauseista , jotka eivät sisällä literaalia literaalin poistamisen jälkeen (jos se esiintyy niissä). $k+1$ $p_{k+1}$ $S$ ${\displaystyle S_{k+1}^{+))$ $S_{k+1}^{-}$ ${\displaystyle S_{k+1}^{+))$ $S$ $\neg p_{k+1}$ $p_{k+1}$ $S_{k+1}^{-}$ $S$ $p_{k+1}$ $\neg p_{k+1}$

Väitetään, että jokainen lausejoukko ja on epäjohdonmukainen, eli sillä ei ole estimaattia, joka täyttää kaikki lausekkeet samanaikaisesti. Tämä pitää paikkansa, koska estimaatin perusteella , joka täyttää joukon kaikki lausekkeet samanaikaisesti, voidaan rakentaa estimaatti , joka täyttää kaikki joukon lausekkeet samanaikaisesti . On ilmeistä, että tämä arvio täyttää kaikki lauseet, jotka on jätetty pois siirrettäessä kohdasta toiseen , koska nämä lausekkeet sisältävät literaalin . Loput lausekkeet täyttyvät olettaen, että arviointi täyttää kaikki joukon lausekkeet ja siten kaikki laajennetut lausekkeet (lisäämällä hylätty literaali ). Vastaavasti estimaatin perusteella , joka täyttää joukon kaikki lausekkeet samanaikaisesti, voidaan rakentaa estimaatti , joka täyttää kaikki joukon lausekkeet samanaikaisesti . ${\displaystyle S_{k+1}^{+))$ $S_{k+1}^{-}$ ${\näyttötyyli \rho ^{+))$ ${\displaystyle S_{k+1}^{+))$ $\rho ^{+}\cup [\rho (p_{k+1})=0]$ $S$ $S$ ${\displaystyle S_{k+1}^{+))$ $\neg p_{k+1}$ $S$ ${\näyttötyyli \rho ^{+))$ ${\displaystyle S_{k+1}^{+))$ $p_{k+1}$ $\rho ^{-}$ $S_{k+1}^{-}$ $\rho ^{-}\cup [\rho (p_{k+1})=1]$ $S$

Induktio-oletuksella ristiriitaisista lausejoukoista ja (koska jokaisessa niistä esiintyy vain lausemuuttujia ) on johtopäätöksiä tyhjästä lauseesta. Jos palautamme joukkolauseiden pois jätetyn literaalin jokaisessa tyhjän lauseen tulosteen esiintymisessä, saadaan yhdestä literaalista koostuvan lauseen tulos . Vastaavasti tyhjän lauseen johdosta epäjohdonmukaisesta joukosta saadaan yhdestä literaalista koostuvan disjunktin johtaminen . Tyhjän lausekkeen saamiseksi on vielä sovellettava ratkaisusääntöä kerran. Q.E.D. ${\displaystyle S_{k+1}^{+))$ $S_{k+1}^{-}$ $k$ ${\displaystyle p_{1},\ldots ,p_{k))$ $p_{k+1}$ ${\displaystyle S_{k+1}^{+))$ $p_{k+1}$ $S_{k+1}^{-}$ $\neg p_{k+1}$

Predikaattilaskenta

Olkoot C 1 ja C 2 kaksi lausetta predikaattilaskennassa.

Päätelmäsääntö

{\frac {C_{1},C_{2}}{(C'_{1}\lor C'_{2})\sigma }}R

kutsutaan erotussääntöksi predikaattilaskennassa, jos lauseissa C 1 ja C 2 on yhtenäiset vastakirjaimet P 1 ja P 2 eli ja ja atomikaavat P 1 ja P 2 on yhdistetty yleisimmällä yhdistäjällä . ${\displaystyle C_{1}=P_{1}\tai C'_{1))$ $C_2 = \lnot P_2 \tai C'_2$ $\sigma$

Tässä tapauksessa lauseiden C 1 ja C 2 resoluutio on lause , joka saadaan lauseesta yhdistäjällä . [2] $(C'_{1}\tai C'_{2})\sigma$ ${\displaystyle C'_{1}\lor C'_{2))$ $\sigma$

Kuitenkin, koska ensimmäisen kertaluvun predikaattien logiikka tyydyttävälle (yhdenmukaiselle) lausekkeelle on epäselvä, ratkaisuperiaatteeseen perustuva menettely voi jatkua loputtomiin. Tyypillisesti resoluutiota käytetään logiikkaohjelmoinnissa suoran tai käänteisen päättelyn yhteydessä. Suora menetelmä (premissoista) lähtökohdista A, B johtaa johtopäätöksen B (modus ponensin sääntö). Suoran päättelymenetelmän suurin haittapuoli on sen suuntaamattomuus: menetelmän toistuvat sovellukset johtavat yleensä jyrkästi välipäätelmiin, jotka eivät liity tavoitepäätelmään.

Käänteinen menetelmä (tavoitteesta) on suunnattu: halutusta johtopäätöksestä B ja samoista lähtökohdista se johtaa uuden osatavoitteen johtopäätöksen A. Päätelmän jokainen vaihe liittyy tässä tapauksessa aina alun perin asetettuun tavoitteeseen.

Erotteluperiaatteen merkittävä puute on se, että jokaisessa vaiheessa muodostuu joukko solventteja - uusia lausekkeita, joista suurin osa osoittautuu tarpeettomiksi. Tältä osin on kehitetty erilaisia ratkaisuperiaatteen muunnelmia, jotka käyttävät tehokkaampia hakustrategioita ja erilaisia rajoituksia alkulausekkeiden muotoon.

Linkit

↑ Chen Ch., Li R. Matemaattinen logiikka ja automaattinen lauseiden todistaminen , s. 77.
↑ Chen Ch., Li R. Matemaattinen logiikka ja automaattinen lauseiden todistaminen , s. 85.

Kirjallisuus

Chen Ch., Li R. Luku 5. Resoluutiomenetelmä // Matemaattinen logiikka ja automaattinen lauseen todistaminen = Chin-Liang Chang; Richard Char-Tung Lee (1973). Symbolinen logiikka ja mekaanisen lauseen todistaminen. Akateeminen Lehdistö. - M . : "Nauka" , 1983. - S. 358.
Guts A. K. Luku 1.3. Resoluutiomenetelmä // Matemaattinen logiikka ja algoritmien teoria. - Omsk: perintö. Dialog-Siperia, 2003. - s. 108.
Nilson N. J. Tekoälyn periaatteet. - M. , 1985.
Mendelson E. Johdatus matemaattiseen logiikkaan. - M. , 1984.
Russell S., Norvig P. Tekoäly: moderni lähestymistapa = Artificial Intelligence: a Modern Approach. - M .: Williams, 2006.