Pravidlo rozlišení

Rezoluční pravidlo je pravidlem odvození , vzestupně k metodě dokazování teorémů prostřednictvím hledání rozporů; používá se ve výrokové logice a logice prvního řádu . Rezoluční pravidlo, aplikované sekvenčně pro seznam rezolucí, nám umožňuje odpovědět na otázku, zda existuje rozpor v původní sadě logických výrazů. Pravidlo rozlišení bylo navrženo v roce 1930 v doktorské práci Jacquese Herbranda pro dokazování teorémů ve formálních systémech prvního řádu. Toto pravidlo vyvinul John Alan Robinson v roce 1965.

Algoritmy dokazující odvoditelnost postavené na základě této metody se používají v mnoha systémech umělé inteligence a jsou také základem, na kterém je postaven logický programovací jazyk Prolog . $A \vdash B$

Výrokový počet

Nechť a být dvě věty ve výrokovém počtu , a nechť , a , kde je výroková proměnná, a a jsou nějaké věty (zejména možná prázdné nebo sestávající pouze z jednoho literálu). $C_{1}$ $C_{2}$ ${\displaystyle C_{1}=P\lor C'_{1))$ $C_{2}=\lnot P\lor C'_{2}$ $P$ $C'_1$ $C'_2$

Odvozovací pravidlo

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

tzv . pravidlo rozlišení . [jeden]

Věty C 1 a C 2 se nazývají resolvable (nebo parent ), věta je resolvent , a vzorce a jsou pultové literály. Obecně se v pravidle rozlišení berou dva výrazy a vygeneruje se nový výraz, který obsahuje všechny literály dvou původních výrazů, kromě dvou vzájemně inverzních literálů. ${\displaystyle C'_{1}\lor C'_{2))$ $P$ $\lne P$

Metoda rozlišení

Důkaz teorémů se redukuje na dokazování, že nějaká formule (hypotéza teorému) je logickým důsledkem množiny formulí (předpokladů). To znamená, že samotný teorém může být formulován následovně: „pokud je pravdivý, pak pravdivý a “. $G$ ${\displaystyle F_{1},\dots ,F_{k))$ ${\displaystyle F_{1},\dots ,F_{k))$ $G$

Abychom dokázali, že vzorec je logickým důsledkem souboru vzorců , použije se metoda rozlišení následovně. Nejprve je sestavena sada vzorců . Poté se každý z těchto vzorců zredukuje na CNF (konjunkce disjunktů) a ve výsledných vzorcích se přeškrtnou znaménka spojky. Ukazuje se mnoho disjunktů . A nakonec výstup prázdné klauzule z . Pokud je prázdná klauzule odvozena od , pak je vzorec logickým důsledkem vzorců . Pokud z # nelze odvodit, pak to není logický důsledek vzorců . Tato metoda dokazování teorémů se nazývá rezoluční metoda . $G$ ${\displaystyle F_{1},\dots ,F_{k))$ ${\displaystyle \{F_{1},\tečky ,F_{k},\neg G\))$ $S$ $S$ $S$ $G$ ${\displaystyle F_{1},\dots ,F_{k))$ $S$ $G$ ${\displaystyle F_{1},\dots ,F_{k))$

Zvažte příklad důkazu metodou rozlišení. Řekněme, že máme následující prohlášení:

"Jablko je červené a voňavé." "Pokud je jablko červené, pak je jablko chutné."

Dokažme tvrzení „jablko je chutné“. Představme si sadu vzorců popisujících jednoduché výroky odpovídající výše uvedeným výrokům. Nechat

X_{1}

- Červené jablko

X_{2}

- "Aromatické jablko",

X_3

- Lahodné jablko.

Samotné příkazy pak mohou být zapsány ve formě složitých vzorců:

X_{1}\land X_{2}

- "Jablko je červené a voňavé."

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

"Pokud je jablko červené, pak je jablko chutné."

Potom tvrzení, které má být dokázáno, je vyjádřeno vzorcem . $X_3$

Pojďme tedy dokázat, že je to logický důsledek a . Nejprve sestavíme sadu formulí s negací dokazovaného tvrzení; dostaneme $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}\}.

