Хорнови дизюнкти

Хорнови дизюнкти.

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

Дизюнктът $D$ наричаме Хорнов, ако най - много един от неговите литерали е позитивен.

  • $\blacksquare$ е Хорнов дизюнкт;
  • $\{p\}$ е Хорнов дизюнкт - факт;
  • $\{p, \lnot{q_1}, \dots , \lnot{q_n}\}, n > 0$ е Хорнов дизюнкт - правило;
  • $\{\lnot{q_1}, \dots , \lnot{q_m}\}, m > 0$ е Хорнов дизюнкт - цел.

Дефиниция (програма).

Ако едно множество от Хорнови дизюнкти съдържа само факти и правила, ще го наричаме програма( хорнова програма ).

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

Нека $S$ е неизпълнимо множество от хорнови дизюнкти и $\blacksquare \not \in S$ . Тогава $S$ съдържа поне един факт и поне една цел.

Доказателство:

Допускаме, че $S$ не съдържа факти. Нека $D \in S, S \ne \emptyset$ е цел или правило , тогава в $D$ има най-много един позитивен литерал. Тогава същетстува $q$, такова че $\lnot q \in D$.
Нека разгледаме следната интерпретация: $I_{false}[p] = f$ ( винаги дава оценка лъжа ), тогава за всяка променлива $p \ \Rightarrow \ I_{false} \models \lnot p$. От това, че в $D$ има поне един непозитивен литерал следва, че $I_{false} \models D \ \ \Rightarrow \ \ I_{false} \models S$, но това е противоречие с изпълнимостта на $S$, тоест допускането ни, че $S$ не съдържа факти е грешно.

Допускаме, че $S$ не съдържа цели. Тогава $D \in S, D$ е факт или правило, следователно съдържа поне един позитивен литерал. Разглеждаме интерпретацията $I_{true}[p] = t$, тогава получаваме, че $I_{true} \models D \ \ \Rightarrow \ \ I_{true} \models S$, което е противоречие, следователно $S$ съдържа поне една цел. с.к.т.д.

Следствие (изпълнимост на хорнова програма)

Всяка хорнова програма е изпълнима.

Дефиниция (сечение на множество Хорнови модели)

Нека $S$ е множество от хорнови дизюнкти и $X$ е множество от модели на $S$. Дефинираме си следната булева интерпретация $I_X$:
$I_X[p] = t \leftrightarrow$ за всяка интерпретация $J \in X, J[p]=t$, за всяка променлива $p$.

Лема (сечение на множество Хорнови модели е модел)

Нека $S$ е множество от хорнови дизюнкти и $X$ е множество от модели на $S$. Нека $X \neq \varnothing$. Тогава $I_X \models S$.

Доказателство:
Ако $J$ е една булева интерпретация, то на $J$ може да съпоставим множеството $A_J$ на всички променливи, верни в $J$: $A_J = \{p | J[p] = t\}$. И обратно, на всяко подмножество от съждителни променливи $А$, може да съпоставим булева интерпретация $J_A[p] = t \leftrightarrow p \in A$.
Така за $I_X$ получаваме
$I_X[p] = t \leftrightarrow p \in A_{I_X}$
$\leftrightarrow$ за всяка интерпретация $J \in X, J[p] = t$
$\leftrightarrow$ за всяка интерпретация $J \in X, p \in A_J$
$\leftrightarrow p \in \bigcap_{J \in X} A_J$
Тоест $A_{I_X} = \cap_{J \in X} A_J$. $I_X$ е "сечение" на интерпретациите от $X$.

Сега същинското доказателство на лемата:
Нека $D \in S$, тогава $D \neq \blacksquare$. Да разгледаме следните случаи за $D$:

  1. $D = \{p\}$ е факт
    Нека $J \in X$ тогава $J \models S, J \models {p}, J[p] = t$ следователно за всички $J \in X, J[p] = t \rightarrow I_X[p] = t$. Следователно и $I_X \models D$
  2. $D = \{\neg q_1,...,\neg q_n\}$ е цел, $n > 0$
    Нека $J \in X$ е модел за $D$. Тогава съществува $q_i : J[q_i] = \mathrm{f}$. От тук $q_i \notin A_J \rightarrow q_i \notin A_{I_X}$ следователно $I_X[q_i] = \mathrm{f}$, т.е. $I_X \models D$.
  3. $D = \{\neg q_1,...,\neg q_n,p\}$ е правило $n > 0$
    Ще разгледаме два случая
    1. $p$ е вярно във всички модели (аналогично на $D$ - факт), т.е. $p \in A_J$ за всяко $J$, следователно и $p \in A_{I_X}$, от където $I_X \models D$
    2. Съществува модел $J \in X$, за който $p$ не е вярно (аналогично на $D$ - цел), т.е. $p \notin A_J$. Тогава със сигурност съществува $q_i : J[q_i] = \mathrm{f}$. Следователно $q_i \notin A_J$. Тогава $q_i \notin A_{I_X}$, следователно $I_X[q_i] = \mathrm{f}$, от където следва, че $I_X \models D$.

Дефиниция (минимален модел)

Нека $S$ множество от булеви формули. Ако съществува модел $I_m \models S$, такъв че за всеки друг модел $I \models S$ е изпълнено $I_m[p] = \mathrm{t} \rightarrow I[p] = \mathrm{t}$ за всяка съждителна променлива $p$, ще наричаме $I_m$ минимален модел на $S$ (още известен като най-малък модел).

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

Нека $S$ е изпълнимо множество от Хорнови дизюнкти. Тогава $S$ има минимален модел $I_m$.

Доказателство: Нека $X$ е непразното множество от всички модели на $S$ : $X = \{ J\ |\ J \models S \} \neq \varnothing$. Не е трудно да се провери, че модела $I_X$ е минимален модел за $S$. Той е модел, от предната лема. От дефиницията на $I_X$ имаме, че ако $I_X[p] = \mathrm{t}$, то за всеки модел $J \in X$ е изпълнено $J[p] = \mathrm{t}$, но $X$ е множеството на всички модели за $S$, следователно от $I_X[p] = \mathrm{t}$ следва $J[p] = \mathrm{t}$, за всеки модел $J$ на $S$.

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