Теорема за пълнота на на резолюцията на положителни елементарни конюнкции с положителни хорнови клаузи. Нека Γ е произволно множество от положителни хорнови клаузи. Ако дадена положителна елементарна конюнкция  Q  е изпълнима във всеки модел за Γ, то съществува резолвентна редица относно Γ, започваща с  Q  и завършваща с празната конюнкция.

      Доказателство. Нека  Q  е положителна елементарна конюнкция, която е изпълнима във всеки модел за Γ. Ще докажем, че съществува резолвентна редица относно Γ, започваща с  Q  и завършваща с празната конюнкция. Това е очевидно, ако  Q  е празната конюнкция, затова да предположим, че  Q  не е празната конюнкция. Ще използваме обстоятелството, че  Q  има затворен частен случай  Q ^o,  на който всеки от членовете е изводим от Γ (знаем това от въпроса за минимален ербранов модел за множество от положителни хорнови клаузи). Разбира се конюнкцията  Q ^o  също не е празна.

      Както направихме преди време в дефиницията за изводимост от Γ, да означим с Γ^o множеството на затворените частни случаи на клаузите от Γ. Основната ни грижа ще бъде да докажем, че съществува резолвентна редица относно Γ^o, която започва с  Q ^o  и завършва с празната конюнкция. Успеем ли да направим това, можем да завършим доказателството на теоремата, като в някоя такава редица заменим началния й член  Q ^o  с дадената конюнкция  Q   -  веднага се вижда, че получената по този начин редица ще бъде резолвентна редица относно Γ.

      За да докажем съществуването на резолвентна редица относно Γ^o, която започва с  Q ^o  и завършва с празната конюнкция, ще бъде удобно да въведем още някои спомагателни термини. Когато са дадени две затворени положителни елементарни конюнкции, ще казваме, че от първата е достижима втората, ако съществува резолвентна редица относно Γ^o, която започва с първата от двете конюнкции и завършва с втората (съвсем лесно се вижда, че така дефинираното отношение достижимост е транзитивно). Ще казваме, че една затворена атомарна формула A е отстранима, ако от всяка затворена положителна елементарна конюнкция с първи член A е достижима същата конюнкция без нейния пръв член. Ще докажем, че всяка затворена атомарна формула, изводима от Γ, е отстранима. Като имаме пред вид дефиницията за изводимост от Γ, достатъчно е да установим следните две свойства на отстранимостта:

        1. Атомарните формули, принадлежащи на Γ^o, са отстраними.

        2. Когато една клауза от Γ^o не е атомарна формула и всяка от предпоставките на тази клауза е отстранима, заключението на клаузата също е отстранимо.

      Свойството 1 се установява, като се забележи, че ако A е атомарна формула от Γ^o, то при всеки избор на затворени атомарни формули  C₁, …, C_n  двучленната редица с членове  A & C₁ & … & C_n  и  C₁ & … & C_n  е резолвентна редица относно Γ^o и следователно от първия й член е достижим вторият.

      За да установим свойството 2, да предположим, че една клауза от Γ^o е със заключение A и с ненулев брой предпоставки  B₁, …, B_m,  като всяка от тези предпоставки е отстранима. Тогава при всеки избор на затворени атомарни формули  C₁, …, C_n  двучленната редица с членове  A & C₁ & … & C_n  и  B₁ & … & B_m & C₁ & … & C_n  е резолвентна редица относно Γ^o и следователно от първия й член е достижим вторият. От друга страна от втория от тези два члена е достижима формулата  C₁ & … & C_n  поради отстранимостта на атомарните формули  B₁, …, B_m  (когато m е по-голямо от 1, използва се и транзитивността на достижимостта). Оттук и от транзитивността на достижимостта получаваме, че от формулата  A & C₁ & … & C_n  е достижима формулата  C₁ & … & C_n.

      От доказаното става ясно, че всеки от членовете на конюнкцията  Q ^o  е отстраним, а оттук (използвайки и транзитивността на изводимостта, когато броят на членовете е по-голям от 1) получаваме, че от тази конюнкция е достижима празната. _□

      По-нататък ние ще успеем да се освободим от предположението, че дадената сигнатура съдържа поне една константа (при това и заключението на теоремата ще бъде в значителна степен усилено). Засега ще направим една частична стъпка към освобождаване от въпросното предположение. За целта да се условим да казваме, че една сигнатура (Φ′,Π′,ρ′) е разширение на дадена сигнатура (Φ,Π,ρ), ако Φ′ и Π′ съдържат съответно Φ и Π като подмножества, а ρ′ е продължение на ρ (от дефиницията за сигнатура е ясно, че всяка сигнатура без константи притежава разширения, в които има константи).

      Лема. Нека Σ е произволна сигнатура, a Σ′ е разширение на Σ. Нека Γ и  Q  са съответно множество от безкванторни формули в Σ и безкванторна формула в Σ, като  Q  е изпълнима във всеки модел на Γ, който е структура със сигнатура Σ. Тогава  Q  е изпълнима във всеки модел на Γ, който е структура със сигнатура Σ′.

      Доказателство. Разбира се всички термове и формули в сигнатура Σ са съответно термове и формули и в сигнатура Σ′. Нека  S = (Σ′,D,I)  е произволен модел на Γ, който е структура със сигнатура Σ′. Разглеждаме структурата  S ^- = (Σ,D,I ^-),  където I ^- е рестрикцията на I върху множеството на функционалните и предикатните символи на Σ. Ако v е произволно изображение на множеството на променливите в множеството D, индуктивно се показва, че за всеки терм в сигнатура Σ стойността му в S ^- при оценката v съвпада със стойността му в S при оценката v. Като се използва това, индуктивно се доказва аналогично твърдение и за всяка безкванторна формула в сигнатура Σ. Следователно онези безкванторни формули в сигнатура Σ, които са тъждествено верни или изпълними в едната от структурите S и S ^-, са съответно тъждествено верни или изпълними и в другата. Понеже S е модел за Γ, формулите от Γ са тъждествено верни в S и следователно са тъждествено верни и в S ^-, т.е. S ^- също е модел за Γ. Предположенията на лемата дават тогава, че формулата  Q  е изпълнима в S ^-, следователно тя е изпълнима и в структурата S. _□

      На пръв поглед горната лема позволява да се освободим от предположението за наличие на поне една константа в дадената сигнатура, като при липса на такава константа приложим доказаната теорема за пълнота към някое разширение на сигнатурата, съдържащо константа. За съжаление резултатът, който се получава по този начин, е по-слаб от онова, което бихме желали. А именно, получава се заключение за съществуване на резолвентна редица относно Γ, започваща с  Q  и завършваща с празната конюнкция, на която редица обаче някои други от членовете може да не са формули в първоначалната сигнатура. Ще се справим с тази трудност едва по-късно, като използваме лемата по аналогичен начин, но за освобождаване от споменатото предположение в една значително по-прецизна форма на теоремата за пълнота.
 

Последно изменение: 3.06.2004 г.
 

Previous  Next  Contents