Nyní uvedeme všechny vzorce do konjunktivního normálního tvaru a spojky proškrtneme. Získáme následující sadu klauzulí:

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

Dále hledáme odvození prázdné klauze. Na první a třetí klauzuli aplikujeme pravidlo řešení:

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

Na čtvrtou a pátou klauzuli aplikujeme pravidlo řešení:

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

Vyvozuje se tedy prázdná klauzule, tudíž se vyvrací výraz s negací výroku, proto se dokazuje samotný výrok.

Úplnost a kompaktnost metody

Pravidlo rozlišení má vlastnost úplnosti v tom smyslu, že jej lze vždy použít k odvození z prázdné klauzule #, pokud je původní sada klauzulí nekonzistentní. $S$ $S$

Relace odvoditelnosti (kvůli konečnosti derivace) je kompaktní: jestliže , pak existuje konečná podmnožina , taková, že . Proto musíme nejprve dokázat, že relace nemožnosti je kompaktní. $S\vdash\#$ $S' \subseteq S$ $S'\vdash\#$

Lemma. Pokud má každá konečná podmnožina uspokojivý odhad, pak existuje vyhovující odhad pro celou množinu klauzulí . $S' \subseteq S$ $S$

Důkaz. Předpokládejme, že tam jsou klauzule, které používají spočetnou množinu výrokových proměnných . Postavme nekonečný binární strom, kde z každého vrcholu vystupují dvě hrany ve výšce , označené literály resp . Z tohoto stromu odstraníme ty vrcholy, literály podél cesty, k nimž tvoří odhad, který je v rozporu s alespoň jedním disjunktem . $S$ $p_{1},\ldots ,p_{k},\ldots$ $k$ $\neg p_{k+1}$ $p_{k+1}$ $S$

U každého zvažte konečnou podmnožinu sestávající z klauzulí, které neobsahují proměnné . Podmínkou lemmatu je takový odhad proměnných (nebo cesta k vrcholu na úrovni ořezaného stromu), že splňuje všechny disjunkce od . To znamená, že zkrácený strom je nekonečný (to znamená, že obsahuje nekonečný počet vrcholů). Podle lemmatu nekonečné cesty Koenig obsahuje ořezaný strom nekonečnou větev. Tato větev odpovídá vyhodnocení všech proměnných , které tvoří všechny klauzule z . Což bylo požadováno. $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$

Věta o úplnosti pro metodu rozlišení pro výrokovou logiku

Věta . Množina klauzulí S je nekonzistentní právě tehdy, když v S (nebo z S ) existuje vyvrácení .

Důkaz. Nutnost (správnost způsobu usnesení) je zřejmá, neboť prázdná klauzule nemůže být pravdivá při žádném hodnocení. Dejme důkaz o dostatečnosti. U lemmatu kompaktnosti se stačí omezit na případ konečného počtu výrokových proměnných. Provedeme indukci počtu výrokových proměnných vyskytujících se alespoň v jedné klauzuli z . Nechť teorém úplnosti platí pro , dokažme jeho pravdivost pro . Jinými slovy, ukážeme, že z jakékoli protichůdné množiny klauzí, ve kterých se vyskytují výrokové proměnné , lze odvodit prázdnou klauzi. $n$ $S$ $n=k$ $n=k+1$ $S$ $p_{1},\ldots ,p_{k+1}$

Zvolme kteroukoli z výrokových proměnných, například . Sestavme dvě sady klauzulí a . Do množiny dáme ty klauze, ve kterých se literál nevyskytuje , a z každé takové klauze literál odstraníme (pokud se tam vyskytuje). Podobně množina obsahuje zbytek klauzulí , které neobsahují literál po odstranění literálu (pokud se v nich vyskytuje). $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}$

