| Съдържание |
В основата на метода лежи следното твърдение.
Теорема на Дейвис и Пътнам. Нека Δ е дадено множество от затворени дизюнкти, φ е дадена затворена атомарна формула, участваща в Δ, а Δ′ е резултатът от елиминацията на φ в Δ.За да бъде множеството Δ изпълнимо, необходимо и достатъчно е да е изпълнимо множеството Δ′.
Доказателство. От дефиницията на множеството Δ′ е ясно, че всеки елемент на това множество е елемент на Δ или е непосредствена резолвента на някои два елемента на Δ. Поради това всеки модел за Δ е модел и за Δ′. Значи ако Δ е изпълнимо, то и Δ′ е изпълнимо. За да докажем обратното твърдение на това, да предположим, че множеството Δ′ е изпълнимо. Нека S е някой модел за Δ′. Нека множествата Δ0, Δ1 и Δ2 са определени както в дадената преди малко дефиниция. С допускане на противното се показва, че за всеки дизюнкт δ1 от Δ1 дизюнктът δ1\{φ} е валиден в S или за всеки дизюнкт δ2 от Δ2 дизюнктът δ2\{¬φ} е валиден в S. И наистина, ако допуснем противното, получаваме, че в S не е валиден някой дизюнкт от вида (δ1\{φ})∪(δ2\{¬φ}), където δ1 принадлежи на Δ1, а δ2 – на Δ2, но това противоречи на предположението, че S е модел за Δ′.
Случай 1. Нека за всеки дизюнкт δ1 от Δ1 дизюнктът δ1\{φ} е валиден в S. Да означим с S° такава структура, че в нея сред затворените атомарни формули са верни точно онези, които са различни от φ и са верни в S. Структура S°, удовлетворяваща това изискване, съществува – ако в сигнатурата има поне една константа, това следва от втората основна лема за ербрановите структури (вж. текста „Ербранови структури“), а в противен случай можем да използваме забележката след споменатата лема. Ще покажем, че S° е модел за множеството Δ. За целта да разгледаме произволен дизюнкт δ от Δ. Ако на този дизюнкт принадлежи литералът ¬φ, дизюнктът ще бъде валиден в S°, тъй като литералът ¬φ е верен в S°. Да предположим сега, че ¬φ не принадлежи на δ. Ако на δ принадлежи φ, то δ е от множеството Δ1, следователно той е валиден в структурата S, т.е. някой литерал от δ\{φ} е верен в S, а значи и в S° (тъй като стойността на този литерал в S° е същата както в S) – значи дизюнктът δ пак е валиден в S°. Ако пък на δ не принадлежи и литералът φ, то δ е от множеството Δ0, а значи и от множеството Δ′, следователно някой литерал от δ е верен в S, а значи и в S° (тъй като стойността на този литерал в S° отново е същата както в S) – отново дизюнктът δ се оказва валиден в S°.
Случай 2. Нека за всеки дизюнкт δ2 от Δ2 дизюнктът δ2\{¬φ} е валиден в S. Да означим с S° такава структура, че множеството на верните в нея затворени атомарни формули се състои от φ и всички затворени атомарни формули, верни в S. Съществуването на структура S°, удовлетворяваща това изискване, отново се вижда с помощта на втората основна лема за ербрановите структури и на забележката след нея. Ще покажем, че S° е модел за множеството Δ. Нека δ е произволен дизюнкт от Δ. Ако на този дизюнкт принадлежи атомарната формула φ, дизюнктът ще бъде валиден в S°, тъй като φ е вярна в S°. Да предположим сега, че φ не принадлежи на δ. Ако на δ принадлежи ¬φ, то δ е от множеството Δ2, следователно някой литерал от δ\{¬φ} е верен в S, а значи и в S° (тъй като стойността на този литерал в S° е същата както в S) – значи дизюнктът δ пак е валиден в S°. Ако пък на δ не принадлежи и литералът ¬φ, то δ е от множеството Δ0 и можем да разсъждаваме по същия начин както в случая 1. □
Когато е дадено едно множество Δ от дизюнкти, за един дизюнкт δ от това множество ще казваме, че е тривиално излишен за Δ, ако δ е тавтологичен или някое същинско подмножество на δ също принадлежи на Δ. За едно множество от дизюнкти Δ′ ще казваме, че е получено от Δ чрез прочистване, ако Δ′ е същинско подмножество на Δ и всички дизюнкти от Δ, които не принадлежат на Δ′, са тривиално излишни за Δ. Лесно е да се види, че когато Δ′ е получено от Δ чрез прочистване, множествата Δ′ и Δ имат едни и същи модели (това следва от обстоятелството, че за всеки нетавтологичен дизюнкт от Δ съществува съдържащ се в него дизюнкт от Δ, който не е тривиално излишен за Δ).
Методът на Дейвис и Пътнам може да бъде описан по следния начин. Дадено е едно крайно множество Δ от затворени дизюнкти. За да проверим дали то е изпълнимо, образуваме последователно крайни множества от затворени дизюнкти, първото от които е Δ, а всяко следващо се получава от предходното чрез елиминация или прочистване. Тъй като изпълнимостта на кое да е от тях е равносилна с изпълнимостта на Δ, ясно е, че ако някое от тях е празно, то множеството Δ е изпълнимо, а ако на някое от тях принадлежи празният дизюнктм, то Δ е неизпълнимо. От друга страна е сигурно, че ако продължим достатъчно дълго процеса на образуване на такива множества, то непременно ще получим множество, за което е налице някой от тези два случая. Това е така, защото ако за едно множество от затворени дизюнкти нямаме никой от двата случая, то към него може да се приложи поне операцията елиминация, като в случая на крайно множество от дизюнкти операцията елиминация намалява броя на елементите на обединението на дизюнктите от множеството, а пък операцията прочистване, неувеличавайки този брой, намалява броя на дизюнктите в множеството.
Забележка. Като използваме опростен вариант на горните разсъждения, виждаме, че при прилагането на метода на Дейвис и Пътнам може да се мине и без да се извършва прочистване. В някои случаи обаче това може да увеличи доста обема на работата.
Ще дадем няколко примера за прилагане на метода на Дейвис и Пътнам.
Пример 1. Нека φ, ψ и θ са три различни затворени атомарни формули, а Δ е множеството, състоящо се от следните шест дизюнкта:
| Δ0 = | {{ψ,θ}, {¬ψ,¬θ}}, |
| Δ1 = | {{φ,ψ}, {φ,θ}}, |
| Δ2 = | {{¬φ,¬ψ}, {¬φ,¬θ}}. |
Пример 2. Нека пак φ, ψ и θ са три различни затворени атомарни формули, но Δ да е множеството, състоящо се от следните четири дизюнкта:
Пример 3. Ще изследваме дали има модел множеството от следните два дизюнкта, където a и b са константи, а p е двуместен предикатен символ:
Пример 4. В предходния пример успяхме да приложим метода на Дейвис и Пътнам без да прибегнем нито веднъж до образуване на резолвента. При друга последователност на елиминиране на атомарните формули можеше и да не е така. Нека например ги елиминраме в следния ред: p(a,a), p(b,b), p(a,b), p(b,a). Тогава при първите две елиминации ще се извърши и резолюция. Последователно получаваните множества ще бъдат
Последно изменение: 21.05.2010 г.