Записки по „Логическо програмиране“ за резолюции

Забележка 1. В тези записки структурите са обозначавани посредством удебелени латински букви вместо с курсив, за да бъде сигурно, че няма да възникнат неочаквани проблеми при изобразяването на текста на някои компютри.

Забележка 2. Ако читателят забележи питанки или празни квадратчета на неочаквани места, то е разумно той да бъде съмнителен относно достоверността на това, което вижда. Следва таблица, в която са поместени символите, за които най-често липсва поддръжка у системните шрифтове:

Ако дори един символ от горната таблица не е изобразен правилно, браузърът задължително трябва да се настрои използва шрифтове с достатъчен брой символи. Такива шрифтове могат да се свалят например от адрес http://www.gnu.org/software/freefont/. В краен случай може да се използва следният PDF-файл.

§1. Съществуване на минимална трансверзала

Да припомним, че ако F е фамилия от множества, то X е трансверзала за F, ако X има непразно сечение с всеки елемент на F.

Множество X е минимална трансверзала за F, ако:

1) X е трансверзала за F;

2) Ако Y е трансверзала за F и Y⊆X, то Y=X. Или с други думи никое същинско подмножество на X не е трансверзала за F.

Трябва да докажем следната

A) Теорема. Ако F е фамилия от непразни крайни множества, то съществува минимална трансверзала за F.

Най-напред да забележим, че за F има поне една трансверзала (не задължително минимална). Наистина, нека Y бъде множеството, което съдържа всички елементи на елементите на F. Тъй като елементите на F са непразни, то очевидно Y има непразно сечение с всеки елемент на F.

От тук нататък идеята на доказателството е следната. Започваме от Y и постепенно махаме елементи от Y по такъв начин, че множеството да остава трансверзала. Очевидно ако стигнем до момент, в който няма начин така да се махат още елементи, че множеството да остава трансверзала, то ще сме получили минимална трансверзала. Но за да можем да реализираме тази идея, трябва по някакъв начин да вземем предвид това, че фамилията F може би е безкрайна и поради това за да получим минимална трансверзала от Y, може да се наложи махнем безброй много елементи от Y.

По принцип ако първоначалната трансверзала Y е неизброиме множество, този безкраен процес на махане на елементи от Y става трансфинитен. За по-просто обаче, тук ще се ограничим със случая, когато множеството Y e изброимо. По принцип теорема (A) е вярна и в общия случай и при това доказателството не е съществено различно от даденото по-долу, но се налага да работим с ординални числа вместо с естествени числа и с трансфинитни редици вместо с обикновени редици.

И тъй, да си предствим един безкраен процес на махане на елементи от Y, при който получаваме следните множества:

Нека Y_∞ е сечението на всички тези множества. Вярно ли е, че това е трансверзала? За да можем да направим доказателство, използващо горната идея, имаме нужда това да бъде трансверзала. Затова изказваме следната

Б) Хипотеза. Нека е дадена фамилия F редица

от намаляващи трансверзали за F. Нека Y_∞ е сечението на всички тези трансверзали. Тогава Y_∞ е трансверзала за F.

Опровержение. За съжаление хипотезата ни не е вярна и това не е трудно да се забележи. Нека F съдържа само един елемент – множеството на естествените числа. И нека множествата Y₀,Y₁,Y₂,… са дефинирани така:

Тогава очевидно Y_i⊇Y_i+1 за всяко i и същевременно Y_i е трансверзала за F също за всяко i, но въпреки това сечението на всички тези трансверзали е празното множество, което очевидно не е трансверзала за F.

В) За щастие идеята ни може да бъде спасена. Вярна е следната

Лема. Нека F е фамилия от крайни множества и е дадена редица

от намаляващи трансверзали за F. Нека Y_∞ е сечението на всички тези трансверзали. Тогава Y_∞ е трансверзала за F.

Доказателство. Да изберем произволен елемент A на F. Трябва да покажем, че A и Y_∞ имат непразно сечение. Нека Z_i=A∩Y_i. Тъй като Y_i⊇Y_i+1, то Z_i⊇Z_i+1. От друга страна A е крайно, значи всички множества Z_i са крайни. Следователно получихме безкрайна редица от крайни намаляващи множества

Това е възможно само ако тази редица се стабилизира в даден момент, т.е. ако съществува такова естествено число n, че Z_i=Z_i+1 за всяко i≧n. Следователно горната редица всъщност изглежда така:

Тъй като Y_n е трансверзала, то Z_n е непразно. Нека b е произволен елемент на Z_n. Тъй като Z_i=A∩Y_i, то от една страна b принадлежи на A. От друга страна щом като b принадлежи на Z_n, то всъщност b принадлежи на всички множества Z_i и следователно b принадлежи на всички Y_i. Но щом като b принадлежи на всички Y_i, то b принадлежи на Y_∞. Следователно b∈A∩Y_∞ и значи A и Y_∞ имат непразно сечение.  □

Г) Доказателство на теорема (A). Най-напред да си припомним, че вече забелязахме, че за F има поне една трансверзала (не задължително минимална). Наистина, нека Y бъде множеството, което съдържа всички елементи на елементите на F. Тъй като елементите на F са непразни, то очевидно Y има непразно сечение с всеки елемент на F.

Да подредим елементите на Y в редица:

Ако Y е крайно, то тази редица е крайна, ако Y е изброимо безкрайно, то тази редица е обикновена безкрайна редица, а ако Y е неизброимо безкрайно, то тогава тази редица е трансфинитна.

Сега да дефинираме индуктивно редица от намаляващи трансверзали

Нека Y₀⇋Y. Тогава Y₀ е трансверзала, защото Y бе трансверзала. При произволно i ако няма начин да отстраним по такъв начин елемент от Y_i, че множеството да остане трансверзала, то нека Y_i+1⇋Y_i. В противен случай нека a_n бъде първият елемент на редицата a, който можем да отстраним от Y_i и множеството да остане трансверзала. Тогава нека Y_i+1⇋Y_i\{a_n}. Очевидно и в двата случая Y_i+1 се оказва трансверзала. Нека Y_∞ е сечението на всички тези трансверзали. Съгласно лема (В) Y_∞ е трансверзала. Ще докажем, че Y_∞ е минимална трансверзала.

Да изберем произволен елемент a_m на редицата a. Тъй като всички елементи на Y_∞ са измежду елементите на a, то ще бъде достатъчно да докажем, че Y_∞\{a_m} не е трансверзала. Затова нека допуснем противното, а именно че Y_∞\{a_m} е трансверзала. Тъй като Y_∞⊆Y_i за всяко i, то Y_i\{a_m} също е трансверзала за всяко i. Да си припомним обаче, че на всяка стъпка за да дефинираме Y_i+1 избирахме първия елемент a_n на редицата a, при който Y_i\{a_n} остава трансверзала. Но Y_i\{a_m} е трансверзала, следователно избраният елемент a_n предхожда a_m в редицата a.

Горните разсъждения показват, че при построението на трансверзалите Y₀,Y₁,Y₂,… на никоя стъпка не премахваме елемент на редицата a, който се намира след a_m. Но преди a_m има само краен брой елементи, следователно след краен брой стъпки трансверзалите Y_i се стабилизират, т.е. за някое естествено число k те изглеждат така:

Сега нужното противоречие получаваме по следния начин. От една страна Y_k=Y_k+1, следователно дефиницията на Y_k+1 влече, че който и елемент да махнем от Y_k, полученото множество няма да бъде трансверзала. От друга страна обаче ние вече знаем, че Y_k\{a_m} е трансверзала, а това е противоречие.

§2. Теорема за компактност за съждителното смятане. Теорема на Ербран

Да припомним следната

A) Дефиниция. (1) Казваме, че множество Γ от съждителни формули е булево изпълнимо, ако съществува такава булева интерпретация I, че всички елементи на Γ са верни при I.

(2) Казваме, че множество Γ от предикатни формули е изпълнимо, ако съществува структура, в която са верни всички формули от Γ. За тази структура казваме, че е модел на Γ.

(3) Казваме, че множество от съждителни формули е булево неизпълнимо, ако то не е булево изпълнимо.

(4) Казваме, че множество от затворени предикатни формули е неизпълнимо, ако то не е изпълнимо.

(5) Казваме, че съждителната формула φ следва булево от множество съждителни формули Γ, ако при всяка булева интерпретация, при която са верни елементите на Γ, формулата φ също е вярна.