Tvrdí se, že každá z množin klauzulí a je nekonzistentní, to znamená, že nemá odhad, který splňuje všechny klauzule současně. To je pravda, protože z odhadu , který splňuje všechny klauzule množiny současně, lze sestavit odhad , který splňuje všechny klauzule množiny současně . Že toto hodnocení splňuje všechny klauzule vynechané při přechodu od do je zřejmé, protože tyto klauzule obsahují doslovný . Zbývající klauzule jsou splněny za předpokladu, že ohodnocení splňuje všechny klauzule sady , a tedy všechny rozšířené klauzule (přidáním vyřazeného literálu ). Podobně z odhadu , který splňuje všechny klauzule množiny současně, lze sestavit odhad , který splňuje všechny klauzule množiny současně . ${\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$

Předpokladem indukce, z protichůdných množin klauzí a (protože v každé z nich se vyskytují pouze výrokové proměnné ), jsou závěry prázdné klauze. Pokud obnovíme vynechaný literál pro množinové klauzule při každém výskytu výstupu prázdné klauzule, dostaneme výstup klauzule skládající se z jediného literálu . Podobně z odvození prázdné klauze z nekonzistentní množiny získáme odvození disjunktu skládajícího se z jediného literálu . Zbývá použít pravidlo řešení jednou, abyste získali prázdnou klauzuli. 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átová kalkulace

Nechť C 1 a C 2 jsou dvě věty v predikátovém počtu.

Odvozovací pravidlo

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

se nazývá rezoluční pravidlo v predikátovém počtu, pokud jsou ve větách C 1 a C 2 sjednocené kontraliterály P 1 a P 2 , tedy , a , a atomové formule P 1 a P 2 jsou sjednoceny nejběžnějším sjednocovačem . ${\displaystyle C_{1}=P_{1}\lor C'_{1))$ $C_2 = \lne P_2 \nebo C'_2$ $\sigma$

V tomto případě je řešením vět C 1 a C 2 věta získaná z věty použitím sjednocovače . [2] $(C'_{1}\lor C'_{2})\sigma$ ${\displaystyle C'_{1}\lor C'_{2))$ $\sigma$

Vzhledem k nerozhodnutelnosti logiky predikátů prvního řádu pro splnitelnou (konzistentní) množinu klauzulí však může procedura založená na rezolučním principu běžet donekonečna. Typicky se rozlišení používá v logickém programování ve spojení s přímým nebo inverzním uvažováním. Přímá metoda (z premis) z premis A, B vyvozuje závěr B (pravidlo modus ponens). Hlavní nevýhodou přímé metody uvažování je její nedostatek směru: opakované aplikace metody obvykle vedou k prudkému nárůstu mezizávěrů, které nesouvisejí s cílovým závěrem.

Opačná metoda (od cíle) směřuje: z požadovaného závěru B a stejných premis odvodí nový dílčí cílový závěr A. Každý krok závěru je v tomto případě vždy spojen s původně stanoveným cílem.

Významný nedostatek rezolučního principu spočívá v tom, že se v každém kroku odvozování množiny rezolucí tvoří nové klauzule, z nichž většina se ukazuje jako nadbytečná. V tomto ohledu byly vyvinuty různé modifikace principu řešení, které využívají efektivnější vyhledávací strategie a různá omezení formy počátečních doložek.

Odkazy

↑ Chen Ch., Li R. Matematická logika a automatické dokazování vět , str. 77.
↑ Chen Ch., Li R. Matematická logika a automatické dokazování vět , str. 85.

Literatura

Chen Ch., Li R. Kapitola 5. Metoda rozlišení // Matematická logika a automatické dokazování vět = Chin-Liang Chang; Richard Char-Tung Lee (1973). Dokazování symbolické logiky a mechanické věty. Academic Press. - M .: "Nauka" , 1983. - S. 358.
Guts A. K. Kapitola 1.3. Metoda rozlišení // Matematická logika a teorie algoritmů. - Omsk: Dědictví. Dialog-Siberia, 2003. - S. 108.
Nilson N. J. Principy umělé inteligence. - M. , 1985.
Mendelson E. Úvod do matematické logiky. - M. , 1984.
Russell S., Norvig P. Umělá inteligence: moderní přístup = Artificial Intelligence: a Modern Approach. — M .: Williams, 2006.