Logikázik

Rezolúciós elv

Szintaktikus levezetésfogalom levezethetőséggel jellemezhető (Bizonyítás előállításával igazolható a kalkulus teljessége és helyessége)

Szemantikus eldöntésprobléma szintaktikus módszerrel megközelítése

Levezető eljárás

Döntési "Algoritmus" olyan lépéssorozat, ami a megadott bemeneti adatok és a megfelelő szabályok használatával eljut a kitűzött célig.

Ha az algoritmus nem jut el a kitűzött célig, még nem jelenti önmagában azt, hogy egy másik eshetőségére esne döntés.

Ezek a Kalkulusok.

Előkészítő definíciók

Literál

Egy prímformula, vagy annak negáltja

Elemi konjunkció/diszjunkció

Egységkonjunkciók és diszjunkciók, valamint különböző alapú literálok konjunkciója/diszjunkciója.

Az elemi diszjunkció más néven Klóz

Teljes elemi konjunkció/diszjunkció

Egy elemi konjunkció/diszjunkció \(n\) változós logikai műveletre nézve, ha mind az \(n\) ítéletváltozó alapja valamelyik benne szereplő literálnak

Konjunktív és Kitüntetett Konjunktív normálformák (KNF / KKNF)

KNF

Elemi diszjunkciók (klózok) konjunkciója

KKNF

Olyan KNF, ami teljes elemi diszjunkciók konjunkciója

Diszjunktív és Kitüntetett Diszjunktív normálformák (DNF / KDNF)

DNF

Elemi konjunkciók diszjunkciója

KDNF

Olyan DNF, ami teljes elemi konjunkciók diszjunkciója

Igaz és Hamishalmaz

Egy \(n\)-változós formula az igazságtáblájával megadott \(\left\{i,\,h\right\}^2\;\longrightarrow\;\left\{i,\,h\right\}\) leképezést ír le.

Igazhalmaz

Azon \(\mathcal{I}\) interpretációk halmaza, melyre a formula igazságértéke igaz.

Hamishalmaz

Azon \(\mathcal{I}\) interpretációk halmaza, melyre a formula igazságértéke hamis.

Kielégíthetetlen formula elve

Amennyiben az igazsághalmaza üres, így a KKNF alakjában minden teljes elemi konjunkció szerepel, ha szisztematikusn egyszerűsítűnk a klózok literálszámán, amíg az nullára nem csökken (üres klóz). Egy KNF alakú formuláról egyszerűsítéssel eldönthető annak kielégíthetetlensége.

Klózok kiterjesztése szemantikus fára

Szemantikus fa - Tétel

Ha egy \(S\) véges klózhalmaz szemantikus fája zárt, akkor \(S\) kielégíthetetlen

A klózhalmaz kielégíthetetlenségét nem szmantikus fával döntjük el, de fontos eszköz marad a rezolúciós kalkulus tulajdonságainak vizsgálatában...

Elnevezések

\(n\)-változós klóz
- \(n\)-argumentumos klóz
\(1\)-változós klóz
- Egységklóz
\(2\)-változós klóz
- Üres klóz \(\square\)

Rezolúciós kalkulus Ítéletlogikában

Egyszerűsítési szabály

Ha \(X\) ítéletváltozó és \(C\) egy \(X\)-et nem tartalmazó klóz, akkor \((X\,\lor\,Y)\,\land\,(\neg X\,\lor\,Y)\,\sim_0\,C\)

Az \((X)\,\land\,(\neg X)\,\sim_0\,\square\) - azonosan hamis.

Rezolúciós levezetés

Rezolvens

Legyenek \(C_1,\,C_2\) olyan klózok, amelyek pontosan egy komplemens literálpárt tartalmaznak: \(C_1 = C'_1\,\lor\,L_1\) és \(C_2 = C'_2\,\lor\,L_2\) és \(L_1\,=\,\neg L_2\)

Ekkor létezik a rezolvensük: a \(\text{res}(C_1,C_2)\,=\,C\) klóz, ami \(C\,=\,C'_1\,\lor\,C'_2\)

Rezolvens - Tétel

\(\left\{C_1,\,C_2\right\}\vDash_0C\) A rezolvensképzés a rezolúciós kalkulus levezetési szabálya

(Helyes következtetésforma)

Rezolúciós levezetés - Definíció

Egy \(S\) klózhalmazból való rezolúciós levezetés egy olyan véges \(k_1,k_2,\dots,k_m\quad(m\geq 1)\) klózsorozat, ahol minden \(j\,=\,1,2,\dots,m\)-re

vagy \(k_j\in S\)

vagy van olyan \(1 \leq s,t < j\), hogy \(k_j\) a \((k_s,k_t)\) klózpár rezolvense

Levezetés célja az üres klóz levezetése, vagy a megállási feltétel elérése.

Példa Rezolúciós levezetésre

Adott \(S\) klózhalmaz.

