Felbontási szabály

A felbontási szabály a következtetés szabálya, amely az ellentmondások keresésén keresztül a tételek bizonyításának módszeréhez nyúlik fel; a propozíciós logikában és az elsőrendű logikában használatos . A rezolválók listájára szekvenciálisan alkalmazott felbontási szabály lehetővé teszi, hogy megválaszoljuk azt a kérdést, hogy van-e ellentmondás a logikai kifejezések eredeti halmazában. A felbontási szabályt 1930-ban javasolta Jacques Herbrand doktori disszertációjában tételek bizonyítására elsőrendű formális rendszerekben. A szabályt John Alan Robinson dolgozta ki 1965-ben.

Az erre a módszerre épülő levezethetőség-bizonyítási algoritmusokat számos mesterséges intelligencia rendszerben alkalmazzák, és egyben a Prolog logikai programozási nyelv alapját is képezik . $A \vdash B$

Állításszámítás

Legyen és két mondat a propozíciós kalkulusban , és legyen , és , ahol egy propozíciós változó, és és tetszőleges mondatok (különösen lehet, hogy üresek vagy csak egy literálból állnak). $C_{1}$ $C_{2}$ ${\displaystyle C_{1}=P\vagy C'_{1))$ ${\displaystyle C_{2}=\lnot P\lor C'_{2))$ $P$ $C'_1$ $C'_2$

Következtetési szabály

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

felbontási szabálynak nevezik . [egy]

A C 1 és C 2 mondatokat feloldhatónak (vagy szülőnek ) nevezzük , a mondatot feloldónak , a és formulákat pedig ellenliteráloknak . Általában két kifejezést veszünk fel egy felbontási szabályban, és egy új kifejezést generálunk, amely tartalmazza a két eredeti kifejezés összes literálját, kivéve két kölcsönösen inverz literált. ${\displaystyle C'_{1}\vagy C'_{2))$ $P$ $\lnem P$

Felbontási módszer

A tételek bizonyítása annak bizonyítására redukálódik, hogy valamilyen formula (a tétel hipotézise) egy képlethalmaz (feltevés) logikai következménye. Vagyis maga a tétel a következőképpen fogalmazható meg: "ha igaz, akkor igaz és ". $G$ ${\displaystyle F_{1},\dots ,F_{k))$ ${\displaystyle F_{1},\dots ,F_{k))$ $G$

Annak bizonyítására, hogy egy képlet egy képlethalmaz logikai következménye , a felbontási módszert a következőképpen alkalmazzuk. Először egy képletkészletet állítunk össze . Ezután mindegyik képlet CNF -re redukálódik (diszjunktusok konjunkciója), és a kötőjeleket áthúzzuk a kapott képletekben. Kiderül, hogy sok a diszjunkció . És végül egy üres záradék kimenete a . Ha az üres tagmondat a -ból származik , akkor a képlet a formulák logikai következménye . Ha a # nem vezethető le, akkor ez nem logikus következménye a képleteknek . Ezt a tételbizonyítási módszert felbontási módszernek nevezzük . $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))$

Tekintsünk egy példát a felbontással történő bizonyításra. Tegyük fel, hogy a következő állításaink vannak:

– Az alma piros és illatos. "Ha az alma piros, akkor az alma finom."

Bizonyítsuk be az „ízletes az alma” állítást. Vezessünk be a fenti állításoknak megfelelő egyszerű állításokat leíró képletkészletet. Hadd

X_{1}

- Piros alma

X_{2}

- "Aromás alma",

X_3

- Finom alma.

Ezután maguk az állítások összetett képletek formájában írhatók fel:

X_{1}\land X_{2}

- "Az alma piros és illatos."

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

"Ha az alma piros, akkor az alma finom."

Ekkor a bizonyítandó állítást a képlet fejezi ki . $X_3$

Tehát bizonyítsuk be, hogy és logikus következménye . Először is összeállítunk egy képlethalmazt a bizonyított állítás tagadásával; kapunk $X_3$ $(X_{1}\land X_{2})$ $(X_{1}\-X_{3})$

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

Most az összes képletet konjunktív normálformába hozzuk, és áthúzzuk az kötőszavakat. A következő kitételeket kapjuk:

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

Ezután keressük egy üres záradék származtatását. A felbontási szabályt az első és harmadik záradékra alkalmazzuk:

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

A felbontási szabályt a negyedik és ötödik záradékra alkalmazzuk:

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

Így üres záradékot vezetünk le, így az állítás tagadásával járó kifejezést cáfoljuk, így magát az állítást bizonyítjuk.

A módszer teljessége és tömörsége

