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

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

    Лема 1. Нека Δ е множество от дизюнкти в дадена сигнатура, съдържаща поне една константа, Δ не притежава модел и Δ° е множеството на всички затворени частни случаи на дизюнкти от Δ.. Тогава празният дизюнкт е просто резолвентно изводим от от Δ°.

    Доказателство. Множеството Δ° е неизпълнимо. И наистина, да допуснем, че съществува структура S, в която са верни всички дизюнкти от Δ°. При това положение празният дизюнкт не може да принадлежи на Δ°, а следователно  –  и на Δ. За всеки дизюнкт от Δ да образуваме дизюнкция на неговите елементи и да означим с Γ множеството на така образуваните дизюнкции. Разбира се Γ е множество от безкванторни формули. Нека Γ° е множеството на всички затворени частни случаи на формули от Γ. Очевидно всяка формула от Γ° е дизюнкция, на която множеството на членовете е дизюнкт от Δ°. Следователно всички формули от Γ° са верни в структурата S и значи множеството Γ° е изпълнимо. Оттук обаче можем да заключим, че множеството Γ има модел, а това е невъзможно, защото всеки модел на Γ би бил модел и на Δ. С това показахме, неизпълнимостта на множеството Δ°, а тя позволява да заключим, че от това множество е просто резолвентно изводим празният дизюнкт.  □

    Лема 2. Нека Δ и Δ° са такива множества от дизюнкти, че всеки дизюнкт от Δ° е частен случай на някой дизюнкт от Δ и от множеството Δ° е просто резолвентно изводим празният дизюнкт. Тогава празният дизюнкт е резолвентно изводим от Δ.

    Доказателство. Достатъчно е да докажем, че всеки дизюнкт, просто резолвентно изводим от Δ°, притежава свойството да е частен случай на някой дизюнкт, който е резолвентно изводим от Δ. Наличието на това свойство за всички дизюнкти, просто резолвентно изводими от Δ°, обаче е ясно от наличието му за дизюнктите от Δ° и от неговото запазване при образуване на непосредствена резолвента.  □

    Теорема (теорема за пълнота на метода на резолюцията). Нека Δ е произволно множество от дизюнкти, което не притежава модел. Тогава празният дизюнкт е резолвентно изводим от Δ.

    Доказателство. Ще разгледаме поотделно случая, когато подразбираната в теоремата сигнатура има поне една константа, и случая, когато тя няма нито една. В първия от тези случаи заключението на теоремата се получава направо от двете леми по-горе. Във втория от тях, за да можем да приложим лема 1, ние ще разширим сигнатурата чрез добавяне на една константа. Нека дадената сигнатура е Σ, а Σ′ е сигнатурата, получена от нея чрез добавяне на една константа α. Предположението на теоремата е, че Δ. няма модел като множество от дизюнкти в сигнатура Σ, но това очевидно гарантира, че Δ. няма модел и като множество от дизюнкти в сигнатура Σ′. Следователно (по лема 1) празният дизюнкт е просто резолвентно изводим от множеството Δ° на онези затворени дизюнкти в сигнатура Σ′, които са частни случаи на дизюнкти от Δ. За да заключим оттук, че празният дизюнкт е резолвентно изводим от Δ в сигнатурата Σ, ще използваме едно преобразуване, което на всеки затворен дизюнкт D в сигнатура Σ′ съпоставя дизюнкт #D в сигнатура Σ. Грубо казано, преобразуването се състои в повсеместно заместване на константата α с една и съща променлива ξ. Точно описание на пробразуването ще дадем, като преди това последователно дефинираме аналогично преобразуване на затворени термове и затворени литерали. А именно, най-напред на всеки затворен терм τ в сигнатура Σ′ съпоставяме терм #τ в сигнатура Σ, като полагаме #α = ξ и приемаме, че

#ω(τ1,…,τm) = ω(#τ1,…,#τm)
при всеки избор на положително цяло число m, на m-местен функционален символ ω на Σ и на затворени термове τ1, …, τm в сигнатура Σ′, а след това на всеки затворен литерал λ в сигнатура Σ′ съпоставяме литерал #λ в сигнатура Σ, като полагаме #π = π, #¬π = ¬π за всеки нулместен предикатен символ π на Σ и приемаме, че
#π(τ1,…,τm) = π(#τ1,…,#τm),    #¬π(τ1,…,τm) = ¬π(#τ1,…,#τm)
при всеки избор на положително цяло число m, на m-местен предикатен символ π на Σ и на затворени термове τ1, …, τm в сигнатура Σ′. Нужното ни преобразуване на дизюнкти дефинираме, като положим
#D = { #λ | λ∈D }
за всеки затворен дизюнкт D в сигнатура Σ′. Нека #Δ° е множеството на всички дизюнкти #D, съответни на дизюнкти D от Δ°. Ще покажем, че са в сила следните две твърдения, от които теоремата следва веднага с помощта на лема 2:
    (а) в сигнатура Σ всеки дизюнкт от #Δ° е частен случай на някой дизюнкт от Δ;
    (б) празният дизюнкт е просто резолвентно изводим от #Δ°.