(6) Казваме, че затворената предикатна формула φ следва булево от множество от предикатни формули Γ (пишем Γ⊨φ), ако при всяка структура, в която са верни елементите на Γ, формулата φ също е вярна в A.

Б) Теорема за компактност на съждителната логика. Множество Γ от съждителни формули е булево изпълнимо тогава и само тогава, когато всяко крайно подмножество Γ е булево изпълнимо.

Доказателство. (⇒) Очевидно ако Γ е булево изпълнимо, то всяко негово подмножество е булево изпълнимо.

(⇐) Да допуснем, че всяко крайно подмножесто на Γ е булево изпълнимо, но въпреки това самото множество Γ e булево неизпълнимо. За всяка формула φ от Γ съществува такова крайно множество Δ_φ от съждителни дизюнкти, че φ е булево еквивалентна на Δ_φ, т.е. ако φ е вярна при някаква булева интерпретация, то и формулите от Δ_φ са верни и обратно – ако формулите от Δ_φ са верни при някаква булева интерпретация, то и φ е вярна. Нека Γ' е обединението на всички тези множества Δ_φ. Тогава Γ' е булево еквивалентно на Γ и значи Γ' е булево неизпълнимо.

От теоремата за пълнота на съждителната резолютивна изводимост следва, че от Γ' можем да изведем ■ посредством съждителна резолюция. По дефиниция това означава, че съществува резолютивен извод

на ■ от Γ'. По дефиниция това означава, че:

1) D_n=■.
2) Всяко D_i или е елемент на Γ', или е непосредствена съждителна резолвента на дизюнкти, предхождащи D_i в резолютивния извод.

Нека Γ''⇋Γ'∩{D₀,D₁,D₃,…,D_n}. Очевидно Γ'' е крайно подмножество на Γ'. Освен това директно се проверява, че горният резолютивен извод на ■ от Γ' е също така и резолютивен извод на ■ от Γ''. По дефиниция това означава, че празният дизюнкт ■ е изводим посредством съждителна резолюция от Γ''. От теоремата за коректност на съждителната резолютивна изводимост следва, че Γ'' е булево неизпълнимо.

Нека Γ''⇋{D'₁,D'₂,…,D'_m}. Тъй като Γ' бе обединение на множествата Δ_φ, а Γ''⊆Γ', то за всеки от дизюнктите D'_i съществува такава формула φ_i, че D'_i∈Δ_φi.

Нека Γ'''⇋{φ₁,φ₂,…,φ_m}. Тъй като Γ''' е крайно подмножество на Γ, по условие Γ''' е булево изпълнимо. Нека I е интерпретация, при която всички формули от Γ''' са верни. От булевата еквивалентност на φ_i с Δ_φi следва, че всички дизюнкти, принадлежащи на множествата Δ_φi са верни при I. Но D'_i∈Δ_φi, следователно в частност дизюнктите D'_i са верни при I. Така намерихме интерпретация, при която са верни елементите на Γ'' са верни, значи Γ'' е булево изпълнимо, а ние знаем, че това не е така. Противоречие.  □

В) Да припомним, че ако множеството Γ съдържа затворени универсални формули, то с CSi(Γ) означаваме множеството от всички затворени частни случаи на формулите от Γ.

Структура A е модел за множество Γ от затворени формули, ако всяка формула от Γ е вярна в A. Множество Γ от затворени формули е изпълнимо, ако има модел. То е неизпълнимо, ако не е вярно, че е изпълнимо.

Г) Вече е доказана следната

Лема (малка теорема на Ербран). Нека Γ е множество от затворени универсални формули за език без формално равенство и с поне една индивидна константа. Тогава следните са еквивалентни:

(1) Γ има модел;

(2) Γ има Ербранов модел;

(3) CSi(Γ) има модел;

(4) CSi(Γ) е булево изпълнимо.

Д) Теорема на Ербран. Нека Γ е множество от затворени универсални формули за език без формално равенство и с поне една индивидна константа. Тогава Γ е неизпълнимо тогава и само тогава, когато съществува такова крайно множество Δ от затворени частни случаи на формули от Γ, че Δ е булево неизпълнимо.

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

(⇐) Нека Δ е такова крайно множество от затворени частни случаи на формули от Γ, че Δ е неизпълнимо. Тъй като Δ⊆CSi(Γ), то тогава CSi(Γ) също ще бъде булево неизпълнимо. От непосредствено цитираната лема следва, че множеството Γ няма модел, т.е. то е неизпълнимо.  □

Е) Теорема за компактност на предикатната логика, първи вариант. Множество Γ от предикатни формули е изпълнимо тогава и само тогава, когато всяко крайно подмножество Γ е изпълнимо.

Доказателство. (⇒) Тази посока е лесна и следва директно от дефинициите. Щом Γ е изпълнимо, то съществува структура A, в която са верни всички формули от Γ. Следователно в A ще са верни елементите на кое да е крайно подмножество на Γ и значи всички крайни подмножества на Γ са изпълними.

(⇐) Да допуснем, че множеството Γ не е изпълнимо.

Нека функцията f' е такава, че за всяка формула φ от Γ, f'(φ) е универсално затваряне на φ. Нека множеството Γ' се получава от Γ като заменим всяка формула φ от Γ с f'(φ). Тъй като всяка формула е еквивалентна на кое да е свое универсално затваряне, то Γ' е такова неизпълнимо множество от затворени формули, че всяко негово крайно подмножество е изпълнимо.

Нека функцията f'' е такава, че за всяка формула φ от Γ', f''(φ) е пренексна нормална форма на φ. Нека множеството Γ'' се получава от Γ' като заменим всяка формула φ от Γ' с f''(φ). Тъй като всяка формула е еквивалентна на коя да е своя пренексна нормална форма, то Γ'' е такова неизпълнимо множество от затворени пренексни формули, че всяко негово крайно подмножество е изпълнимо.

Нека функцията f''' е такава, че за всяка формула φ от Γ'', f'''(φ) е правилно извършена скулемизация на φ (т.е. няма конфликт на допълнително добавените индивидни константи и функционални символи). Нека множеството Γ''' се получава от Γ'' като заменим всяка формула φ от Γ'' с f'''(φ). Разбира се Γ'' е множество от универсални затворени формули. От вече доказана теорема следва, че Γ'' е неизпълнимо множество. От същата теорема следва още, че всяко крайно подмножество на Γ'' е изпълнимо.

От теоремата на Ербран следва, че има такова крайно булево неизпълнимо множество {ψ₁,ψ₂,…,ψ_k}, че елементите му са затворени частни случаи на елементи на Γ''. Нека за определеност ψ_i е частен случай на φ_i∈Γ'' и да дефинираме Δ⇋{φ₁,φ₂,…,φ_k}. Тъй като булево неизпълнимото множество {ψ₁,ψ₂,…,ψ_k} е подмножество на CSi(Δ), то CSi(Δ) е булево неизпълнимо. От от малката теорема на Ербран (Г) следва, че Δ е неизпълнимо. Така намерихме крайно неизпълнимо подмножество на Γ'', което е противоречие.  □

Ж) Теорема за компактност на предикатната логика, втори вариант. Множество Γ е неизпълнимо тогава и само тогава, когато съществува крайно подмножество на Γ, което е неизпълнимо.

Доказателство. Ще използваме, че вече сме доказали първия вариант на теоремата за компактност.

Γ е неизпълнимо ↔ не е вярно, че Γ е изпълнимо ↔ не е вярно, че всяко крайно подмножество на Γ е изпълнимо ↔ някое крайно подмножество на Γ е неизпълнимо.  □

И) Теорема за компактност на предикатната логика, трети вариант. Γ⊨φ тогава и само тогава, когато съществува такова крайно подмножество Δ на Γ, че Δ⊨φ.

Доказателство. (⇒) Нека ψ е универсално затваряне на φ. Тъй като φ и ψ са еквивалентни, то от една страна Γ⊨ψ, а от друга – ще бъде достатъчно да докажем, че съществува такова крайно подмножество Δ на Γ, че Δ⊨φ.

