Съждителни формули. Съждителна резолюция.
Table of Contents

Дизюнкти

Дефиниции (литерали)

Булев литерал

Съждителна формула от вида $p$, или $\lnot p$.
С други думи - или съждителна променлива, или нейното отрицание.

Дуален литерал

Нека $L$ е литерал. Дефинираме:

(1)
\begin{align} L^\partial \rightleftharpoons \begin{cases} \lnot p & L = p \\ p & L = \lnot p \end{cases} \end{align}

Това е просто отрицанието на $L$, само че ако станат две отрицания се разкарват. Може да запишем $L^\partial |\overset{b}=| \lnot L$.

Контрарна двойка литерали

Литералите $L, L^\partial$ ще наричаме контрарна двойка литерали.

Дефиниция (елементарна дизюнкция)

Формула от вида $\varphi = L_1 \lor L_2 \lor \dots \lor L_n$ където $n > 0$ и $L_i$ са булеви литерали, ще наричаме елементарна дизюнкция.

Твърдение (необходимо и достатъчно условие за булева тавтология)

Нека $\varphi$ е елементарна дизюнкция. Тогава $\varphi$ е булева тавтология, т.с.т.к. $\varphi$ съдържа поне една контрарна двойка литерали.

Доказателство
$| \Rightarrow |$ Нека $\varphi$ е булева тавтология. Да допуснем, че $\varphi$ не съдържа контрарна двойка литерали. Да си образуваме следната булева интерпретация $I$ (целта ще бъде, да покажем, че $I[\varphi] = \mathrm{f}$, т.е че $I \nvDash \varphi$):

(2)
\begin{align} I(p) = \begin{cases} \mathrm{t} & \lnot p \mbox{ is in } \varphi \\ \mathrm{f} & p \mbox{ is in } \varphi \\ \mathrm{t} & p \mbox { and } \lnot p \mbox{ are not in } \varphi \\ \end{cases} \end{align}

Обърнете внимание, че дефиницията е валидна, защото няма контрарна двойка литерали - т.е няма как да се случим едновременно в първия и втория случай. Колкото до третия случай - няма никакво значение каква стойност даваме там (защото променливите не са от $\varphi$), но за пълнота трябва да дадем стойност на всички променливи.
Сега лесно се проверява, че всички литерали участващи в $\varphi$ имат стойност лъжа, следователно $I \nvDash \varphi$. Следователно и $\varphi$ не е булева тавтология. Противоречие. Следователно във $\varphi$ има поне една двойка контрарни литерали.
$| \Leftarrow |$ Нека във $\varphi$ има контрарна двойка литерали. Тогава при произволна булева интерпретация $I$ единия литерал от двойката винаги ще има стойност истина1. Следователно и $\varphi$ ще има стойност истина. Направихме това разсъждение за произволна интерпретация, следователно то е вярно за всяка, следователно $\varphi$ е булева тавтология.

Дефиниция (дизюнкт)

Дизюнкт ще наричаме крайно множество от литерали.

Дефиниция (празен дизюнкт)

Ще отбелязваме празния дизюнкт с $\blacksquare$.

Дефиниция (модел на дизюнкт)

Нека $D$ е дизюнкт, а $I$ е булева интерпретация. Тогава $I \models D \rightleftharpoons$ съществува $L \in D : I \models L$.
С други думи един дизюнкт има модел $I$, ако поне един от литералите му има стойност истина при $I$.

Обърнете внимание, че празният дизюнкт $\blacksquare$ е винаги неизпълним. Нарочно го бележим различно от $\varnothing$, защото $\varnothing$ означава и празното множество от формули, което е винаги изпълнимо.

Твърдение

Всяка съждителна формула е булево еквивалентна с формула, която е конюнкция от елементарни дизюнкции.
При това такава конюнкция от елементарни дизюнкции може да се намери алгоритмично.

Доказателство: Става дума за привеждане в конюнктивна нормална форма. Винаги може, и може да става автоматично :-)

Сега вече от произволна съждителна формула получаваме нормална конюнктивна форма - т.е конюнкция от елементарни дизюнкции, образуваме дизюнкта на всяка дизюнкция и така получихме множество от дизюнкти.

Дефиниция (модел на множество дизюнкти)

Нека $I$ е булева интерпретация и $S$ е множество от дизюнкти. Тогава $I \models S \rightleftharpoons$ за всеки дизюнкт $D \in S : I \models D$.

Съждителна резолюция

Дефиниция (съждителна резолюция)

Нека $D_1, D_2$ са дизюнкти, нека $L$ е литерал, казваме, че правилото за резолюция е приложимо към $D_1, D_2$ отностно $L$, ако $L \in D_1$ и $L ^ \partial \in D_2$. Отбелязваме $!\mathcal{R}_L(D_1, D_2)$ или само с $\mathcal{R}_L(D_1, D_2)$2.
А самото правило е $\mathcal{R}_L(D_1, D_2) \rightleftharpoons (D_1 \setminus \{ L \}) \bigcup (D_2 \setminus \{ L ^ \partial \})$.

