ПЪЛНОТА НА МЕТОДА НА РЕЗОЛЮЦИЯТА
ЗА МНОЖЕСТВА ОТ ЗАТВОРЕНИ ДИЗЮНКТИ

    Очевидно е, че ако два дизюнкта са затворени и даден дизюнкт е тяхна резолвента, той е тяхна непосредствена резолвента и също е затворен. Следователно, ако Δ е едно множество от затворени дизюнкти, то всеки дизюнкт, който е резолвентно изводим от Δ, може да бъде получен от дизюнкти, принадлежащи на Δ, чрез някакъв (евентуално нулев) брой образувания на непосредствена резолвента и също е затворен. Целта ни ще бъде докажем, че от всяко неизпълнимо множество от затворени дизюнкти е резолвентно изводим празният дизюнкт. Ще я постигнем с помощта на няколко леми.

    Лема 1. Нека Δ е множество от затворени дизюнкти, а D′ и D′′ са затворени дизюнкти. Ако от множеството Δ ∪ {D′} е резолвентно изводим празният дизюнкт, то от множеството Δ ∪ {D′′} е резолвентно изводим някой дизюнкт, който се съдържа в D′′ \ D′.

    Доказателство. Ще докажем по-общото твърдение, че ако от Δ ∪ {D′} е резолвентно изводим даден дизюнкт D, то от Δ ∪ {D′′} е резолвентно изводим някой дизюнкт, който се съдържа в D ∪ (D′′ \ D′). Свойството от заключението на това твърдение се проверява непосредствено в случая, когато D е дизюнкт, принадлежащ на множеството Δ ∪ {D′}  –  ако D принадлежи на Δ, то самият дизюнкт D е един дизюнкт, резолвентно изводим от Δ ∪ {D′′} и съдържащ се в D ∪ (D′′ \ D′), а ако D=D′, то такъв е дизюнктът D′′. При това положение е достатъчно да покажем още, че всеки път, когато един дизюнкт е непосредствена резолвента на два дизюнкта, резолвентно изводими от Δ ∪ {D′} и притежаващи въпросното свойство, той също притежава това свойство. Нека един дизюнкт D е непосредствена резолвента на два дизюнкта D1 и D2, резолвентно изводими от Δ ∪ {D′} и такива, че някои дизюнкти D1 и D2, резолвентно изводими от Δ ∪ {D′′}, се съдържат съответно в D1 ∪ (D′′ \ D′) и в D2 ∪ (D′′ \ D′). Имаме равенство

D = (D1 \ {λ1}) ∪ (D2 \ {λ2}),
където λ1 и λ2 са противоположни литерали, принадлежащи съответно на D1 и на D2. Ако λ1 не принадлежи на D1, то
D1 ⊆ (D1 \ {λ1}) ∪ (D′′ \ D′) ⊆ D ∪ (D′′ \ D′),
a ako λ2 не принадлежи на D2, то
D2 ⊆ (D2 \ {λ2}) ∪ (D′′ \ D′) ⊆ D ∪ (D′′ \ D′).
В случай пък, че λ1 принадлежи на D1 и λ2 принадлежи на D2, дизюнктът
(D1 \ {λ1}) ∪ (D2 \ {λ2})
е резолвента на D1 и D2 и се съдържа в D ∪ (D′′ \ D′). Следователно винаги е налице дизюнкт, който е резолвентно изводим от Δ ∪ {D′} и се съдържа в D ∪ (D′′ \ D′).  □

    Лема 2. Нека Δ е множество от затворени дизюнкти, D′ е затворен дизюнкт и D′′ е подмножество на D′. Ако от множеството Δ ∪ {D′} е резолвентно изводим празният дизюнкт, той е резолвентно изводим и от множеството Δ ∪ {D′′}.

    Доказателство. Използваме лема 1 и обстоятелството, че в случая множеството D′′ \ D′ е празно.  □

    Лема 3. Нека Δ е множество от затворени дизюнкти, а D1 и D2 са такива затворени дизюнкти, че празният дизюнкт е резолвентно изводим както от множеството Δ ∪ {D1}, така и от множеството Δ ∪ {D2}. Тогава той е резолвентно изводим и от множеството Δ ∪ {D1 ∪ D2}.

    Доказателство. Като приложим лема 1 при D′=D1 и D′′=D1 ∪ D2, виждаме. че съществува дизюнкт D, който е резолвентно изводим от множеството Δ ∪ {D1 ∪ D2} и се съдържа в D2. Прилагайки лема 2 при D′=D2 и D′′=D, заключаваме, че от множеството Δ ∪ {D} е резолвентно изводим празният дизюнкт. Значи в крайна сметка той е резолвентно изводим и от множеството Δ ∪ {D1 ∪ D2}.  □

    Лема 4. Нека Δ е множество от затворени дизюнкти, а D1, …, Dn, където n≥2, са такива затворени дизюнкти, че празният дизюнкт е резолвентно изводим от всяко от множествата Δ ∪ {Di}, i=1,…, n. Тогава той е резолвентно изводим и от множеството Δ ∪ {D1 ∪ … ∪ Dn}.

    Доказателство. Чрез индукция относно n.  □

    Теорема. Ако едно множество от затворени дизюнкти е неизпълнимо, то празният дизюнкт е изводим от това множество.

    Доказателство. Благодарение на теоремата за компактност за множества от затворени дизюнкти достатъчно е да докажем, че празният дизюнкт е резолвентно изводим от всяко неизпълнимо крайно множество от затворени дизюнкти. Разбира се можем да се ограничим с такива множества от дизюнкти, на които не принадлежи празният дизюнкт, защото за множествата, на които той принадлежи, твърдението е тривиално. Нека Δ е произволно неизпълнимо крайно множество от непразни затворени дизюнкти и нека m е броят на онези дизюнкти от Δ, които имат повече от един елемент. Ще си послужим с индукция относно m. Ако m=0, то всички дизюнкти от Δ са едноелементни и техните елементи образуват едно неизпълнимо множество от затворени литерали. Знаем, че сред елементите на такова множество има непременно два противоположни литерала. Очевидно едноелементните множества, съответни на тези литерали, са елементи на Δ, имащи празна резолвента, и значи празният дизюнкт е резолвентно изводим от Δ. Да предположим сега, че доказваното твърдение е в сила при m=k, където k е дадено естествено число, и е дадено неизпълнимо крайно множество Δ от непразни затворени дизюнкти, за което m=k+1. Нека λ1, …, λn са елементите на някой дизюнкт D от Δ, който е с повече от един елемент. Разглеждаме множествата

(Δ \ {D}) ∪ {λi},  i=1, …, n.
Всяко от тях е неизпълнимо, а дизюнктите в Δ \ {D}, които са с повече от един елемент, са k на брой. По индуктивното предположение празният дизюнкт е резолвентно изводим от всяко от множествата (Δ \ {D}) ∪ {λi}, а от друга страна обединението на едноелементните множества {λ1}, …, {λn} е D. По лема 4 празният дизюнкт е резолвентно изводим от множеството (Δ \ {D}) ∪ {D}, а то е точно множеството Δ.  □

 

Последно изменение във файла:  14 февруари 2008 г.