Тъй като Γ⊨ψ, то по дефиниция ψ е вярна във всяка структура, в която са верни формулите от Γ. Тъй като ψ е затворена, то ψ е невярна в дадена структура тогава и само тогава, когато ¬ψ е вярна в същата структура. Следователно не съществува структура, при която са верни формулите от Γ и формулата ¬ψ също е вярна. Значи множеството Γ∪{¬ψ} е неизпълнимо. Сега от втория вариант на теоремата за компактност следва, че съществува крайно множество Δ' на Γ∪{¬ψ}, което също е неизпълнимо. Нека Δ⇋Δ'∩Γ. Тъй като единственият елемент на Δ', който може да не е елемент на Γ е ¬ψ, то ¬ψ e единственият елемент на Δ', койтo може би не е елемент на Δ. Следователно Δ'⊆Δ∪{¬ψ} и значи Δ∪{¬ψ} е неизпълнимо. Това значи, че не съществува структура, в която са верни формулите от Δ, а формулата ψ да не е вярна. По дефиниция това означава, че Δ⊨ψ. Но Δ=Δ'∩Γ, значи Δ e крайно подмножество на Γ.

(⇐) Ако Δ⊨φ за някое подмножество Δ на Γ, то формулата φ е вярна във всички структури, в които са верни формулите от Δ. В частност φ e вярна във всички структури, в които са верни формулите от Γ, т.е. Γ⊨φ.  □

§3. Съждителна резолюция за предикатни дизюнкти

A) Основната причина, поради която досега се занимавахме със съждителната логика и със съждителната резолюция, бе да се подготвим по-добре за атака на основния случай – предикатния. Най-напред припомняне на някои дефиниции.

Дефиниция. (1) Предикатен литерал или просто литерал е атомарна формула или отрицание на атомарна формула.

(2) Предикатен дизюнкт или просто дизюнкт е крайно множество от литерали.

(3) Предикатен дизюнкт е верен в структура A при оценка v, ако поне един литералите на дизюнкта е верен в структурата A при оценка v.

(4) Предикатен дизюнкт е верен в структура A, ако той е верен в A при произволна оценка.

(5) Предикатен дизюнкт е затворен, ако всичките му литерали са затворени (т.е. не съдържат променливи, защото в литералите не може да има свързани променливи).

(6) Предикатен дизюнкт е изпълним, ако е верен в поне една структура. Той е неизпълним, ако не е изпълним. Множество от предикатни дизюнкти е изпълнимо, ако съществува структура, в която се верни всички дизюнкти от множеството. То е неизпълнимо, ако не е изпълнимо.

(7) Предикатен дизюнкт е тавтологичен, ако е верен в произволна структура. Съгласно (4) това означава, че той е верен в произволна структура при произволна оценка.

(8) Празният дизюнкт е дизюнктът, който съдържа нула на брой литерали и се означава с ■.

(9) Ако литералът L е атомарна формула, то ¬L също е литерал. Литералът ¬L е дуален на L, a литералът L – дуален на ¬L. Дуалният литерал се обозначава с надреден знак ^∂. Например ако L е атомарна формула, то L^∂=¬L и (¬L)^∂=L.

(10) Ако Γ е множество от литерали, с Γ^∂ ще обозначаваме множеството от всички литерали, които са дуални на елементите на Γ.

(11) Елементарна дизюнкция е дизюнкция на литерали (един или повече). За всяка елементарна дизюнкция φ=L₁⋁L₂⋁…⋁L_n с D_φ означаваме дизюнкта {L₁,L₂,…,L_n}. Директно от дефинициите следва, че φ e вярна в структура A тогава и само тогава, когато D_φ е верен в A и φ е вярна в структура A при оценка v тогава и само тогава, когато D_φ е верен в структурата A при оценка v.

Б) Твърдение. Празният дизюнкт е единственият неизпълним предикатен дизюнкт. Всички останали предикатни дизюнкти са изпълними.

Доказателство. Празният дизюнкт е неизпълним, защото не е възможно да съдържа верен литерал без значение какви са структурата и оценката. Нека D не е празен дизюнкт и L е литерал от D. Ще разгледаме два случая в зависимост от това дали L е атомарна формула или отрицание на атомарна формула.

Ако L е атомарна формула, нека L=p(τ₁,…,τ_n), където p е предикатен символ, а τ₁,…,τ_n – термове. Нека A е структура, в която предикатният символ p е интерпретиран така, че винаги е истина. Тогава очевидно в тази структура литералът L ще бъде верен без значение каква е оценката. Следователно D е верен в тази структура.

Във втория случай – когато L е отрицание на атомарна формула се действа аналогично, само че тогава ще интерпретираме предикатния символ така, че да бъде винаги лъжа.  □

В) Твърдение. Предикатен дизюнкт е тавтологичен тогава и само тогава, когато съдържа едновременно литерал заедно с неговия дуален.

Доказателство. Засега не сме подготвени да докажем лесно, че ако дизюнкт е тавтологичен, то той със сигурност съдържа даден литерал едновременно с неговото отрицание. Ще докажем само обратната посока на твърдението.

Да допуснем, че дизюнктът D е такъв, че за някой литерал L едновременно L∈D и L^∂∈D. Да изберем произволни структура A и оценка v. Ако L не е верен в A при v, то L^∂ e верен и обратно – ако L^∂ не е верен, то L е верен. И в двата случая получаваме, че D съдържа литерал, който е верен в A при оценка v. Тъй като A и v бяха произволни, то D е тавтологичен.  □

Г) Твърдение. Затворен дизюнкт е верен в структура A тогава и само тогава, когато той съдържа литерал, който е верен в A.

Доказателство. (⇒) Нека D е затворен дизюнкт, който е верен в A. Да изберем произволна оценка v. Тъй като D e верен в A при оценка v, то D съдържа литерал L, който е верен в A при оценка v. Но D е затворен и значи литералът L също е затворен и верността му не зависи от оценката. Следователно L е верен в A при произволна оценка, което по дефиниция означава, че L е верен в A.

(⇐) Ако дизюнктът D съдържа литерал L, който е верен в структурата A, то значи L е верен в A при произволна оценка. Следователно при произволна оценка D съдържа литерал, който е верен в A. По дефиниция това означава, че D е верен в A.  □

Д) Твърдение. Множество от дизюнкти има модел тогава и само тогава, когато има Ербранов модел.

Доказателство. (⇒) Нека Γ е изпълнимо множество от дизюнкти (т.е. множество, което има модел). Тъй като празният дизюнкт не може да принадлежи на Γ, то за всеки дизюнкт D от Γ съществува такава елементарна дизюнкция φ, че D=D_φ. Нека Γ' е такова множество, че за всеки дизюнкт D от Γ в Γ' се съдържа елементарна дизюнкция φ, за която D=D_φ. Коя да е елементарна дизюнкция φ е вярна в някоя структура A тогава и само тогава, когато дизюнктът D_φ е верен в A. Поради това от съществуването на модел за Γ следва, че същата структура е модел и за Γ. Но от (2Г) следва, че Γ' има Ербранов модел. Същата структура ще бъде модел и за Γ.

(⇐) Тази посока е тривиална.  □

Е) Засега не знаем дали съждителната резолюция може да се използва и в предикатния случай. Но тъй като основната разлика между съждителната и предикатната логика са кванторите, то надеждата ни е, че поне в безкванторния случай съждителната резолюция ще работи. Тъй като в дефиницията за вярност на предикатен дизюнкт в структура се съдържа неявен квантор за всеобщност (защото в дефиницията е казано „при произволна оценка“), то когато става въпрос за дизюнкти „безкванторен случай“ ще рече „затворен дизюнкт“ – при затворените дизюнкти оценката е без значение.

Да докажем, че съждителната резолюция наистина може да се използва когато предикатните дизюнкти са затворени.

Ж) Твърдение. Ако Γ е множество от затворени предикатни дизюнкти, то Γ е изпълнимо тогава и само тогава, когато не съществува съждителен резолютивен извод на ■ от Γ. (И разбира се Γ е неизпълнимо тогава и само тогава, когато съществува съждителен резолютивен извод на ■ от Γ.)

Забележка. Правата посока (⇒) на това твърдение се нарича „пълнота на съждителната резолютивна изводимост за затворени предикатни дизюнкти“. Обратната посока (⇐) се нарича „коректност на съждителната резолютивна изводимост за затворени предикатни дизюнкти“.

Доказателство. Ако в Γ се съдържа празният дизюнкт, то от една страна очевидно Γ e неизпълнимо, а от друга съществува съждителен резолютивен извод на празния дизюнкт от Γ. Така че в този случай няма какво да доказваме.