A felbontási szabály teljességi tulajdonsággal rendelkezik abban az értelemben, hogy mindig használható egy üres záradékból # következtetni, ha az eredeti tagmondat nem konzisztens. $S$ $S$

A levezethetőségi reláció (a levezetés végessége miatt) kompakt: ha , akkor van véges részhalmaza , úgy, hogy . Ezért először be kell bizonyítanunk, hogy a lehetetlenségi reláció kompakt. $S\vdash\#$ $S'\subseteq S$ $S'\vdash\#$

Lemma. Ha minden véges részhalmaznak van kielégítő becslése, akkor van kielégítő becslés a klózok teljes halmazára . $S'\subseteq S$ $S$

Bizonyíték. Tételezzük fel, hogy vannak olyan klózok, amelyek megszámlálható állítási változókat használnak . Építsünk egy végtelen bináris fát, ahol minden csúcsból két él emelkedik ki egy magasságban , literálokkal , ill. Ebből a fából eltávolítjuk azokat a csúcsokat, az elérési út mentén lévő literálokat, amelyek legalább egy diszjunktnak ellentmondó becslést alkotnak . $S$ $p_{1},\ldots ,p_{k},\ldots$ $k$ $\neg p_{k+1}$ $p_{k+1}$ $S$

Mindegyik esetében vegyünk egy véges részhalmazt , amely olyan klózokból áll, amelyek nem tartalmaznak változókat . A lemma feltétele szerint a változóknak olyan becslése van (vagy egy út a csúcshoz a metszett fa szintjén), hogy teljesíti az összes diszjunkciót -ból . Ez azt jelenti, hogy a csonka fa végtelen (vagyis végtelen számú csúcsot tartalmaz). A Koenig végtelen ösvény lemmája szerint a metszett fa végtelen ágat tartalmaz. Ez az ág az összes változó kiértékelésének felel meg , amely az összes tagmondatot a -ból állítja elő . Amire szükség is volt. $k$ $S_{k}\subseteq S$ $p_{k+1}, p_{k+2}, \lpontok$ ${\displaystyle p_{1},\ldots ,p_{k))$ $k+1$ $S_k$ $p_{1},\ldots ,p_{k},\ldots$ $S$

Teljességi tétel a propozíciós logika felbontási módszeréhez

Tétel . Az S tagmondatok halmaza akkor és csak akkor inkonzisztens, ha S-ben ( vagy S -ből ) van cáfolat.

Bizonyíték. A szükségesség (a határozatok módszerének helyessége) nyilvánvaló, hiszen az üres tagmondat egyetlen értékelésnél sem lehet igaz. Adjunk bizonyítékot az elégségességről. A tömörségi lemma alapján elegendő, ha véges számú propozíciós változó esetére szorítkozunk. Indukciót hajtunk végre azon propozíciós változók számán, amelyek legalább egy klózban előfordulnak -tól . Legyen igaz a teljességi tétel -re , bizonyítsuk be az igazságát . Más szavakkal, megmutatjuk, hogy bármely ellentmondó klózhalmazból, amelyben propozíciós változók fordulnak elő , üres klózt lehet levezetni. $n$ $S$ $n=k$ $n=k+1$ $S$ $p_{1},\ldots ,p_{k+1}$

Válasszuk ki a propozíciós változók bármelyikét, például . Alkossunk két klózhalmazt és . A halmazba azokat a tagmondatokat helyezzük el , amelyekben a literál nem fordul elő , és minden ilyen tagmondatból eltávolítjuk a literált (ha ott előfordul). Hasonlóképpen, a halmaz tartalmazza a literált nem tartalmazó tagmondatokat a literál eltávolítása után (ha előfordul bennük). $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}$

Azt állítják, hogy az és a klózhalmazok mindegyike inkonzisztens, vagyis nincs olyan becslése, amely egyszerre kielégíti az összes klózt. Ez azért igaz, mert egy olyan becslésből , amely egyidejűleg kielégíti a halmaz összes klózát, megalkotható egy olyan becslés , amely egyidejűleg kielégíti a halmaz összes klózát . Nyilvánvaló, hogy ez a kiértékelés teljesíti az összes kihagyott záradékot a -tól -ig , mert ezek a tagmondatok tartalmazzák a literált . A többi tagmondat teljesül, ha feltételezzük, hogy a kiértékelés megfelel a halmaz összes tagjának , és így az összes kiterjesztett tagmondatnak (az elvetett literál hozzáadásával ). Hasonlóképpen, egy olyan becslésből , amely egyidejűleg kielégíti a halmaz összes klózát, megalkotható egy olyan becslés , amely egyidejűleg kielégíti a halmaz összes klózát . ${\displaystyle S_{k+1}^{+))$ $S_{k+1}^{-}$ ${\displaystyle \rho ^{+))$ ${\displaystyle S_{k+1}^{+))$ $\rho ^{+}\cup [\rho (p_{k+1})=0]$ $S$ $S$ ${\displaystyle S_{k+1}^{+))$ $\neg p_{k+1}$ $S$ ${\displaystyle \rho ^{+))$ ${\displaystyle S_{k+1}^{+))$ $p_{k+1}$ $\rho ^{-}$ $S_{k+1}^{-}$ $\rho ^{-}\cup [\rho (p_{k+1})=1]$ $S$

