|
Table of Contents
|
Дизюнкти
Дефиниции (литерали)
Булев литерал
Съждителна формула от вида $p$, или $\lnot p$.
С други думи - или съждителна променлива, или нейното отрицание.
Коментар: Не съм сигурен в това колко е вярна тази дефиниция. Отрицание на променливи няма логика. Предполагам, че Литерал означава атомарна формула или
отрицание на атомарна формула.
Дуален литерал
Нека $L$ е литерал. Дефинираме:
(1)Това е просто отрицанието на $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$):
Обърнете внимание, че дефиницията е валидна, защото няма контрарна двойка литерали - т.е няма как да се случим едновременно в първия и втория случай. Колкото до третия случай - няма никакво значение каква стойност даваме там (защото променливите не са от $\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( накратко обърнато двоично дърво ) като на листата на дървото са написани дизюнкти, а на останалите е написана резолвентата на върховете, които наследяват.
Твърдение (еквивалентност на дървовиден и нормален резолютивен извод)
$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) \}$
Дефинираме
Твърдение (връзка между 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$.