Верността на твърдението (а) се установява, като най-напред се докаже (чрез индукция относно построението на τ), че за всеки терм τ в сигнатура Σ, всяка n-ка от различни помежду си променливи ξ1, …, ξn, измежду които са променливите на τ, и всяка n-ка θ1, …, θn от затворени термове в сигнатура Σ′ имаме равенството
#[ξ1/θ1,…,ξn/θn]τ = [ξ1/#θ1,…,ξn/#θn]τ,
след което доказаното се използва, за да се получат аналогични твърдения за литерали в сигнатура Σ и за дизюнкти в тази сигнатура. За да се убедим пък във верността на твърдението (б), показваме, че за всеки затворен дизюнкт D, който е просто резолвентно изводим от Δ°, съответният дизюнкт #D е просто резолвентно изводим от #Δ°. За целта е е достатъчно да покажем, че преобразуването # запазва непосредствените резолвенти, т.е. винаги, когато един затворен дизюнкт D в сигнатура Σ′ е непосредствена резолвента на два затворени дизюнкта D1 и D2 в тази сигнатура, дизюнктът #D е непосредствена резолвента на дизюнктите #D1 и #D2  –  ясно е, че тогава за всеки дизюнкт D, който е просто резолвентно изводим от множеството Δ°, съответният дизюнкт #D, ще бъде просто резолвентно изводим от множеството #Δ°. Изказаното твърдение за запазване на непосредствените резолвенти се обосновава лесно, като се използва обстоятелството, че на всеки два различни литерала в сигнатура Σ′ преобразуването # съпоставя различни литерали, а това следва от лесно доказуемия факт, че [ξ/α]#λ = λ за всеки затворен литерал λ в сигнатура Σ′ (за да се докаже въпросният факт, първо се установява аналогично твърдение за затворените термове в същата сигнатура).  □

    Има по-прецизни версии на метода на резолюцията, при които са наложени допълнителни изисквания как да се образуват резолвенти и въпреки това е в сила теорема за пълнота. При спазване на въпросните изисквания използването на метода обикновено е по-удобно, отколкото ако работим без тях. За да опишем една такава версия, ще въведем понятие за резолвента на два дизюнкта по техни непразни подмножества. А именно, ако D1 и D2 са два дизюнкта, а E1 и E2 са непразни подмножества съответно на D1 и на D2, то под резолвента на D1 и D2 по E1 и E2 ще разбираме дизюнкт от вида

(σ1D1 \ {λ1}) ∪ (σ2D2 \ {λ2}),
където λ1 и λ2 са противоположни литерали, а σ1 и σ2 са такива субституции, че
Ei = {λ∈Di | σiλ = λi},   i = 1, 2.
(очевидно всеки такъв дизюнкт е резолвента на D1 и D2 в досегашния смисъл и всяка резолвента на D1 и D2 в досегашния смисъл е тяхна резолвента по подходящо избрани техни непразни подмножества).

    Пример 1. Нека

D1 = {p(a,y,z),p(x,b,z),p(x,y,c)},   D2 = {¬p(x,b,c),¬p(a,y,c),¬p(a,b,z)}
където p е триместен предикатен символ, а a, b и c са константи. Тъй като субституцията [x/a,y/b,z/c] преобразува всички елементи на D1 във формулата p(a,b,c), а всички елементи на D2  –  в нейното отрицание, виждаме, използвайки тази субституция в качеството и на σ1, и на σ2, че празният дизюнкт е резолвента на D1 и D2 по самите тях. Ако пък използваме в качеството на σ1 субституцията [x/a,y/b], а в качеството на σ2  –  тъждествената субституция, виждаме, че дизюнктът
{p(a,b,c),¬p(x,b,c),¬p(a,y,c)}
е резолвента на D1 и D2 по техните подмножества {p(a,y,z),p(x,b,z)} и {¬p(a,b,z)}. И дизюнктът
{p(a,b,c),¬p(z,b,c),¬p(a,z,c)}
е резолвента на D1 и D2 по същите техни подмножества. Това се вижда при σ2=[x/z,y/z] и същия избор на σ1.

    Ако D1 и D2 са два дизюнкта, а E1 и E2 са непразни подмножества съответно на D1 и на D2, то под най-обща резолвента на D1 и D2 по E1 и E2 ще разбираме такава резолвента D на D1 и D2 по E1 и E2, че всяка резолвента на D1 и D2 по E1 и E2 да бъде частен случай на D.

    Пример 2. Нека D1 и D2 са същите както в пример 1. Лесно се вижда, че празният дизюнкт е единствената тяхна резолвента по самите тях и следователно той е тяхна най-обща резолвента по самите тях. От разгледаните там две резолвенти на D1 и D2 по техните подмножества {p(a,y,z),p(x,b,z)} и {¬p(a,b,z)} втората не е най-обща, защото първата не е неин частен случай, но може да се покаже, че първата е най-обща.

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

 

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