Сега да разгледаме случая когато празният дизюнкт не се съдържа в Γ. Тогава за всеки дизюнкт D от Γ съществува такава елементарна дизюнкция φ, че D=D_φ. Нека Γ' е такова множество, че за всеки дизюнкт D от Γ в Γ' се съдържа елементарна дизюнкция φ, за която D=D_φ. Тъй като коя да е елементарна дизюнкция φ е вярна в някоя структура A тогава и само тогава, когато дизюнктът D_φ е верен в A, то множеството Γ е изпълнимо тогава и само тогава, когато Γ' е изпълнимо. Да забележим още, че коя да е елементарна дизюнкция, разглеждана като съждителна формула е вярна при някоя съждителна интерпретация I тогава и само тогава, когато дизюнктът D_φ е верен при I. Следователно множеството Γ е булево изпълнимо тогава и само тогава, когато Γ' е изпълнимо.

Елементарните дизюнкции от Γ' са затворени формули, които не съдържат никакви квантори. Следователно те са универсални затворени формули. (Да припомним, че универсална затворена формула е затворена формула от вида ∀x₁∀x₂…∀x_nφ, където φ е безкванторна формула и се позволява n=0, т.е. отпред да има нула на брой квантори.)

Съгласно малката теорема на Ербран (2Г) Γ' е изпълнимо тогава и само тогава, когато е булево изпълнимо множеството CSi(Γ') от всички затворени частни случаи на формулите от Γ'. Но формулите от Γ' са едновременно безкванторни и затворени и следователно не съдържат променливи, които да заменяме при образуването на частни случаи. Това означава, че за всяка формула φ от Γ' единственият затворен частен случай на φ е самата формула φ и значи Γ'=CSi(Γ').

По този начин доказахме, че Γ е изпълнимо тогава и само тогава, когато Γ' е изпълнимо, тогава и само тогава, когато Γ' е булево изпълнимо, тогава и само тогава, когато Γ е булево изпълнимо.

Съгласно теоремите за пълнота и коректност на съждителната резолютивна изводимост множеството Γ e булево изпълнимо тогава и само тогава, когато съществува съждителен резолютивен извод на празния дизюнкт от Γ.  □

И) Сега да разгледаме общия случай – когато не е задължително дизюнктите да бъдат затворени. В сила е следното

Твърдение. Ако предикатният дизюнкт D е съждителна резолвента на предикатните дизюнкти D₁ и D₂ и дизюнктите D₁ и D₂ са верни в дадена структура A, то дизюнктът D също е верен в A.

Доказателство. Да допуснем, че дизюнктите D₁ и D₂ са верни в дадена структура A и да изберем произволна оценка v. Ако успеем да докажем, че D е верен в A при оценка v, поради произволността на v от това ще следва, че D е верен в A, което и трябва да докажем.

Съгласно дефиницията на съждителна резолвента съществува такъв литерал L, че D=D₁\{L}∪D₂\{L^∂}. Литералът L или е верен в A при оценката v, или не е. Да разгледаме случая, когато L е верен и съответно литералът L^∂ не е верен. Тъй като дизюнктът D₂ е верен в структурата A, то той е верен в A при оценка v. Значи D₂ съдържа поне един литерал, който е верен в A при оценка v. Но литералът L^∂ не е верен, следователно сред литералите от D₂\{L^∂} трябва да се съдържа поне един верен литерал. Тъй като D₂\{L^∂}⊆D, то дизюнктът D съдържа поне един верен в A при оценка v литерал, следователно D е верен в A при оценка v.

Вторият случай – когато L е неверен в A при оценка v е аналогичен. Тогава D₁\{L} трябва да съдържа поне един верен литерал.  □

Й) Току що доказаното твърдение показва, че ако Γ е множество от верни в дадена структура A предикатни дизюнкти и започнем да добавяме към Γ нови и нови съждителни резолвенти на дизюнктите от Γ, то всички така породени дизюнкти ще се оказват верни в A. Разбира се празният дизюнкт е винаги неверен и значи не може да бъде породен.

Така виждаме, че ако множество от предикатни дизюнкти е изпълнимо, то празният дизюнкт не е изводим от това множество. И обратно – ако празният дизюнкт е изводим посредством пораждане на съждителни резолвенти от множество от предикатни дизюнкти, то това множество е неизпълнимо. Току що направената констатация можем да наречем коректност на съждителната резолюция за предикатни дизюнкти.

За съжаление надеждата ни, че съждителната резолюция може да се окаже пълна и в предикатния случай, лесно се попарва. Да разгледаме множеството Γ={{p(x)},{¬p(a)}}, където p е предикатен символ, x е променлива и a е индивидна константа. Лесно се забелязва, че ако формулата ¬p(a) е вярна в някоя структура, то няма начин в същата структура да е вярна и формулата p(x) (последното би означавало да е вярно и универсалното ѝ затваряне ∀xp(x)). Следователно множеството Γ е неизпълнимо. Въпреки това от дизюнктите в Γ не може да се породи нито една съждителна резолвента и значи празният дизюнкт не е изводим.

Но макар този прост пример да показва, че съждителната резолюция не е пълна за предикатни дизюнкти, той е полезен още и с това, че показва доста ясно какво точно ѝ липсва на съждителната резолюция, за да бъде тя пълна. Ако в дадена структура е верен дизюнктът {p(x)}, то в същата структура ще е вярна формулата ∀xp(x) и значи ще е вярна формулата p(a) и съответно дизюнктът {p(a)}. Тъй като празният дизюнкт е съждителна резолвента на дизюнктите {p(a)} и {¬p(a)}, то значи за да можем да изведем празния дизюнкт от множеството Γ={{p(x)},{¬p(a)}}, е нужно при пораждането на съждителни резолвенти да позволим и вземането на частни случаи на дизюнктите. В разгледания конкретен случай е необходимо да вземем частния случай {p(a)} на първоначалния дизюнкт {p(x)}.

По-нататък ще видим, че вземането на подходящи частни случаи е изключително важно когато прилагаме метода на резолюциите за предикатни дизюнкти. Знаем, че всяко пораждане на частен случай представлява замяна на променливи с термове. Затова сега се налага да спрем временно изследването на предикатната резолюция, за да въведем едно ново понятие – субституцията. Субституциите представляват формализация на понятието „замяна на променливи с термове“.

§4. Субституции

A) Да си припомним, че универсумът на свободните Ербранови структури е множеството на всички термове и поради това можем да наречем това множество свободен Ербранов универсум. Всяка оценка в свободна Ербранова структура представлява функция, чийто аргумент е променлива, а стойността ѝ е елемент на свободния Ербрановия универсум, т.е. терм. Такива оценки ще наричаме свободни Ербранови оценки. Виждаме, че всяка замяна на променливи с термове може да бъде представена посредством свободна Ербранова оценка.

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

Б) Дефиниция. Субституцията е такава свободна Ербранова оценка, че за всички променливи, освен евентуално за краен брой, е в сила равенството s(x)=x.

Посредством {x₁/τ₁,x₂/τ₂,…,x_n/τ_n} ще обозначаваме субституцията s, за която s(x₁)=τ₁, s(x₂)=τ₂,…, s(x_n)=τ_n и s(y)=y, за всяка променлива y, различна от x₁,x₂,…,x_n.

В) Дефиниция. Ако s е субституция, а τ е терм, то с τs ще обозначаваме резултатът от замяната на всяка променлива x в τ с s(x). Термът τs се нарича резултат от прилагането на субституцията s към терма τ. Ако φ е безкванторна формула, то φs се дефинира аналогично и се нарича резултат от прилагането на субституцията s към формулата φ.

Забележка. Има начин да се дефинира резултат от прилагането на субституция към произволна формула, но дефиницията е много трудоемка, а пък и няма да ни трябва и затова няма да я даваме.

Г) Директно от дефинициите следва, че за произволен терм τ и безкванторна формула φ са в сила следните равенствa:

Д) Следствие. Частните случаи на терм τ са всички термове от вида τs, където s е произволна субституция. Частните случаи на безкванторна формула φ са всички формули от вида φs, където s е произволна субституция.

Е) Дефиниция. Ако Γ е множество от безкванторни формули и s е субституция, с Γs ще означаваме множеството от всички формули от вида φs, където φ∈Γ. В частност, ако D={L₁,…,L_n} е непразен дизюнкт, а s - субституция, то Ds={L₁s,…,L_ns}. Ако пък D е празният дизюнкт, то Ds също е празният дизюнкт.

Ж) Дефиниция. Ако D е дизюнкт, то дизюнктите от вида Ds при произволна субституция s ще наричаме частни случаи на D. Частните случаи, които са затворени дизюнкти, ще наричаме затворени частни случаи.

