Лема за резолюция. Нека имаме равенствата D₁=D₁ўИ{L₁},D₂=D₂ўИ{L₂}, където D₁, D₁ў,D₂,D₂ў са дадени дизюнкти, а L₁ и L₂ са взаимно противоположни литерали. При тези предположения винаги, когато двата дизюнкта D₁ и D₂ са верни в дадена структура при дадена оценка на променливите, дизюнктът D₁ўИD₂ў също е верен в тази структура при дадената оценка на променливите.

    Доказателство. Нека S и v са съответно структура и оценка в нея на променливите и нека D₁ и D₂ са верни в S при оценката v. Тогава някой литерал от D₁ е верен в S при оценката v и някой литерал от D₂ също е верен в S при оценката v. Първият от тези два литерала принадлежи на D₁ў или съвпада с L₁, а вторият от тях принадлежи на D₂ў или съвпада с L₂. Не е възможно обаче едновременно първият от двата литерала да съвпада с L₁, а вторият да съвпада с L₂, защото тогава би се оказало, че и L₁, и L₂ са верни в S при оценката v, а това е невъзможно. Следователно първият от двата разглеждани литерала принадлежи на D₁ў или вторият от тях принадлежи на D₂ў и значи някой от тях ще бъде литерал от D₁ўИD₂ў, верен в S при оценката v.  _ї

    Следствие. При предположенията на горната лема, ако двата дизюнкта D₁ и D₂ са тъждествено верни в дадена структура, то и дизюнктът D₁ўИD₂ў е тъждествено верен в тази структура.

    Нека са дадени два дизюнкта D₁ и D₂. Един дизюнкт D ще наричаме тяхна непосредствена резолвента, ако съществуват литерал L₁ от D₁ и литерал L₂ от D₂, такива, че единият от тези два литерала е атомарна формула, другият е нейното отрицание и е в сила равенството D=(D₁\{L₁})И(D₂\{L₂}) (ясно е, че ако в такъв случай положим D₁ў=D₁\{L₁},D₂ў=D₂\{L₂}, то ще бъдат изпълнени предположенията на лемата за непосредствената резолюция).

    Пример 1. За всеки три атомарни формули A, B и C, където A е различна и от B, и от C, дизюнктът {B,ШC} е непосредствена резолвента на дизюнктите {A,B} и  {ШA,ШC} (в специалния случай, когато B=C, споменатата непосредствена резолвента на {A,B} и  {ШA,ШC} е всъщност дизюнктът {B,ШB}, а една друга тяхна непосредствена резолвента в този случай ще бъде дизюнктът {A,ШA}).

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

    Пример 2. Дизюнктите (2) и (3) от пример 1 от предходния въпрос имат непосредствена резолвента {Шodd(X),even(succ(X))}, а дизюнктите (2) и (4) от същия пример имат непосредствена резолвента {Шeven(X),odd(succ(X))}. Значи и тези два нови дизюнкта са тъждествено верни в структурата S от въпросния пример (това разбира се лесно се вижда и непосредствено, тъй че настоящият пример е само с илюстративна цел).

    Един дизюнкт ще наричаме резолвента на два дадени дизюнкта D₁ и D₂, ако той е непосредствена резолвента на някой частен случай на D₁ и някой частен случай на D₂. Тъй като всеки дизюнкт е свой частен случай (тъждествената субституция го преобразува в самия него), ясно е, че ако един дизюнкт е непосредствена резолвента на два дадени дизюнкта, той е и тяхна резолвента. Лесно се вижда, че обратното не е вярно.

    Пример 3. Нека D₁={p(a,Y)},D₂={Шp(X,b)},  където p е двуместен предикатен символ, a и b са константи, а X и Y са променливи. Тогава празният дизюнкт е резолвента на D₁ и D₂, защото е непосредствена резолвента на дизюнктите {p(a,b)} и {Шp(a,b)}, а те са частни случаи съответно на D₁ и на D₂. От друга страна D₁ и D₂ очевидно нямат непосредствена резолвента.

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

    Пример 4. Ще покажем, че дизюнктът (1) от пример 1 от предходния въпрос е тъждествено верен не само в структурата, разгледана там, но и във всяка структура, в която са тъждествено верни дизюнктите (2), (3) и (4) от същия пример. Ще направим това, като покажем, че (1) може да се получи от (2), (3) и (4) чрез двукратно образуване на резолвента. И наистина, да си образуваме първо частния случай на (2), който се получава с помощта на субституцията [succ(X)=:X]. Това е дизюнктът

    На запазването на тъждествената вярност при всяко образуване на резолвента се основава тъй нареченият метод на резолюцията, предложен от Джон Алън Робинсън (John Alan Robinson). Ще опишем накратко идеята на метода, без да се впускаме в подробностите на неговото прилагане (например няма да се спираме на използването  на техниката на унификацията при прилагането му, с която техника ще се занимаем по-късно).

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

    Пример 5. От казаното в пример 4 е ясно, че дизюнктът (1) от пример 1 от предходния въпрос е резолвентно изводим от множеството, състоящо се от дизюнктите (2), (3) и (4) от същия пример.

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

    Едно множество от дизюнкти се нарича изпълнимо, ако съществува структура, в която са тъждествено верни всички дизюнкти от това множество. Методът на резолюцията, предложен от Робинсън, служи за изследване на изпълнимостта на множества от дизюнкти. Накратко казано, този метод свежда въпроса дали е изпълнимо дадено множество от дизюнкти към въпроса дали от това множество е резолвентно изводим празният дизюнкт. А именно, в сила е следният критерий за изпълнимост: едно множество от дизюнкти е неизпълнимо точно тогава, когато от него е резолвентно изводим празният дизюнкт. С това, което сме направили дотук, лесно можем да докажем едната половина на критерия за изпълнимост - ако от едно множество от дизюнкти е резолвентно изводим празният дизюнкт, то това множество е неизпълнимо. И наистина, да допуснем, че от дадено множество от дизюнкти е резолвентно изводим празният дизюнкт и въпреки това множеството е изпълнимо. Тогава ще съществува структура, в която са тъждествено верни всички дизюнкти от даденото множество, а значи и всички дизюнкти, резолвентно изводими от него. Това обаче е невъзможно, защото празният дизюнкт, за който допуснахме, че е резолвентно изводим от даденото множество, не е верен в никоя структура при никоя оценка.

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

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

    Пример 6. Нека се интересуваме дали е изпълнимо множеството от двата дизюнкта D₁ и D₂ от пример 3. Там показахме, че празният дизюнкт е резолвента на въпросните два дизюнкта. Следователно той е резолвентно изводим от {D₁,D₂} и значи то е неизпълнимо.

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

   Пример 8. Неизпълнимостта на  множеството от пример 7 може да се покаже и чрез други начини на установяване на резолвентната изводимост на празния дизюнкт от това множество. Някои от тях имат предимството, че всички нови дизюнкти, получени преди да се стигне до празния, съдържат само по един литерал. Например бихме могли да работим така: първо образуваме резолвентата {p(a)} на елементите {p(X),q(X)} и {Шq(a)} на даденото множество. След това образуваме резолвентата {Шr(a)}на така получения дизюнкт и елемента {Шp(X),Шr(X)} на даденото множество. Накрая от нея и от от дизюнкта {r(a)} получаваме празния дизюнкт.

    Пример 9. В пример 1 от предходния въпрос беше отбелязано, че никой от двата дизюнкта {even(X)} и {odd(X)} не е тъждествено верен в разглежданата там структура S. Интересно е, че никой от тях не е тъждествено верен и в коя да е структура, в която са тъждествено верни дизюнктите (2), (3), (4) от въпросния пример. Ще покажем това за дизюнкта {even(X)}, а за другия нещата са аналогични. Да допуснем, че дизюнктът {even(X)} е тъждествено верен в някоя структура, в която са тъждествено верни споменатите дизюнкти (2), (3), (4). Тогава тези три дизюнкта заедно с дизюнкта {even(X)} ще образуват изпълнимо множество. С помощта на метода на резолюцията ние ще покажем обаче, че това не е така. И наистина, дизюнктът {even(X)} има с дизюнкта (2) непосредствена резолвента {Шodd(X)}, а тя пък има с дизюнкта (4) непосредствена резолвента {odd(succ(X))}. Така получените два дизюнкта очевидно имат за резолвента празния дизюнкт (това показва, че даже и по-малкото множество, състоящо се от дизюнктите (2) и (4) и дизюнкта {even(X)}, е неизпълнимо).

    Забележка. В днешно време са налице няколко компютърни програми, позволяващи решаване на сложни логически задачи с помощта на метода на резолюцията. Такава е например програмата Gandalf, създадена от Tanel Tammet (една нейна версия от 1997 г., към която има и ръководство, може да работи в MS-DOS прозорец на Windows).
 

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

Previous  Next  Contents