Пълнота на метода на резолюцията

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

Ще предполагаме, че е дадена една сигнатура Σ, и за всички дизюнкти, за които не е казано изрично нещо друго, ще смятаме, че са при сигнатура Σ.

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

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

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

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

Ще разгледаме най-напред случая, когато в сигнатурата Σ има поне една константа. Нека Δ° е множеството на всички затворени частни случаи на дизюнктите от Δ. От свеждането на въпроса за съществуване на модел за множество от дизюнкти към същия въпрос за множество от затворени дизюнкти знаем, че щом в Σ има поне една константа и Δ няма модел, множеството Δ° е неизпълнимо. Оттук по лемата, която доказахме преди малко, получаваме, че празният дизюнкт е резолвентно изводим от Δ°. От друга страна обаче лесно е да се убедим, че всеки дизюнкт, резолвентно изводим от Δ°, е затворен частен случай на дизюнкт, резолвентно изводим от Δ. И наистина, за дизюнктите от самото множество Δ° това е ясно от дефиницията на това множество. От друга страна, ако два дизюнкта δ₁ и δ₂ са затворени частни случаи съответно на дизюнкти δ₁ и δ₂, резолвентно изводими от Δ, а трети дизюнкт е резолвента (разбира се непосредствена) на δ₁ и δ₂, той ще бъде резолвента на δ₁ и δ₂, следователно ще бъде резолвентно изводим от Δ и можем да използваме, че той е затворен частен случай на себе си. Като приложим доказаното към празния дизюнкт, получаваме, че той е затворен частен случай на някой дизюнкт, резолвентно изводим от множеството Δ, а въпросният дизюнкт не може да бъде друг освен празен. Значи празният дизюнкт е резолвентно изводим от Δ.

Преминаваме към случая, когато в сигнатурата Σ няма нито една константа. В този случай разглеждаме нова сигнатура Σ⁺, получена от Σ чрез добавяне на една константа α. Дизюнктите от множеството Δ могат да се разглеждат и като дизюнкти при сигнатура Σ⁺, като множеството Δ няма да има модел и сред структурите със сигнатура Σ⁺ (ако би имало такъв, от него щеше да може чрез обедняване да се получи и модел за Δ със сигнатура Σ). Нека Δ° е множеството на всички затворени частни случаи на дизюнктите от Δ при сигнатура Σ⁺, т.е. Δ° се състои от резултатите от замествания на променливите на дизюнктите от Δ със затворени термове при сигнатура Σ⁺. Множеството Δ° отново ще бъде неизпълнимо и лемата, която доказахме, позволява да твърдим, че от Δ° е резолвентно изводим при сигнатура Σ⁺ празният дизюнкт. Оттук ще успеем да заключим, че той е резолвентно изводим от Δ при сигнатура Σ (разбира се, от разглежданията, които направихме в първия случай, е ясно, че празният дизюнкт е изводим от Δ при сигнатура Σ⁺, но това твърдение е по-слабо от онова, което трябва да докажем). За целта избираме една променлива ξ и на всички затворени термове τ, литерали λ и дизюнкти δ при сигнатура Σ⁺ съпоставяме техни образи τ^ξ, λ^ξ и δ^ξ, които са съответно термове, литерали и дизюнкти при сигнатура Σ и са получени, грубо казано, чрез замяна на константата α с променливата ξ. Съпоставянето извършваме с помощта на следните равенства:

α^ξ = ξ;
ω(τ₁,…,τ_n)^ξ = ω(τ₁^ξ,…,τ_n^ξ) за всяко положително цяло число n, всеки n-местен функционален символ ω и всяка n-орка τ₁, …, τ_n от затворени термове при сигнатура Σ⁺;
π^ξ = π за всеки нулместен предикатен символ π;
π(τ₁,…,τ_n)^ξ = π(τ₁^ξ,…,τ_n^ξ) за всяко положително цяло число n, всеки n-местен предикатен символ π и всяка n-орка τ₁, …, τ_n от затворени термове при сигнатура Σ⁺;
not(φ)^ξ = not(φ^ξ) за всяка затворена атомарна формула φ при сигнатура Σ⁺;
δ^ξ = {λ^ξ | λ∈δ} за всеки затворен дизюнкт δ при сигнатура Σ⁺.

След това доказваме следното твърдение: винаги, когато един затворен дизюнкт δ е резолвентно изводим при сигнатура Σ⁺ от множеството Δ°, съответният дизюнкт δ^ξ е частен случай на дизюнкт, резолвентно изводим при сигнатура Σ от множеството Δ. Прилагайки това твърдение в случая, когато δ е празният дизюнкт, получаваме нужното ни заключение за неговата изводимост от Δ при сигнатура Σ. Що се касае до доказателството на въпросното твърдение, основните моменти са два:
1. За дизюнктите от множеството Δ° верността на твърдението се установява, като се докаже, че е в сила равенството δ[ξ₁/θ₁,…,ξ_m/θ_m]^ξ = δ[ξ₁/θ₁^ξ,…,ξ_m/θ_m^ξ] винаги, когато ξ₁, …, ξ_m са различни помежду си променливи, δ е дизюнкт при сигнатура Σ, нямащ променливи, различни от ξ₁, …, ξ_m, а θ₁, …, θ_m са затворени термове при сигнатура Σ⁺ (равенството се доказва, като най-напред последователно се докажат аналогични равенства за термове и за литерали при сигнатура Σ).
2. За да покажем, че верността на твърдението се запазва при образуване на непосредствена резолвента на два затворени дизюнкта при сигнатура Σ⁺, използваме, че (δ \ {λ})^ξ = δ^ξ \ {λ^ξ} за всеки затворен дизюнкт δ при сигнатура Σ⁺ и всеки литерал λ, който му принадлежи (верността на това твърдение следва от обстоятелството, че литералите λ^ξ, съответстващи на различни литерали λ, са различни помежду си, а че това обстоятелство е налице, може да се види, като последователно се докаже, че за всеки затворен терм τ при сигнатура Σ⁺ е в сила равенството τ^ξ[ξ/α] = τ и за всеки затворен литерал λ при сигнатура Σ⁺ е в сила равенството λ^ξ[ξ/α] = λ). _□

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

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