И) Да забележим, че всеки терм, всяка безкванторна формула и всеки дизюнкт е частен случай на себе си. Например ако D е произволен дизюнкт, то нека s е субституцията идентитет (т.е. s(x)=x за всяка променлива). Тогава очевидно Ds=D.

Й) Дефиниция. Ако s и t са субституции, с st ще означаваме Eрбрановата оценка, която на произволна променлива x съпоставя резултата от прилагането на субституцията t към терма s(x). С други думи за произволна променлива x е в сила следното равенство:

Свободната Ербранова оценка ts се нарича композиция на t и s.

Лесно се вижда, че композицията на субституции е не каква да е свободна Ербранова оценка, а също субституция.

К) Твърдение. За произволен терм τ и безкванторна формула φ и за произволни субституции s и t е в сила (τs)t=τ(st) и (φs)t=φ(st). Това означава, че можем да изпускаме скобите и да пишем просто τst и φst вместо τ(st) и φ(st) или (τs)t и (φs)t.

Доказателство. Ще докажем твърдението за случая на терм τ. Случаят на безкванторна формула е напълно аналогичен. Термът τs представлява замяната на всяка променлива x в τ с s(x). Това означава, че всяка променлива, срещаща се в τs се съдържа в терм s(x), който се е появил в τs в резултат от замяната на някоя променлива x от τ с s(x). Ако сега приложим t към τs, всяка такава променлива ще бъде заменена с терма t(x). Това показва, че последователното прилагане най-напред на s и после на t към τ е равносилно на замяната на всяка променлива x от τ с резултата от прилагането на t към терма s(x). По дефиниция последното означава да приложим st към τ.  □

Л) Следствие. Частен случай на частен случай е частен случай.

Доказателство. Нека дизюнктът D₁ е частен случай на D₂ и D₂ е частен случай на D₃. От дефиницията на частен случай следва, че съществуват такива субституции s₁ и s₂, че D₂=D₁s₁ и D₃=D₂s₂. Съгласно току що доказаното твърдение D₃=D₁(s₁s₂). Следователно D₃ е частен случай на D₁.

М) Дефиниция Ако s е субституция, а v – оценка в структурата A, то с ∥s∥^A[v] ще означаваме субституцията в A, която на всяка променлива x дава стойност ∥s(x)∥^A[v].

Оценката ∥s∥^A[v] се нарича композиция на субституцията s с оценката v в структурата A.

Н) Твърдение. (1) За произволен терм τ, субституция s и оценка v в структура A е в сила равенството:

(2) За произволна безкванторна формула φ, субституция s и оценка v в структура A е в сила същото равенство:

(3) За произволен дизюнкт D, субституция s и оценка v в структура A е в сила равенството:

Доказателство. (1) Нека за определеност s={x₁/τ₁,x₂/τ₂,…,x_n/τ_n}. Нека v₁=∥s∥^A[v] и v₂=v. Тогава за произволно i е в сила v₁(x_i)=∥τ_i∥^A[v₂]. Ако пък променливата y не е измежду x₁,x₂,…,x_n, то тогава v₁(y) = ∥s(y)∥^A[v] = ∥y∥^A[v] = v(y) = v₂(y). Следователно можем да прилагаме твърдението за стойност на терм след замяна. Съгласно това твърдение ∥τ∥^A[v₁] = ∥τ[x₁/τ₁,x₂/τ₂,…,x_n/τ_n]∥^A[v₂], което е просто друг запис на равенството, което трябваше да докажем.  □

(2) С индукция по построението на формулата φ. Нека за краткост w=∥s∥^A[v].

Ако φ=p(τ₁,…,τ_n) е атомарна формула, то ∥φs∥^A[v] = ∥(p(τ₁,…,τ_n))s∥^A[v] = ∥p(τ₁s,…,τ_ns)∥^A[v]. Последното е истина тогава и само тогава, когато <∥τ₁s∥^A[v],…,∥τ_ns∥^A[v]>∈p^A. Съгласно (1) ∥τ_is∥^A[v] = ∥τ_i∥^A[∥s∥^A[v]] = ∥τ_i∥^A[w], следователно горното е истина тогава и само тогава, когато <∥τ_i∥^A[w],…,∥τ_n∥^A[w]>∈p^A и значи тогава и само тогава, когато е истина ∥p(τ₁,…,τ_n)∥^A[w] = ∥φ∥^A[w] = ∥φ∥^A[∥s∥^A[v]].

Ако φ=¬ψ, то използвайки индукционното предположение ∥ψs∥^A[v]=∥ψ∥^A[w], получаваме ∥φs∥^A[v] = ∥(¬ψ)s∥^A[v] = ∥¬(ψs)∥^A[v] = H_¬(∥ψs∥^A[v]) = H_¬(∥ψ∥^A[w]) = ∥¬ψ∥^A[w] = ∥φ∥^A[w] = ∥φ∥^A[∥s∥^A[v]].

Ако φ=ψ₁⋁ψ₂, то използвайки индукционното предположение ∥ψ₁s∥^A[v]=∥ψ₁∥^A[w] и ∥ψ₂s∥^A[v]=∥ψ₂∥^A[w], получаваме ∥φs∥^A[v] = ∥((ψ₁⋁ψ₂)s∥^A[v] = ∥((ψ₁s)⋁(ψ₂s)∥^A[v] = H_⋁(∥ψ₁s∥^A[v],∥ψ₂s∥^A[v]) = H_⋁(∥ψ₁∥^A[w],∥ψ₂∥^A[w]) = ∥ψ₁⋁ψ₂∥^A[w] = ∥φ∥^A[w] = ∥φ∥^A[∥s∥^A[v]].

Случаите φ=ψ₁&ψ₂, φ=ψ₁⇒ψ₂ и φ=ψ₁⇔ψ₂ се разглеждат аналогично.  □

(3) Директно от дефинициите следва, че горното равенство е вярно в случая, когато D е празният дизюнкт. В противен случай нека φ е такава елементарна дизюнкция, че D=D_φ. Тогава директно от дефинициите следва, че Ds=D_φs=D_φs и значи ∥Ds∥^A[v] = ∥D_φs∥^A[v] = ∥φs∥^A[v] и ∥D∥^A[∥s∥^A[v]] = ∥D_φ∥^A[∥s∥^A[v]] = ∥φ∥^A[∥s∥^A[v]]. Но от (Н) следва, че ∥φs∥^A[v] = ∥φ∥^A[∥s∥^A[v]], така че получаваме исканото.  □

П) Забележка. Може да се забележи, че всичко направено в този параграф е вярно не само при използване на субституции, но и изобющо за произволни свободни Ербранови оценки.

§5. Либерална резолюция

A) Твърдение. Дизюнкт е верен в структура тогава и само тогава, когато в структурата са верни всичките му частни случаи.

Доказателство. (⇒) Да допуснем, че дизюнктът D е верен в структура A. Да изберем произволен частен случай Ds на D. Нека v e произволна оценка в структурата A и w е оценката w=∥s∥^A[v]. Съгласно (4Н) ∥Ds∥^A[v] = ∥D∥^A[∥s∥^A[v]] = ∥D∥^A[w]. Последното е истина, тъй като дизюнктът D е верен в A, следователно Ds е верен в A при оценка v. От това и произволността на v следва верността на Ds в A.

(⇐) Тъй като всеки дизюнкт е частен случай на себе си, то ако в дадена структура са верни всички частни случаи на даден дизюнкт, то в частност в структурата ще бъде верен и самият дизюнкт.  □

Б) Твърдение. Дизюнкт е верен в Ербранова структура тогава и само тогава, когато в структурата са верни всичките му затворени частни случаи.

Доказателство. (⇒) Тази посока на твърдението следва от (A).

(⇐) Да допуснем, че в Ербрановата структура A са верни всички затворени частни случаи на дизюнкта D. Да изберем произволна оценка v в A. Трябва да докажем, че D е верен в A при оценка v. Нека всички свободни променливи в D са измежду x₁,x₂,…,x_n и s бъде субституцията s={x₁/v(x₁),x₂/v(x₂),…,x_n/v(x_n)}. Тъй като структурата A е Ербранова, то v(x₁),v(x₂),…,v(x_n) са затворени термове и значи Ds затворен дизюнкт. Нека w е оценката w=∥s∥^A[v]. По дефиниция w(x_i) = ∥s(x_i)∥^A[v] = ∥v(x_i)∥^A[v]. Последното е равно на v(x_i), тъй като v(x_i) е затворен терм, а стойността на затворен терм в Ербранова структура при каква да е оценка е самият терм. Така получаваме, че v(x_i)=w(x_i), т.е. оценките v и w съвпадат за всички свободни променливи на D. Следователно ∥D∥^A[v] = ∥D∥^A[w] = ∥D∥^A[∥s∥^A[v]] = ∥Ds∥^A[v]. Последното е истина, тъй като Ds е затворен частен случай на D.