\[ S\,=\,\left\{\neg A\lor B, \neg A \lor C, A \lor C, \neg B\lor \neg C, \neg C\right\} \]

\[ \begin{array}{clr} 1. & \neg C & \left[\in S\right]\\ 2. & A \lor C & \left[\in S\right]\\ 3. & A & \left[\text{res}\left(1,\,2\right)\right]\\ 4. & \neg A \lor C& \left[\in S\right]\\ 5. & C & \left[\text{res}\left(3,\,4\right)\right]\\ 6. & \square & \left[\text{res}\left(1,\,5\right)\right]\\ \end{array} \]

Rezolúció helyessége és teljessége

Helyesség

Legyen \(S\) tetszőleges klózhalmaz és \(k_1,k_2,\dots,k_m\) klózsorozat rezolúciós levezetés \(S\)-ből. Ekkor minden \(k_j,\,j\,=\,1,2,\dots,n\)-re szemantikus következmény \(S\)-nek.

Legyen \(S\) tetszőleges klózhalmaz. Ha \(S\)-bő levezethető az üres klóz, akkor \(S\) kielégíthetetlen.

Bizonyításuk indukcióval lehetséges

Teljesség

Ha az \(S\) véges klóüzhalmaz kielégíthetetlen, akkor \(S\)-ből levezethető az üres klóz.

Teljesség bizonyításának algoritmusa

Tetszőleges zárt szemantikus fa esetén előállítunk egy rezolúciós cáfolatot

\(j\,:=\,0\quad S_j\,:=\,S\quad\text{LIST}\,:=\,\emptyset\)
Állítsuk elő \(S_j\) szemantikus fáját. \(n_j\,:=\) a szemantikus fa szintjeinek száma. Ha \(n_j\,=\,0\), akkor levezetjük az üres klózt, a levezetés \(\text{LIST}\)-ből kiolvasható.
Egyébként válasszuk ki a fa egy levezető csúcsát. A levezető csúcsot tartalmazó két ágra illesztett klózok legyenek \(k'_j\) és \(k''_j\), rezolvensük pedig \(k_j\). Tegyük \(\text{LIST}\) végére a \(k'_j,k''_j,k_j\) klózokat
\(S_{j+1}\,:=\,S_j \cup\left\{k_j\right\},\,j\,:=\,j+1\). Folytassuk a \(2\). lépéssel

Levezetési fa

Egy rezolúciós levezetés szerkezetét mutatja. Olyan gráf, amelynek csúcsaiban klózok vannak. Két csúcsból akkor vezet él egy harmadik csúcsba, ha abban két csúcsban lévő klózok rezolvense található.

Példa rezolúciós levezetési fa szemléltetésére

Levezetési fa példa

Levezetési stratégiák I

Lineáris rezolúciós levezetés

Egy \(S\) klózhalmazból egy olyan \(k_1,l_1,k_2,l_2,\dots,k_{m-1},l_{m-1},k_m\) klózsorozat, ahol \(k_1,l_1\in S\) a \(k_j(i = 2,3,\dots,m)\) esetben a \(k_i\) a \(k_{i-1},l_{i-1}\) rezolvense, ahol \(l_{i-1} \in S\), vagy egy korábban megkapott centrális klóz (rezolvense valamely \(k_s,l_s(s<i)\)-nek)

Lineáris rezolúció kép

Levezetési stratégiák II

Lineáris inputrezolúciós levezetés

\(S\) klózhalmazból egy olyan \(k_1,l_1,k_2,l_2,\dots,k_{m-1},l_{m-1},k_m\) klózsorozat, ahol \(k_1,l_1\in S\), az \(l_i(i = 2,3,\dots,m-1)\) esetben \(l_i \in S\) és a \(k_i\) pedig a \(k_{i-1},l_{i-1}\) rezolvense.

Egységrezolúciós stratégia

Rezolvens csak akkor képezhető, ha legalább az egyik klóz egységklóz

Horn klózok, Horn logika

Horn Klóz

Olyan klóz, aminek legfeljebb egy literálja nem negált

Horn Logika

Az össes, csak Horn klózokat tartalmazó KNF alakú formulák halmaza

Horn Logika - Példa

\[ S\,=\,\left\{B\lor C, A \lor \neg C, \neg A \lor \neg B, \neg A \lor C, C\right\} \]

Horn klózok halmaza

Horn Logika - Teljesség tétel

A lineáris input és egységrezolúciós stratégia teljes a Horn logikában

Horn Logika - Levezethetőségi tétel

Ha az \(\square\) levezethető lineáris input rezolúcuióval egy \(K\) klózhalmazból, akkor \(K\)-ban van legalább egy egységklóz.

Biz: Az \(\square\)-t mint rezolvenst egy centrális regységklózból és egy klózhalmazbeli klózból kapjuk. Egy utóbbi csak egységklóz lehet.

Horn Logika - Egységklóz tétel

Kielégíthetetlen Horn klózhalmazban van legalább egy egységklóz.