Забелeжка

$! \mathcal{R}_L(D_1, D_2) \longleftrightarrow ! \mathcal{R}_{L^\partial}(D_2, D_1)$

Дефиниция (резолвента)

Нека $D$ е дизюнкт. Ще казваме, че $D$ е резолвента на $D_1, D_2$, ако съществува литерал $L$, такъв че $D = \mathcal{R}_L(D_1, D_2)$.

Забележка

Възможно е $L \in \mathcal{R}_L(D_1, D_2)$. Тъй като нямаме никакво ограничение от вида: $L \notin D_2$.

Твърдение (резолвентата не губи модели)

Нека $D_1, D_2$ са дизюнкти, а $D = \mathcal{R}_L(D_1, D_2)$, нека $I$ е модел за $D_1, D_2$, т.е $I \models \{D_1, D_2\}$. Тогава $I \models D$.

Доказателство:
Нека $L \in D_1$ и $L^\partial \in D_2$ и нека I е интерпретация ($I \models D_1$ и $I \models D_2$). Тогава за $L$ има 2 възможности: I е модел за този литерал или не.

1) $I \models L$.
От $I \models D_2$ следва, че можем да изберем литерал $M \in D_2$, такъв че $I \models M$.
Тъй като $I \models L$, то $I \nvDash L^\partial$, откъдето $M \in D_2 \setminus \{ L^\partial \} \subseteqq D$. Следователно $I \models D$. (1)

2) $I \nvDash L$.
От $I \models D_1$ следова, че съществува литерал $M \in D_1$, такъв че $I \models M$. Тогава $M \neq L$ и $M \in D_1 \setminus \{L\} \subseteqq D$, следователно $I \models D$. (2)

От (1) и (2) следва, че $I \models D$.

Дефиниция (резолютивен извод)

Резолютивен извод от множество от дизюнкти $S$ се нарича крайна редица от дизюнкти $D_1, D_2, \dots , D_n$, такава че всеки нейн член е от $S$ или е резолвента на два предходни члена.

Дефиниция (резолютивно изводим)

Казваме, че $D$ е резолютивно изводим от $S$, $S \overset{r}\vdash D$, ако съществува резолютивен извод $D_1, D_2, \dots , D_n$ от $S$, такъв че $D = D_n$.

Твърдение (резолютивния извод не губи модели)

Нека $I$ е модел за $S$ и $S \overset{r}\vdash D$. Тогава $I \models D$.

Доказателство:
Индукция по дължината на резолютивния извод(n). Тоест трябва да докажем, че ако $D_1, D_2, \dots , D_n$ е резлютивен извод от $S$, то $I \models \{ D_1, D_2, \dots , D_n \}$.
База на индукцията: n = 1
От $S \overset{r}\vdash D_1$ следва, че $D_1 \in S$, откъдето $I \models D_1$
Индукционна хипотеза: Нека за $\forall k \le n$ $I \models D_1, D_2, \dots , D_k$
Индукционна стъпка: Нека $D_1, D_2, \dots , D_{n+1}$ е произволен резолютивен извод от $S$. Тогава $D_1, D_2, \dots , D_n$ е резолютивен извод от $S$, за който прилагаме индукционната хипотеза, т.е получаваме $I \models \{ D_1, \dots, D_n \}$.
Сега да разгледаме двете възможности за $D_{n+1}$:
(1) $D_{n+1} \in S$. Следователно $I \models D_{n+1}$.
(2) $D_{n+1} = \mathcal{R}(D_{k_1}, D_{k_2})$, където $k_1, k_2 < n + 1$. Следователно и $I \models \{ D_{k_1}, D_{k_2} \}$. Използваме, че резолвентата не губи модели и получаваме $I \models D_{n+1}$.
От (1), (2) следва, че $I \models \{ D_1, \dots, D_{n+1} \}$.

Теорема (коректност на резолютивните изводи)

Ако $S \overset{r}\vdash \blacksquare$, то $S$ не e изпълнимо.

Доказателство:
Нека $S \overset{r}\vdash \blacksquare$, тогава има резолютивен извод от $S$ $D_1, D_2, \dots , D_n$, такъв че $D_n = \blacksquare$. Да допуснем, че $S$ е изпълнимо. Разглеждаме един модел $I \models S$, то тогава $I \models \blacksquare$, което е противоречие, тъй като празният дизюнкт няма модел, следователно $S$ не e изпълнимо.

Теорема (за пълнота на резолютивния извод)

$S \overset{r}\vdash \blacksquare \longleftrightarrow S$ е неизпълнимо.

В правата посока го доказахме в теоремата за коректност.
В обратната посока ще го докажем в следващата тема след като вземем малко материал, който да ни помогне в доказателството (трансверзали на фамилия от множества).