В) Твърдение. Множество от дизюнкти е изпълнимо тогава и само тогава, когато е изпълнимо множеството от всичките затворени частни случаи на дизюнктите от множеството.

Доказателство. (⇒) От (A) следва, че ако Γ е изпълнимо множество от дизюнкти, то е изпълнимо и множеството от всички затворени частни случаи на дизюнктите от Γ.

(⇐) Щом затворените частни случаи на дизюнктите от Γ образуват изпълнимо множество, то съгласно (3Д) те имат ербранов модел. Съгласно (Б) същата структура е модел и за дизюнктите от Γ.  □

Г) Дефиниция. Казваме, че дизюнкт D е либерална резолвента на дизюнктите D₁ и D₂, ако D е съждителна резолвента на някой частен случай на D₂ и частен случай на D₂.

Д) Твърдение. Нека D е либерална резолвента на D₁ и D₂. Ако D₁ и D₂ са верни в структура A, то D също е верен в A.

Доказателство. Следва непосредствено от (A) и (3И).  □

Е) Дефиниция. Нека D е дизюнкт и Γ е множество от дизюнкти. Казваме, че редицата от дизюнкти D₁,D₂,…,D_n е либерален резолютивен извод на D от Γ, ако:

(1) Всеки член на редицата е елемент на Γ или е либерална резолвента на дизюнкти, срещащи се преди него в редицата.

(2) D_n=D.

Ж) Дефиниция. Казваме, че дизюнктът D е изводим посредством либерална резолюция от множеството от дизюнкти Γ, ако съществува либерален резолютивен извод на D от Γ.

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

Доказателство. Да изберем произволна структура A. Тъй като празният дизюнкт е изводим посредством либерална резолюция от Γ, то съществува либерален резолютивен извод на празния дизюнкт от Γ. Самият празен дизюнкт не е верен в никоя структура и в частност не е верен в A. Следователно този резолютивен извод съдържа поне един дизюнкт, който не е верен в A. Нека D бъде първият дизюнкт от този резолютивен извод, който не е верен в A. Съгласно дефиницията на либерален резолютивен извод D е елемент на Γ или е либерална резолвента на дизюнкти, срещащи се преди него в извода. Но той не може да бъде резолвента на дизюнкти, срещащи се преди него в извода, защото всички такива дизюнкти са верни в A, тъй че от (Д) би следвало, че и D е верен в A. Следователно D е елемент на Γ.

Така доказахме, че Γ съдържа дизюнкт, който не е верен в A. Тъй като структурата A бе избрана произволно, то виждаме, че не може да съществува структура, в която са верни всички формули от Γ.  □

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

Доказателство. Нека Γ е неизпълнимо множество от дизюнкти и Γ' е множеството от всички затворени частни случаи на дизюнктите от Γ. Съгласно (В) Γ' е неизпълнимо. Съгласно (3Ж) съществува съждителен резолютивен извод на празния дизюнкт от дизюнктите от Γ'. Нека D₁,D₂,…,D_n е някой такъв съждителен резолютивен извод. Да дефинираме дизюнктите D'₁,D'₂,…,D'_n по следния начин: ако D_i е затворен частен случай на поне един елемент на Γ, то нека D'_i бъде някой такъв дизюнкт от Γ; в противен случай нека D'_i=D_i. Ще докажем, че редицата D'₁,D'₂,…,D'_n е либерален резолютивен извод на празния дизюнкт от Γ.

Първо трябва да докажем, че всеки елемент на тази редица е елемент на Γ, или е либерална резолвента от дизюнкти, които го предхождат в редицата. Да допуснем, че тази редица съдържа дори един дизюнкт, който не е елемент на Γ, нито е либерална резолвента на дизюнкти които го предхождат. Нека D'_j е първият такъв дизюнкт. Щом D'_j не е елемент на Γ, то D_j не е затворен частен случай на никой елемент на Γ, следователно D_j не е елемент на Γ'. Но D₁,D₂,…,D_n е съждителен резолютивен извод, значи D_j е съждителна резолвента на дизюнкти, които го предхождат в този резолютивен извод. Нека D_j е съждителна резолвента на D_k и D_l, където k<j и l<j. Съгласно дефиницията на D'₁,D'₂,…,D'_n дизюнктите D_k и D_l са частни случаи на дизюнктите D'_k и D'_l, следователно D_j е съждителна резолвента на частни случаи на D'_k и D'_l, т.е. D_j е либерална резолвента на D'_k и D'_l. Но D_j=D'_j, тъй като D'_j не е елемент на Γ, значи D'_j е либерална резолвента на D'_k и D'_l – противоречие.  □

К) Въпреки, че получихме коректна и пълна изводимост за предикатната логика, тази изводимост на практика не може да се използва с компютър, тъй като дизюнктите имат твърде много частни случаи (обикновено безброй много), така че и либералните резолвенти – дори само от два дизюнкта – са безброй много. Така например от дизюнктите {p(x),q(f(x))} и {¬p(x)} получаваме следните безброй много либерални резолвенти: {q(f(x))}, {q(f(f(x)))}, {q(f(f(f(x))))}, {q(f(f(f(f(x)))))} и т.н. Всички тези безброй много дизюнкти обаче са частни случаи на първия от тях, така че ако се ограничим само с него, пълнотата не би трябвало да се загуби. За да формализираме това наблюдение и да направим действително използваема резолютивна процедура, в следващия параграф ще въведем важното понятие „най-общ унификатор“, след което ще формулираме резолютивна процедура, използваща това понятие.

§6. Унификация

A) Най-напред ще дефинираме помятието унификатор и ще преформулираме дефиницията на либерална резолвента, използвайки унификатори.

Б) Дефиниция. Нека x₁,x₂,…,x_n са всички свободни променливи на дизюнкта D (като искаме x_i≠x_j при i≠j). Дизюнктите от вида D[x₁/y₁,x₂/y₂,…,x_n/y_n], където y₁,y₂,…,y_n са различни променливи се наричат варианти на D.

В) Лесно се забелязва, че релацията „вариант“ е релация на еквивалентност. По конкретно:

(1) Всеки дизюнкт е вариант на себе си.

(2) Ако D' е вариант на D'', то и D'' е вариант на D'.

(3) Ако D' е вариант на D'' и D'' е вариант на D''', то D' е вариант на D'''.

Г) Също така лесно се забелязва, че ако два дизюнкта са варианти, то те имат едни и същи частни случаи.

Д) Очевидно за кои да е два дизюнкта D₁ и D₂ могат да се намерят такива варианти D'₁ и D'₂, че дизюнктите D'₁ и D'₂ да нямат общи променливи.

Е) Дефиниция. Казваме, че субституцията s е унификатор за множеството от литерали Γ, ако Γs е едноелементно множество. Да припомним, че Γs={ξs : ξ∈Γ}.

Ж) Дефиниция. Казваме, че субституцията s₁ е частен случай на s₂, ако за някоя субституция s е вярно s₁=s₂s.

И) Вижда се, че ако субституцията s₁ е частен случай на s₂, то ξs₁ е частен случай на ξs₂ за произволен терм или безкванторна формула ξ.

Й) Дефиниция. Субституцията s е най-общ унификатор за множеството Γ, ако s e унификатор за Γ и всеки унификатор за Γ е частен случай на s.

К) Оказва се, че е възможно да ограничим съществено броя на резолвентите, ако формулираме резолютивната процедура по такъв начин, че тя да използва най-общи унификатори, а не какви да е субституции. Така например ако някое множество от литерали има поне един унификатор, то това множество обикновено има безброй много унификатори. Оказва се обаче, че с точност до преименуване на променливите такова множество притежава само един най-общ унификатор. Ще оставим това без доказателство.

Ако едно множество има най-общ унификатор, то този най-общ унификатор може да замени употребата на кой да е друг унификатор на това множество, тъй като всички унификатори са негови частни случаи. Остава обаче въпросът вярно ли е, че едно множество, което притежава унификатор, притежава и най-общ унификатор? Отговорът на този върпос е положителен.