Az indukció feltételezésével ellentmondó klózhalmazokból és (mivel mindegyikben csak propozíciós változók fordulnak elő ) egy üres tagmondat következtetései vannak. Ha visszaállítjuk a kihagyott literált a halmazmondatokhoz egy üres klóz kimenetének minden előfordulásakor, akkor egy egyetlen literálból álló klóz kimenetét kapjuk . Hasonlóképpen, egy inkonzisztens halmazból származó üres tagmondat származtatásából megkapjuk az egyetlen literálból álló diszjunkt származtatását . A feloldási szabályt egyszer kell alkalmazni, hogy üres záradékot kapjunk. 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}$

Predikátumszámítás

Legyen C 1 és C 2 két mondat a predikátumszámításban.

Következtetési szabály

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

Felbontási szabálynak nevezzük a predikátumszámításban, ha a C 1 és C 2 mondatokban egységes P 1 és P 2 ellenliterálok , azaz és , valamint a P 1 és P 2 atomi képleteket a leggyakoribb egyesítő egyesíti . ${\displaystyle C_{1}=P_{1}\vagy C'_{1))$ $C_2 = \lnem P_2 \vagy C'_2$ $\sigma$

Ebben az esetben a C 1 és C 2 mondatok felbontása a mondatból az egyesítő alkalmazásával kapott mondat . [2] $(C'_{1}\vagy C'_{2})\sigma$ ${\displaystyle C'_{1}\vagy C'_{2))$ $\sigma$

A kielégíthető (konzisztens) klózhalmaz elsőrendű predikátumai logikájának eldönthetetlensége miatt azonban a felbontási elven alapuló eljárás korlátlanul futhat. A felbontást általában a logikai programozásban a közvetlen vagy inverz érveléssel együtt használják. A közvetlen módszer (a premisszákból) az A, B premisszákból vezeti le a B következtetést (a modus ponens szabályát). A közvetlen érvelési módszer fő hátránya az iránytalanság: a módszer ismételt alkalmazása általában a célkövetkeztetéshez nem kapcsolódó köztes következtetések meredek növekedéséhez vezet.

A fordított módszer (a célból) irányul: a kívánt B következtetésből és ugyanazokból a premisszákból egy új A részcél következtetést vezet le. A következtetés minden lépése ebben az esetben mindig az eredetileg kitűzött célhoz kapcsolódik.

A felbontási elv jelentős hiányossága abban rejlik, hogy a levezetés minden lépésében létrejön egy sor rezolváló - új záradék, amelyek többsége feleslegesnek bizonyul. E tekintetben a feloldási elv különféle módosításait fejlesztették ki, amelyek hatékonyabb keresési stratégiákat és különféle korlátozásokat alkalmaznak a kezdeti záradékok formájára vonatkozóan.

Linkek

↑ Chen Ch., Li R. Matematikai logika és automatikus tételbizonyítás , p. 77.
↑ Chen Ch., Li R. Matematikai logika és automatikus tételbizonyítás , p. 85.

Irodalom

Chen Ch., Li R. Fejezet 5. Felbontási módszer // Matematikai logika és automatikus tételbizonyítás = Chin-Liang Chang; Richard Char-Tung Lee (1973). Szimbolikus logika és mechanikai tételbizonyítás. Akadémiai Kiadó. - M . : "Nauka" , 1983. - S. 358.
Guts A. K. Fejezet 1.3. Felbontási módszer // Matematikai logika és algoritmusok elmélete. - Omszk: Örökség. Dialog-Siberia, 2003. - 108. o.
Nilson N. J. A mesterséges intelligencia alapelvei. - M. , 1985.
Mendelson E. Bevezetés a matematikai logikába. - M. , 1984.
Russell S., Norvig P. Artificial Intelligence: a Modern Approach = Artificial Intelligence: a Modern Approach. - M .: Williams, 2006.