Бележка

Има алгоритъм, който по дадена крайна редица от дизюнкти разпознава дали тя е резолютивен извод от S, като за S предполагаме, че е ефективно разпознаваемо. Като елементите на тази редица са от S или са резолютивни изводи от предходни елементи от редицата.

Дефиниция (дървовиден резолютивен извод)

ДРИ( дървовиден резолютивен извод ) е крайно дърво с индекс на разклонение точно 2( накратко обърнато двоично дърво ) като на листата на дървото са написани дизюнкти, а на останалите е написана резолвентата на върховете, които наследяват.
1.bmp

Твърдение (еквивалентност на дървовиден и нормален резолютивен извод)

$S \overset{r}\vdash D \longleftrightarrow D$ е дървовидно резолютивно изводим от $S$.
Доказателство: Едно postfix обхождане на дървото (първо децата, после корена) ще създаде точно резолютивен извод за корена.
Обратно - ако имаме дървовиден резолютивен извод за всички върхове освен корена (т.е правим индукция по построението на дървото), то ако сме от $S$ просто добавяме ново листо, иначе свързваме двете дървета с корени - двата дизюнкта на която новия е резолюция.

Дефиниция (S*)

Дефинираме индуктивно множествата $S_n$ по следния начин:
(1) $S_0 = S$
(2) $S_{n+1} = S_n \cup \{ D\ |\ \exists D_1, D_2 \in S_n \mbox{ and } D = \mathcal{R}(D_1, D_2) \}$
Дефинираме

(3)
\begin{align} S^* = \bigcup_{n=0}^{\infty} S_n \end{align}

Твърдение (връзка между S* и резолютивна изводимост)

Нека $S$ е множество от дизюнкти, тогава за всеки дизюнкт $D$ е изпълнено: $S \overset{r}\vdash D \longleftrightarrow D \in S^*$.

Доказателство:
$|\Rightarrow|$ Ще докажем нещо по-силно - ако $D_1, D_2, \dots, D_k$ е резолютивен извод от $S$, то $D_i \in S^*$ за $i = \overline{1,k}$.
Провеждаме индукция по $k$:
База на индукцията: $k = 1$. Ако $D_1$ е резолютивен извод от $S$, то $D_1 \in S$, защото няма как да е резолвента на два предходни члена, следователно $D_1 \in S = S_0 \subseteq S^*$.
Индукционна хипотеза: Нека твърдението е изпълнено за $k$.
Индукционна стъпка: Ще докажем, че е изпълнено при $k + 1$:
Разглеждаме произволен резолютивен извод от S - $D_1, D_2, \dots , D_{k+1}$. Съгласно индукционната хипотезата $D_i \in S^*$ за $i = \overline{1,k}$ $(\star)$. За $D_{k + 1}$ имаме две възможности: $D_{k + 1} \in S = S_0 \subseteq S^*$, с което твърдението е доказано, или $D_{k + 1} = \mathcal{R}(D_{i_1}, D_{i_2}),\ i_1, i_2 \le k, \ D_{i_1}, D_{i_2} \overset{(\star)}\in S^*$. Сега използваме дефиницията на $S^*$ и заключаваме, че съществуват $n_1, n_2$, такива че $D_{i_1} \in S_{n_1}$ и $D_{i_2} \in S_{n_2}$.
Нека $n = \max( n_1, n_2 )$, тогава $D_{i_1}, D_{i_2} \in S_n$, от където $D_{k+1} = \mathcal{R}(D_{i_1}, D_{i_2}) \in S_{n+1}$. Следователно $D_{k+1} \in S^*$.

$|\Leftarrow|$ Нека $D \in S^*$. Следователно съществува $n$ за което $D \in S_n$. Ще докажем с индукция по $n$, че от това следва $S \overset{r}\vdash D$.
База на индукцията $n = 0, \quad D \in S_0$, но $S_0 = S \rightarrow D \in S \rightarrow S \overset{r}\vdash D$.
Индукционна хипотеза Допускаме, че твърдението е изпълнено за всички числа до $n$ включително.
Индукционна стъпка Ще докажем твърдението за $n + 1$.
Нека $D \in S_{n+1}$. Има два начина, по които това може да стане:
(1) $D \in S_n$. Прилагаме индукционната хипотеза и сме готови.
(2) $D = \mathcal{R}(D_1, D_2)$, където $D_1, D_2 \in S_n$. Прилагайки индукционната хипотеза за $D_1, D_2$ получаваме $S \overset{r}\vdash D_1, D_2$. От тук следва, че съществуват резолютивни изводи $\alpha, \beta$ с последни членове съответно $D_1, D_2$3. Сега остава да се уверим, че редицата $\alpha\beta D$ е редица, която е резолютивен извод за $D$ от $S$, т.е. $S \overset{r}\vdash D$.

Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-NonCommercial-ShareAlike 3.0 License