Л) Твърдение. Ако множество Γ притежава унификатор, то Γ притежава и най-общ унификатор.

Ще отложим доказателството на това твърдение за по-нататък, когато ще дадем и алгоритъм, който проверява дали дадено крайно множество от термове или литерали притежава унификатор и ако да – то намира най-общ унификатор.

§7. Предикатна резолюция

A) Дефиниция. Дизюнктът D е предикатна резолвента на дизюнктите D₁ и D₂, ако дизюнктите D₁ и D₂ имат такива варианти D'₁ и D'₂, че
(1) D'₁ и D'₂ нямат общи променливи,
(2) D'₁ и D'₂ притежават такива непразни подмножества Γ₁⊆D'₁ и Γ₂⊆D'₂, че
(3) множеството Γ₁∪Γ₂^∂ притежава най-общ унификатор s, за който
(4) D=(D'₁s)\(Γ₁s)∪(D'₂s)\(Γ₂s).

Б) Твърдение. Всяка предикатна резолвента е либерална резолвента.

Доказателство. Нека дизюнктът D е предикатна резолвента на D₁ и D₂. Съгласно дефиницията на предикатна резолвента това означава, че D₁ и D₂ имат такива варианти D'₁ и D'₂, че D'₁ и D'₂ нямат общи променливи и D'₁ и D'₂ притежават такива непразни подмножества Γ₁⊆D'₁ и Γ₂⊆D'₂, че множеството Γ₁∪Γ₂^∂ притежава най-общ унификатор s, за който D=(D'₁s)\(Γ₁s)∪(D'₂s)\(Γ₂s). Нека субституциите s₁ и s₂ са такива, че D'₁=D₁s₁ и D'₂=D₂s₂. Тъй като s е унификатор за Γ₁∪Γ₂^∂, то съществува такъв литерал L, че Γ₁s={L} и Γ₂s={L^∂}. В сила са следните равенства: D = (D'₁s)\(Γ₁s)∪(D'₂s)\(Γ₂s) = (D'₁s)\{L}∪(D'₂s)\{L^∂} = (D₁s₁s)\{L}∪(D₂s₂s)\{L^∂}. Но литералът L се среща в D₁s₁s, защото от Γ₁⊆D₁'=D₁s₁ следва {L}=Γ₁s⊆D₁'s=D₁s₁s и аналогично литералът L^∂ се среща в D₂s₂s. Следователно D е съждителна резолвента на дизюнктите D₁s₁s и D₂s₂s, които от своя страна са частни случаи на D₁ и D₂. По дефиниция D е либерална резолвента на D₁ и D₂.  □

В) Дефиниция. Нека D е дизюнкт и Γ е множество от дизюнкти. Казваме, че редицата от дизюнкти D₁,D₂,…,D_n е предикатен резолютивен извод на D от Γ, ако:

(1) Всеки член на редицата е елемент на Γ или е предикатна резолвента на дизюнкти, срещащи се преди него в редицата.

(2) D_n=D.

Г) Дефиниция. Казваме, че дизюнктът D е изводим посредством предикатна резолюция от множеството от дизюнкти Γ, ако съществува предикатен резолютивен извод на D от Γ.

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

Доказателство: Тъй като всяка предикатна резолвента е и либерална резолвента, то всеки предикатен резолютивен извод е и либерален резолютивен извод. Затова теоремата следва от теоремата за коректност на либералната резолюция (5И).  □

За да докажем пълнотата, имаме нужда от следната

Е) Лема за повдигането
Ако D е либерална резолвента на D₁ и D₂ и D₁ и D₂ са частни случаи съответно на D'₁ и D'₂, то D е частен случай на някоя предикатна резолвента D' на D'₁ и D'₂.

Доказателство. Съгласно дефиницията на либерална резолвента D е съждителна резолвента на някои частни случаи на D₁ и D₂. Но D₁ и D₂ от своя страна са частни случаи на D'₁ и D'₂. Затова от (4Л) следва, че D е съждителна резолвента на някои частни случаи на D'₁ и D'₂, т.е. D е либерална резолвента на D'₁ и D'₂.

Нека D''₁ и D''₂ са произволни варианти на D'₁ и D'₂, които нямат общи променливи. Тъй като съгласно (6Г) вариантите имат едни и същи частни случаи, то D е съждителна резолвента на някои частни случаи на D''₁ и D''₂. Нека субституциите s₁ и s₂ са такива, че D е съждителна резолвента на D''₁s₁ и D''₂s₂. Тогава за някой литерал L е вярно равенството D=(D''₁s₁)\{L}∪(D''₂s₂)\{L^∂}, като при това L∈D''₁s₁ и L^∂∈D''₂s₂. Нека субституцията s е такава че s(x)=s₁(x), ако променливата x се среща в D''₁, s(x)=s₂(x), ако променливата x се среща в D''₂ и s(x) е дефинирано произволно за останалите променливи. Можем да дефинираме такава субституция s, тъй като D''₁ и D''₂ нямат общи променливи. Тогава D''₁s₁=D''₁s и D''₂s₂=D''₂s.

Да дефинираме множествата Γ₁={K∈D''₁ : Ks=L} и Γ₂={K∈D''₂ : Ks=L^∂}. Те са непразни, тъй като L∈D''₁s₁=D''₁s и L^∂∈D''₂s₂=D''₂s. Тъй като (Γ₁∪Γ₂^∂)s={L}, то субституцията s е унификатор за Γ₁∪Γ₂^∂. Нека s' е най-общ унификатор за Γ₁∪Γ₂^∂ и D'⇋(D''₁s')\(Γ₁s')∪(D''₂s')\(Γ₂s'). От дефиницията за предикатна резолвента следва, че D' е предикатна резолвента на D'₁ и D'₂, така че единственото, което остава да докажем е, че D е частен случай на D'.

Тъй като s' е най-общ унификатор за Γ₁∪Γ₂^∂, а s – унификатор за същото множество, то s е частен случай на s'. Значи s=s's'' за някоя субституция s''. Тогава са в сила равенствата: D = (D''₁s₁)\{L}∪(D''₂s₂)\{L^∂} = (D''₁s)\{L}∪(D''₂s)\{L^∂} = (D''₁s)\(Γ₁s)∪(D''₂s)\(Γ₂s) = (D''₁s's'')\(Γ₁s's'')∪(D''₂s's'')\(Γ₂s's''). От друга страна D' = (D''₁s')\(Γ₁s')∪(D''₂s')\(Γ₂s'). Следователно за да докажем, че D е частен случай на D' е достатъчно да покажем, че (D''₁s's'')\(Γ₁s's'')=((D''₁s')\(Γ₁s'))s'' и (D''₂s's'')\(Γ₂s's'')=((D''₂s')\(Γ₂s'))s''.

Ще докажем само първото от тези равенства (второто се доказва аналогично). Да изберем произволен литерал от (D''₁s's'')\(Γ₁s's''). Този литерал е равен на Ks's'', където K е литерал от D''₁. Ясно е, че Ks'∈D''₁s'. Освен това от Ks's''∉Γ₁s's'' следва Ks'∉Γ₁s'. Следователно Ks's''∈((D''₁s')\(Γ₁s'))s''. По този начин доказахме, че (D''₁s's'')\(Γ₁s's'')⊆((D''₁s')\(Γ₁s'))s''.

Сега нека изберем произволен литерал от ((D''₁s')\(Γ₁s'))s''. Този литерал е равен на Ks's'', където K е литерал от D''₁, такъв че Ks'∈D''₁s' и Ks'∉Γ₁s'={L'}. Тъй като е ясно, че Ks's''∈D''₁s's'', за да докажем, че Ks's''∈(D''₁s's'')\(Γ₁s's'') е достатъчно да покажем, че Ks's''∉Γ₁s's''. Да допуснем противното, т.е. че Ks's''∈Γ₁s's''. Но Γ₁s's''={L}, значи Ks's''=L, т.е. Ks=L, което съгласно дефиницията на Γ₁ означава, че K∈Γ₁. От това следва Ks'∈Γ₁s', което е противоречие.  □

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

Доказателство. Съглано теоремата за пълнота на либералната резолюция съществува резолютивен извод D₁,D₂,…,D_n на празния дизюнкт от Γ. Да дефинираме дизюнктите D'₁,D'₂,…,D'_n, така че D_i е частен случай на D'_i по следния начин: ако D_i∈Γ, то нека D'_i=D_i. Ако пък D_i∉Γ, то D_i либерална резолвента на дизюнкти D_j и D_k, където j<i и k<i. Тъй като D_j е частен случай на D'_j, а D_k – на D'_k, то съгласно лемата за повдигането съществува такава предикатна резолвента на D'_j и D'_k, че D_i е неин частен случай. Нека тази предикатна резолвента бъде D'_i.

Тъй като D_n е празният дизюнкт и D_n e частен случай на D'_n, то D'_n също е празният дизюнкт. Следователно D'₁,D'₂,…,D'_n е предикатен резолютивен извод на празния дизюнкт от Γ.  □

§8. Алгоритъм за намиране на най-общ унификатор

A) В рамките на този параграф под „израз“ ще разбираме терм или безкванторна формула. „Уравнение“ е дума от вида τ=σ, където τ₁ и τ₂ са изрази. „Система“ e множество от уравнения.

Б) Казваме, че субституцията s е решение на системата {τ₁=σ₁,τ₂=σ₂,…,τ_n=σ_n}, ако изразите τ_is и σ_is съвпадат при всяко i от 1 до n.

В) Казваме, че две системи са еквивалентни, ако множествата от решенията им съвпадат.

Г) Казваме че дадена система е решена относно променливата x, ако тя съдържа уравнение от вида x=τ и променливата x не се съдържа нито в τ, нито в някое друго уравнение от системата. За уравнението x=τ ще казваме, че е решаващо.

Д) Нека Γ={τ₁,…,τ_n} е произволно крайно множество от изрази. Да разгледаме системата {τ₁=τ₂,τ₂=τ₃,…,τ_n-1=τ_n}. Директно от дефинициите следва, че една субституция е унификатор за Γ тогава и само тогава, когато тя е решение на тази система.

Това, което предстои да направим сега, е да намерим алгоритм, посредством който всяка за система или ще бъде установено, че тя няма решения, или ще бъде намерена еквивалентна ней система, която съдържа единствено решаващи уравнения. Следващото твърдение има следствие, което показва ясно ползата от това.

Е) Твърдение. Нека системата {x₁=τ₁,x₂=τ₂,…,x_n=τ_n} съдържа единствено решаващи уравнения. Тогава субституцията {x₁/τ₁,…,x_n/τ_n} е решение на тази система и всяко решение на тази система е частен случай на тази субституция.

Доказателство. Да означим за краткост тази субституция с s. Тъй като тя променя единствено променливите x₁,x₂,…,x_n, които не се срещат в термовете τ₁,τ₂,…,τ_n, то x_is=τ_i и τ_is=τ_i. Следователно s е решение на разглежданата система.

Нека s' е произволно решение на тази система. Ще докажем, че s'=ss', от където ще следва, че s' е частен случай на s. За целта е достатъчно да покажем, че xs'=xss' за произволна променлива x.

Наистина, ако x=x_i за някое i, то xs'=x_is'=τ_is'=x_iss'=xss', защото субституцията s' е решение на уравнението x_i=τ_i и x_is=τ_i.

Ако пък променливата x не е равна на никоя от променливите x₁,x₂,…,x_n, то xs=x, следователно xs'=xss'.  □

Ж) Следствие. Нека Γ={τ₁,τ₂,…,τ_n} е произволно множество от изрази и системата {τ₁=τ₂,τ₂=τ₃,…,τ_n-1=τ_n} е еквивалентна на система от вида {x₁=σ₁,x₂=σ₂,…,x_m=σ_m}, в която всяко уравнение е решаващо. Тогава субституцията {x₁/σ₁,…,x_m/σ_m} е най-общ унификатор за Γ.

Доказателство. Да означим за краткост тази субституция с s. Тя е унификатор за Γ, тъй като от предходното твърдение следва, че s е решение на система, която е еквивалентна на {τ₁=τ₂,τ₂=τ₃,…,τ_n-1=τ_n}.

Нека s' е произволен унификатор на Γ. Тогава s' е решение на {τ₁=τ₂,τ₂=τ₃,…,τ_n-1=τ_n} и значи също и на {x₁=σ₁,x₂=σ₂,…,x_m=σ_m}. В такъв случай отново от предходното твърдение следва, че s' е частен случай на s.  □

И) Да дефинираме специален вид преобразования на системи, които ще наричаме решаващи преобразования.

Първо решаващо преобразование:

Ако в системата има уравнение от вида τ=x, където термът τ не е променлива, то заместваме това уравнение с x=τ.

Второ решаващо преобразование:

Ако в системата има уравнение от вида x=x, където x е променлива, то отстраняваме това уравнение от системата.

Трето решаващо преобразование:

Ако в системата има уравнение от вида f(τ₁,…,τ_n)=f(σ₁,…,σ_n), то заместваме това уравнение с уравненията τ₁=σ₁,…,τ_n=σ_n.

Четвърто решаващо преобразование:

Ако в системата има уравнение от вида x=τ, което не е решаващо, но променливата x не се среща в терма τ, то заместваме навсякъде в останалите уравнения променливата x с τ.

Й) Твърдение. Ако приложим решаващо преобразование към система, то получаваме система, еквивалентна на първоначалната.

Доказателство. Твърдението е очевидно по отношение на решаващите преобразования от първи и втори вид.

Ако е било приложено решаващо преобразование от трети вид за уравнението f(τ₁,…,τ_n)=f(σ₁,…,σ_n), то също няма нищо сложно – коя да е субституция е решение на това уравнение тогава и само тогава, когато е решение на всяко от уравненията τ₁=σ₁,…,τ_n=σ_n.

Нека е било приложено решаващо преобразование от четвърти вид за уравнението x=τ. Ако субституцията s е решение на системата (без значение дали преди или след преобразованието), то xs=τs. Това показва, че σs=σ[x/τ]s за произволен терм σ и значи s или е решение на системата както преди, така и след преобразованието, или s не е решение на системата нито преди, нито след преобразованието.  □

К) Твърдение. Ако към система не може да бъде приложено нито едно решаващо преобразование, то или всички уравнения в тази система са решаващи, или тя няма решение.

Доказателство: Да допуснем, че към система не може да бъде приложено нито едно решаващо преобразование, но въпреки това тя съдържа уравнение, което не е решаващо. Щом не може да бъде приложено никое решаващо преобразование, то това уравнение не може да бъде нито от вида x=x, нито от вида τ=x, където τ не е променлива, нито от вида f(τ₁,…,τ_n)=f(σ₁,…,σ_n), нито пък от вида x=τ, където x не се среща в τ. Следователно то има един от следните два вида: или x=τ, където променливата x се среща в τ, или f(τ₁,…,τ_n)=g(σ₁,…,σ_m), където f и g са различни функционални символи. Но никое уравнение от този вид не може да има решение.  □

Л) Сега да разгледаме следния процес. Започваме с произволна система. На всяка стъпка прилагаме някое решаващо преобразование. Ако в даден момент това се окаже невъзможно, то или всяко уравнение от системата е станало решаващо, или системата няма решение. Въпросът е какво да правим, ако се окаже възможно да прилагаме безброй много пъти решаващи преобразования. За щастие следващото твърдение показва, че това не е възможно.

М) Твърдение. Към никоя система не може да се прилагат безброй много пъти решаващи преобразования.

Доказателство. Да допуснем, че има система, към която можем да прилагаме безброй много пъти решаващи преобразования.

Да забележим, че ако системата е решена относно променлива x, то и след прилагането на някое решаващо преобразование тя остава решена относно x. От друга страна след прилагането на четвъртото решаващо преобразование броят на променливите, относно които системата е решена, се увеличава с един. Тъй като в системата се срещат само краен брой променливи, ясно е, че няма как този брой да се увеличава безброй много пъти. Следователно четвъртото решаващо преобразование може да се прилага само краен брой пъти. След като приложим четвъртото решаващо преобразование за последен път получаваме система, към която можем да прилагаме безброй много пъти решаващи преобразования, никое от които обаче не е от четвърти вид.

Сега да забележим, че решаващите преобразования от първи, втори и трети вид не увеличават броя на срещанията на функционални символи в системата. От друга страна прилагането на решаващо преобразование от трети вид със сигурност намалява този брой. Ясно е, че това няма как да става безброй много пъти, следователно третото решаващо преобразование може да се прилага само краен брой пъти. След като го приложим за последен път, получаваме система, към която можем да прилагаме безброй много пъти решаващи преобразования, всяко от които е от първи или втори вид. Самата дефиниция на преобразованията от първи и втори вид обаче показва, че това е невъзможно.  □