Предикатска логика¶

У претходном поглављу смо видели да се исказна логика може успешно примењивати у ситуацијама у којима је природно било моделовати проблем тако да се траже решења која задовољавају неке услове над коначним скупом променљивих које имају вредности или 0 или 1 (променљиве могу бити или тачне или нетачне). На пример, код загонетке Судоку свако поље може бити променљива чија је вредност од 1 до 9, међутим, да бисмо дошли до исказног модела, увели смо нове променљиве које (по једну променљиву за свако поље и сваку вредност од 1 до 9) и те променљиве представљају појединачне исказе (који могу бити или тачни или нетачни). Ово има смисла када је скуп вредности коначан (и релативно мали) и када нисмо вршили никакве променљиве над бројевним вредностима. Исказна логика је сасвим природна за моделовање хардвера (где се природно ради са променљивима које имају само вредности 0 или 1) и SAT решавачи се интензивно примењују у дизајну и верификацији хардвера.

Друге примене (пре свега оне које нису над коначним доменима) захтевају богатије логике и другачије механизме закључивања.

Исказна логика не разматра унутрашњу структуру исказа. Исказ се представља словом (исказном променљивом) и не анализира се како је он изграђен нити шта говори (само се анализирају могућности да буде тачан и да буде нетачан). Са друге стране, у предикатској логици разматрамо како се искази формирају. Сваки исказ говори о својству неког објекта или о вези између нека два или више објеката. На пример, исказ „Број 7 је прост“ говори да број 7 има својство је прост број, исказ „Пера је Миленин отац“ говори о односу између Пере и Милене, док исказ „Тачка А се налази између тачака B и C“ говори о односу између три тачке. Дакле, \(\mathrm{prost}(x)\), \(\mathrm{је\_otac\_od}(x, y)\), \(\mathrm{između}(x, y, z)\) означавају неке односе тј. релације између објеката. Релација обухвата неколико објеката (видели смо пример унарне, бинарне и тернарне релације) и исказ да су објекти у релацији може бити тачан или нетачан (број је или прост или није, неко је нечији отац или није, тачка је између неке две тачке или није). Дакле, сваки исказ подразумева да се говори о некој релацији између објеката.

Објекти могу бити конкретни објекти, који се означавају константама. У прва два примера објекти су били константе (на пример, 7 означава неки конкретан број, а Пера и Милена неке конкретне особе). У трећем примеру су уместо константи употребљене променљиве (нису у питању константе, јер није баш унапред јасно на које три тачке се односе \(A\), \(B\) и \(C\)). Као што ћемо касније видети, да бисмо могли одредити истинитосну вредност таквих исказа, морамо знати вредности променљивих које се у њима јављају (док не знамо на које тачке се односе имена \(A\), \(B\) и \(C\) не можемо знати да ли је исказ тачан).

Искази могу говорити и о објектима који су добијени од неких једноставнијих објеката применом неких функција или операција. На пример, „Следбеник броја 6 је прост“, „Збир бројева 3 и 5 је паран“, „Перин отац је Миленин деда“. У овим примерима \(\mathrm{sledbenik}(x)\), \(\mathrm{zbir}(x, y)\) tj. \(x + y\) и \(\mathrm{otac\_od}(x)\) су функције које примају неке објекте и враћају неке друге објекте. На пример, функција следбеник прима број 6 и враћа број 7. Обратимо пажњу на разлику између функције \(\mathrm{otac}\) и релације \(\mathrm{je\_otac\_od}\). Када смо рекли „Перин отац“ применили смо функцију која прими особу „Пера“ и врати особу (његовог оца). Када смо рекли „Пера је Миленин отац“ применили смо релацију која прима две особе и враћа тачно ако и само ако је прва особа отац од друге.

Функције примају објекте и враћају објекте. Релације примају објекте, а враћају тачно или нетачно.

Применом функција на константе, променљиве и резултате других функција добијамо изразе (кажемо термове). Сваки исказ (говорићемо и атомичка формула) се добија применом релације на неке термове, тј. тако што се крене од неких константи или променљивих, на њих се примењују функције (угнежђене на произвољан начин) и на крају се на добијене термове примени једна релација. Пошто је говорни језик непрецизан, у математици користимо прецизнији запис, који подразумева да смо се у старту договорили којим симболима означавамо константе, функције и релације. Да бисмо формално могли да запишемо неки исказ, тј. атомичку формулу, потребно је да знамо језик (кажемо и сигнатуру) – списак симбола којима записујемо константе, функције и релације. Исказе које смо раније анализирали у математичком запису можемо представити следећим атомичким формулама (при чему смо језик уводили постепено).

Када се применом функција и релација добију искази, они се даље комбинују истим везницима као и у исказној логици. На пример, „Број 7 је непаран прост број“ се записује формулом (не више атомичком)

Ако се знају истинитосне вредности исказа који су повезани везником, може се одредити и вредност сложеног исказа (на потпуно исти начин као у исказној логици).

Веома важан начин грађења сложених исказа у предикатској логици је уз помоћ квантификатора. Они су у тесној вези са променљивама које учествују у исказима. Основни квантификатори су егзистенцијални квантификатор „постоји“ (\(\exists\)) и универзални квантификатор „за сваки“ (\(\forall\)). На пример, исказ \(x < 1\) садржи слободну променљиву \(x\) и не можемо знати његову истинитосну вредност док не знамо вредност те променљиве. Са друге стране, на овај исказ можемо применити неки квантификатор и тиме добити исказе \((\exists x)(x < 1)\) и \((\forall x)(x < 1)\). Ови искази више не садрже слободне променљиве (променљива \(x\) је у оба случаја везана квантификатором) и њихова истинитосна вредност се може одредити без познавање конкретне вредности променљиве \(x\) (квантификатори кодирају знање о вредностима исказа \(x < 1\) за разне вредности променљиве \(x\) – универзални квантификатор представља одређено уопштење конјункције, а егзистенцијални дисјункције). Ипак, да бисмо могли одредити истинитосне вредности ових исказа, морамо још знати домен могућих вредности променљиве \(x\). Свака квантификација подразумева да знамо које су све могуће вредности променљиве. Некада је то имплицитно јасно и подразумева се из контекста (на пример, ако је формула у делу књиге о природним бројевима, подразумеваћемо да \(x\) може бити било који природан број), а некада је потребно бити пажљив и експлицитно нагласити домен променљивих.

• Формула \((\forall x)(x < 1)\) ће бити нетачна без обзира на домен, јер том домену мора припадати и константа 1, а не важи да је \(1 < 1\) (наиме, уобичајено је да се подразумева да постоји јединствен домен у ком се налазе сви објекти, па и објекти који представљају константе које се јављају у формулама).

• Формула \((\exists x)(x < 1)\) ће бити нетачна у домену природних бројева (јер се обично подразумева да је 1 најмањи природан број), а тачна у домену целих бројева (као и рационалних, реалних, итд.).

Дакле, да би се могла одредити истинитосна вредност произвољне формуле, потребно је да неколико услова буде испуњено.

• Ако формула садржи слободне променљиве (променљиве које нису под дејством квантификатора), њену истинитосну вредност је могуће одредити само у односу на неке конкретне вредности тих променљивих (кажемо вредност при некој валуацији променљивих). Такве формуле се обично избегавају и у запису математичких тврђења се користе искључиво формуле без слободних променљивих (тзв. реченице). Истинитосна вредност реченица не зависи од вредности, тј. валуације променљивих. Некада се усваја договор да се користе само реченице, али да се неки квантификатори могу изоставити – када год је изостављен квантификатор, подразумева се универзална квантификација. Да не би долазило до забуне, ми ћемо увек експлицитно записивати све квантификаторе.

• Потребно је знати домен у ком се налазе објекти о којима формула говори. У том (јединственом) домену налазе се све константе и све променљиве узимају вредност из тог домена.

• Морамо знати шта означавају сви симболи који се јављају у запису формуле: симболи константи, симболи релација, симболи функција. Када се формула напише она је само синтаксички објекат и да бисмо одредили њену истинитосну вредност, потребно је да му некако доделимо и значење, тј. семантику. Кажемо да је потребно да знамо интерпретацију сваког симбола. На пример, ако у формули пише \((\forall x)(x \star 1 = x)\), морамо знати коју операцију означава симбол \(\star\) да бисмо разумели о чему формула говори и одредили њену истинитосну вредност (ако је у питању операција множења, формула је тачна (нпр. у домену реалних бројева), а ако је у питању операција сабирања, формула је нетачна). Неки симболи су стандардни и њихова интерпретација се подразумева (на пример, у претходном примеру смо подразумевали да симбол \(<\) означава релацију поретка бројева). Ако то није случај, неопходно је прецизирати интерпретацију сваког симбола у запису формуле (симболе константи интерпретирамо објектима из домена, функцијске симболе функцијама у том домену, а релацијске симболе релацијама у том домену).

У предикатској логици првог реда квантификатори се примењују искључиво на променљиве. У предикатској логици вишег реда допуштено је да се квантификатори примене и на релацијске и функцијске симболе. На пример, наредна формула је исправна формула логике вишег, али не и логике првог реда, јер је на десној страни квантификатор примењен на функцијски симбол (\(\exists f\)).

Синтакса и семантика предикатске логике се могу и мало прецизније дефинисати.

Дефинишимо прво синтаксу. Крећемо од језика \(L\), који се састоји од скупа функцијских и скупа релацијских симбола. Сваки симбол има своју арност. Функцијски симболи арности 0 се називају константе, а релацијски симболи арности 0 логичке константе (њих увек обележавамо са \(\top\) и \(\bot\)).

Термови се рекурзивно дефинишу следећом контекстно слободном граматиком:

\[\begin{split}\begin{eqnarray*} term &\rightarrow& x, \quad x\ \textrm{je promenljiva}\\ term &\rightarrow& f(term_1, \ldots, term_n), \quad f\ \textrm{je funkcijski simbol arnosti}\ n \end{eqnarray*}\end{split}\]

Формуле се дефинишу на следећи начин:

\[\begin{split}\begin{eqnarray*} \mathit{formula} &\rightarrow& \top\\ \mathit{formula} &\rightarrow& \bot\\ \mathit{formula} &\rightarrow& P(term_1, \ldots, term_n), \quad P\ \textrm{je relacijski simbol arnosti}\ n\\ \mathit{formula} &\rightarrow& \neg \mathit{formula}\\ \mathit{formula} &\rightarrow& \mathit{formula} \wedge \mathit{formula}\\ \mathit{formula} &\rightarrow& \mathit{formula} \vee \mathit{formula}\\ \mathit{formula} &\rightarrow& \mathit{formula} \Rightarrow \mathit{formula}\\ \mathit{formula} &\rightarrow& \mathit{formula} \Leftrightarrow \mathit{formula}\\ \mathit{formula} &\rightarrow& (\forall x)(\mathit{formula})\\ \mathit{formula} &\rightarrow& (\exists x)(\mathit{formula})\\ \mathit{formula} &\rightarrow& (\mathit{formula})\\ \end{eqnarray*}\end{split}\]

Дефинишимо сада семантику. Структура језика \(L\) (скр. \(L\)-структура) је уређени пар \((D, I)\) где је \(D\) непразан скуп (домен), а \(I\) функција интерпретације која сваком \(n\)-арном функцијском симболу \(f\) језика \(L\) додељује функцију \(f^d : D^n \rightarrow D\), а сваком \(n\)-арном релацијском симболу \(f\) језика \(L\) додељује релацију \(P^d \subseteq D^n\). Валуација \(v\) пресликава променљиве у елементе домена \(D\).

Тада се може дефинисати функција \(T_{D, I, v}(t)\) која израчунава вредност термова, тј. сваки терм пресликава у елементе домена \(D\). Дефиниција је рекурзивна у односу на структуру терма.

• \(T_{D, I, v}(x) = v(x)\)

• \(T_{D, I, v}(f(t_1, \ldots, t_n)) = f^d(T_{D, I, v}(t_1), \ldots, T_{D, I, v}(t_1))\)

Затим се може дефинисати функција \(I_{D, I, v}(F)\) којом се одређује истинитосна вредност формуле. Њена рекурзивна дефиниција наслеђује велики број случајева из исказне логике, тако да ћемо приказати само оне који су специфични за предикатску логику.

• \(I_{D, I, v}(P(t_1, \ldots, t_n)) = 1\) ако и само ако важи \(P^d(T_{D, I, v}(t_1), \ldots, T_{D, I, v}(t_1))\)

• \(I_{D, I, v}((\forall x)F) = 1\) ако и само ако за сваку валуацију \(v'\) која се поклапа са \(v\) на свим променљивим, осим на \(x\) важи \(I_{D, I, v'}(F) = 1\) (другим речима, за било који избор вредности \(x\) формула \(F\) је тачна за ту вредност \(x\)).

• \(I_{D, I, v}((\exists x)F) = 1\) ако и само ако постоји валуација \(v'\) која се поклапа са \(v\) на свим променљивим осим на \(x\) и важи \(I_{D, I, v'}(F) = 1\) (другим речима, постоји вредност \(x\) таква да је формула \(F\) тачна за ту вредност \(x\)).

Доказује се да за реченице (формуле без слободних променљивих) функција \(I_{D, I, v}\) враћа исту вредност за све валуације \(v\), тј. да истинитосна вредност реченица не зависи од валуације. Зато се за реченице разматра функција \(I_{D, I}\). Кажемо да је \(L\)-структура модел реченице \(F\) ако и само ако важи \(I_{D, I}(F) = 1\). Ово обележавамо и са \((D, I) \vDash F\). У супротном, \(L\)-структура је контра-модел реченице \(F\).

Размотримо следеће формуле и покушајмо да одредимо њихову истинитосну вредност:

Јасно је да у првој формули не знамо шта означава бинарни релацијски симбол \(\rho\), а да у другој не знамо шта означава унарни релацијски симбол \(P\), као и да ни за једну формулу не знамо домен. Ако у првој формули интерпретирамо симбол \(\rho\) релацијом \(<\) формула говори да од сваког броја постоји већи број и тачна је у свим уобичајеним бројевним доменима (природним бројевима, целим, рационалним, реалним). Ако симбол \(\rho\) релацијом \(<\) формула говори да од сваког броја постоји мањи број и она није тачна у домену природних бројева, а јесте тачна у домену целих, рационалних и реалних бројева. Дакле, истинитосна вредност прве формуле зависи од интерпретације симбола \(\rho\) и од домена на који се односи. Та формула има и модел (може бити тачна) и контра-модел (може бити нетачна). Формуле које имају модел зовемо задовољиве, а које имају контра-модел порециве.

Са друге стране, друга формула је тачна на које год својство се односи симбол \(P\) и који год домен да посматрамо (подразумевамо да увек разматрамо непразне домене). Такве формуле, дакле, не зависе од математичких појмова на које се односе већ су тачне искључиво на основу своје логичке структуре. За такве формуле кажемо да су универзално ваљане (или краће, ваљане). Ваљане формуле су на неки начин уопштење појма таутологије и исправност закључивања се може свести на испитивање ваљаности одређених формула. Појам логичке последице и логички еквивалентних формула се у предикатској логици дефинише на исти начин као и у исказној и испитивање ових односа између формула (који су основа исправног закључивања) се своди на испитивање ваљаности одговарајућих формула.

Ако, на пример, кренемо од претпоставки „Сви Грци су људи“ и „Сви људи су смртни“, тада можемо да изведемо закључак „Сви Грци су смртни“. Тврдимо, дакле, да је формула

логичка последица формула

Ово је чувени први Аристотелов силогизам (правило исправног закључивања). Овај закључак јесте исправан пошто је следећа формула ваљана.

Кључни проблем је то што је испитивање ваљаности, тј. задовољивости у предикатској логици неупоредиво тежи проблем него испитивање исказне таутологичности, тј. задовољивости и у општем случају не постоји алгоритам који би могао да испита ваљаност произвољне формуле предикатске логике (и доказано је да такав алгоритам не само да није тренутно измишљен, него не може ни да постоји). Постоје алгоритми који успевају да испитају ваљаност неких формула, али они су често неефикасни, треба им пуно времена и меморије и не могу да увек дају одговор. Кажемо да је проблем испитивања ваљаности неодлучив. Са друге стране, проблем јесте полу-одлучив, што значи да постоје алгоритми који (под претпоставком да им се да довољно времена и меморије) за било коју ваљану формулу у неком тренутку могу да утврде да је ваљана. Међутим, за формуле које нису ваљане ти алгоритми раде бесконачно, никада се не заустављајући и никада не утврђујући да дата формула није ваљана.

Трећа формула \((\forall x)(P(x) \wedge \neg P(x))\) је незадовољива јер је нетачна у свим доменима и за све могуће интерпретације симбола \(P\). Она нема ниједан модел (сваки домен и интерпретација су јој контра-модел).

Данас се за испитивање ваљаности логичких формула користе аутоматски доказивачи теорема (енгл. automated theorem provers, ATP). Њихову употребу смо описали у посебном поглављу овог курса, па у неком тренутку можете покушати да их употребите да докажете неку теорему (као пример, навели смо једну интересантну детективску загонетку).

Метода резолуције¶

Најпознатија техника за испитивање ваљаности формула јесте метода резолуције и она представља основу великог броја доказивача теорема (програма који се користе у математици и верификацији софтвера), али и теоријску основу логичког програмирања (пре свега кроз језик Prolog). Циљ овог поглавља је да вам да неки наговештај како ова метода функционише, а не да детаљно научите све њене детаље.

У питању је метода побијања, што значи да се ваљаност доказује тако што се покаже да је негација формуле незадовољива. Слично као што су се SAT решавачи примењивали на формуле у КНФ, тако се метода резолуције примењује превођењем формуле у клаузалну форму.

• Први корак превођења у ту форму је да се формула доведе у тзв. нормалну форму prenex, тј. облик \(Q_1\ x_1.\ \ldots\ Q_n\ x_n.\ F\), где су \(Q_i\) квантификатори, а формула \(F\) не садржи квантификаторе.

• Други корак је да се тело формуле (део испред извучених квантификатора) преведе у КНФ.

• На крају се примењује ослобађање егзистенцијалних квантифитора (корак познат као Сколемизација).

Крећемо од негације наше формуле и преводимо је у клаузалну форму. Наша формула има облик \(\phi_1 \wedge \phi_2 \Rightarrow \theta\) (две премисе имплицирају закључак), па је њена негација логички еквивалентна формули \(\phi_1 \wedge \phi_2 \wedge \neg \theta\). Превођење у клаузалну форму вршимо, између осталог, применом логичких еквиваленција које смо навели у опису превођења формуле у КНФ. Додатно примењујемо и следећа правила која се односе на квантифкаторе:

\[\begin{split}\neg (\forall x)(P(x)) \equiv (\exists x)(\neg P(x))\\ \neg (\exists x)(P(x)) \equiv (\forall x)(\neg P(x))\\\end{split}\]

Циљ нам је да све квантификаторе извучемо напоље и да добијемо нормалну форму prenex. За превођење користимо следеће логичке еквиваленције:

\[\begin{split}\begin{eqnarray*} (\forall x)(A) \wedge B &\equiv& (\forall x)(A \wedge B)\\ (\forall x)(A) \vee B &\equiv& (\forall x)(A \vee B)\\ B \wedge (\forall x)(A) &\equiv& (\forall x)(B \wedge A)\\ B \vee (\forall x)(A) &\equiv& (\forall x)(B \vee A)\\ (\exists x)(A) \wedge B &\equiv& (\exists x)(A \wedge B)\\ (\exists x)(A) \vee B &\equiv& (\exists x)(A \vee B)\\ B \wedge (\exists x)(A) &\equiv& (\exists x)(B \wedge A)\\ B \vee (\exists x)(A) &\equiv& (\exists x)(B \vee A) \end{eqnarray*}\end{split}\]

при чему, ако се променљива \(x\) јавља слободна у \(B\), потребно је да је преименујемо у формули \((\forall x)(A)\), тј. \((\exists x)(A)\). Да бисмо уштедели на броју квантификатора, можемо да користимо и следеће формуле.

\[\begin{split}\begin{eqnarray*} (\forall x)(A) \wedge (\forall x)(B) &\equiv& (\forall x)(A \wedge B)\\ (\exists x)(A) \vee (\exists x)(B) &\equiv& (\exists x)(A \vee B)\\ \end{eqnarray*}\end{split}\]

Међутим, обратите пажњу на то да наредне две формуле нису исправне (квантификатор „за сваки“ се слаже са конјункцијом, али не и са дисјункцијом, док се квантификатор „постоји“ слаже само са дисјункцијом, а не и са конјункцијом.

\[\begin{split}\begin{eqnarray*} (\forall x)(A) \vee (\forall x)(B) &\equiv& (\forall x)(A \vee B)\\ (\exists x)(A) \wedge (\exists x)(B) &\equiv& (\exists x)(A \wedge B)\\ \end{eqnarray*}\end{split}\]

Вратимо се на формулу из нашег примера. Њена негација је еквивалентна формули

\[\begin{split}(\forall x)(\mathrm{grk}(x) \Rightarrow \mathrm{covek}(x))\ \wedge \\ (\forall x)(\mathrm{covek}(x) \Rightarrow \mathrm{smrtan}(x)) \wedge\\ \neg (\forall x)(\mathrm{grk}(x) \Rightarrow \mathrm{smrtan}(x))\end{split}\]

Ослобађамо се унутрашњих импликација и увлачимо негацију.

\[\begin{split}(\forall x)(\neg \mathrm{grk}(x) \vee \mathrm{covek}(x))\ \wedge \\ (\forall x)(\neg \mathrm{covek}(x) \vee \mathrm{smrtan}(x))\ \wedge\\ (\exists x)(\mathrm{grk}(x) \wedge \neg \mathrm{smrtan}(x))\end{split}\]

Извлачимо сада прво егзистенцијални квантификатор на почетак формуле на основу правила \(B \wedge (\exists x)(A) \equiv (\exists x)(B \wedge A)\). Пошто се \(x\) не јавља слободно у делу \(B\), нема потребе за преименовањем, па добијамо:

\[(\exists x)\left((\forall x)(\neg \mathrm{grk}(x) \vee \mathrm{covek}(x))\ \wedge (\forall x)(\neg \mathrm{covek}(x) \vee \mathrm{smrtan}(x))\ \wedge (\mathrm{grk}(x) \wedge \neg \mathrm{smrtan}(x))\right)\]

Извлачимо сада универзални квантификатор истовремено испред две премисе на основу правила \((\forall x)(A) \wedge (\forall x)(B) \equiv (\forall x)(A \wedge B)\) и добијамо:

\[(\exists x)\left((\forall x)\left((\neg \mathrm{grk}(x) \vee \mathrm{covek}(x))\ \wedge (\neg \mathrm{covek}(x) \vee \mathrm{smrtan}(x))\right)\ \wedge (\mathrm{grk}(x) \wedge \neg \mathrm{smrtan}(x))\right)\]

На крају извлачимо универзални квантификатор на почетак тела егзистенцијално квантификованог дела формуле на основу правила \((\forall x)(A) \wedge B \equiv (\forall x)(A \wedge B)\), али пошто се сада променљива \(x\) јавља као слободна у делу \(B\), тј. у делу \(\mathrm{grk}(x) \wedge \neg \mathrm{smrtan}(x)\), вршимо преименовање квантификоване променљиве и добијамо.

\[(\exists x)(\forall x')((\neg \mathrm{grk}(x') \vee \mathrm{covek}(x'))\ \wedge (\neg \mathrm{covek}(x') \vee \mathrm{smrtan}(x'))\ \wedge \mathrm{grk}(x) \wedge \neg \mathrm{smrtan}(x))\]

Добијена формула је логички еквивалентна полазној, и у нормалној форми prenex, при чему је тело формуле (део испред квантификатора) у КНФ.

Наредни корак при превођењу у клаузалну форму је ослобађање од егзистенцијалних квантификатора. То се ради процедуром која се назива Сколемизација (у част логичара Сколема). На тај начин се не добија формула која је еквивалентна полазној, али се добија формула која је еквизадовољива, што је нама довољно (јер ми ваљаност доказујемо тиме што доказујемо да негација полазне формуле није задовољива). Сколемизација се врши тако што се уместо егзистенцијално квантификованих променљивих уводе нове константне.

• Формула \((\exists x)(P(x))\) је еквизадовољива формули \(P(c)\), где је \(c\) нови симбол константе (не сме да се јавља нигде другде у формули).

• Ако је егзистенцијални квантификатор испред једног или више универзалних, онда се уместо константе мора увести функција. На пример, формула \((\forall x)(\exists x)(P(x, y))\) је еквизадовољива формули \((\forall x)P(x, f(x))\), где је \(f\) нови симбол функције (не сме да се јавља негде другде у формули)

Сколемизацијом наше формуле добијамо формулу

\[(\forall x')((\neg \mathrm{grk}(x') \vee \mathrm{covek}(x'))\ \wedge (\neg \mathrm{covek}(x') \vee \mathrm{smrtan}(x'))\ \wedge \mathrm{grk}(c) \wedge \neg \mathrm{smrtan}(c))\]

Можемо се сада вратити корак назад увлачећи квантификаторе до сваке клаузуле и формулу представити као конјункцију следеће 4 (универзално квантификоване) клаузуле (преименоваћемо и променљиве, ради једноставности):

\[\begin{split}(\forall x)(\neg \mathrm{grk}(x) \vee \mathrm{covek}(x))\\ (\forall x)(\neg \mathrm{covek}(x) \vee \mathrm{smrtan}(x))\\ \mathrm{grk}(c)\\ \neg \mathrm{smrtan}(c)\end{split}\]

Потребно је да докажемо да је овај скуп клаузула незадовољив. То се ради методом резолуције. Пошто смо се ослободили универзалних квантификатора, све преостале променљиве су универзално квантификоване, па се обично приликом примене метода резолуције квантификатори не пишу.

\[\begin{split}\neg \mathrm{grk}(x) \vee \mathrm{covek}(x)\\ \neg \mathrm{covek}(x) \vee \mathrm{smrtan}(x)\\ \mathrm{grk}(c)\\ \neg \mathrm{smrtan}(c)\end{split}\]

Овај скуп клаузула је незадовољив. То можемо видети на следећи начин. Пошто прва клаузула важи за свако \(x\) она важи и за \(x=c\), тј. важи и \(\neg \mathrm{grk}(c) \vee \mathrm{covek}(c)\). Пошто на основу треће клаузуле знамо да важи \(\mathrm{grk}(c)\), мора да важи \(\mathrm{covek}(c)\). Пошто и друга клаузула важи за свако \(x\), она важи и за \(x=c\), тј. важи и \(\neg \mathrm{covek}(c) \vee \mathrm{smrtan}(c)\). Пошто важи \(\mathrm{covek}(c)\) мора да важи \(\mathrm{smrtan}(c)\), међутим, то је у супротности са нашом четвртом клаузулом.

Формално, правило резолуције се примењује тако што се пронађу две клаузуле које садрже неки супротан литерал и затим се у скуп клаузуле дода њихова резолвента, која се добија обједињавањем свих осталих литерала осим тог супротног. Правило резолуције за исказну логику се примењује на клаузуле облика

\[\begin{split}p \vee q_1 \vee \ldots \vee q_m\\ \neg p \vee r_1 \vee \ldots \vee r_n\end{split}\]

и добија се резолвента

\[q_1 \vee \ldots \vee q_m \vee r_1 \vee \ldots \vee r_n.\]

Када год су полазне две клаузуле тачне, тачна је и њихова резолвента (она је њихова логичка последица). Доказ овога је једноставан и остављамо ти га за вежбу. Централна теорема метода резолуције за исказну логику је следећа:

Скуп исказних клаузула је незадовољив ако и само ако се резолвирањем може извести празна клауза (клауза која не садржи ниједан литерал).

Иако би се SAT решавач могао засновати на методу резолуције за исказну логику, SAT решавачи користе друге алгоритме (у којима се ипак резолуција јавља као један од корака).

Правило резолуције за предикатску логику је компликованије, јер литерали нису више само исказна слова, већ атомичке формуле које садрже променљиве. Литерали преко којих се врши резолуција се не разликују само по томе што је један негиран, а други није. Допуштено је да се они могу изједначити процесом унификације, што значи да је допуштено да се променљиве замене произвољним изразима да би се добила иста атомичка формула. На пример, могуће је извршити резолуцију клаузула \(\neg \mathrm{grk}(x) \vee \mathrm{covek}(x)\) и \(grk(c)\). Заиста, \(\mathrm{grk}(x)\) и \(grk(c)\) нису једнаки, али се могу унификовати тиме што се \(x\) замени са \(c\). Након те замене се добија прва клаузула \(\neg \mathrm{grk}(c) \vee \mathrm{covek}(c)\) и сада се може извршити резолуција те инстанциране клаузуле и клаузуле \(grk(c)\) и добити резолвента \(\mathrm{covek}(c)\).

Наведимо још неколико примера унификације.

• Литерали \(\rho(x, f(x))\) и \(\rho(g(y), z)\) се могу унификовати (пошто литерали долазе из различитих клаузула које су засебно универзално квантификоване, увек можемо претпоставити да су им променљиве различито назване). Можемо да заменимо \(x\) са \(g(y)\), а \(z\) са \(f(g(y))\), чиме у оба случаја добијамо \(\rho(g(y), f(g(y)))\).

• Са друге стране, литерали \(\rho(x)\) и \(\sigma(y)\) се не могу унификовати (јер им се разликују релацијски симболи и никаква замена променљивих не може довести до њиховог изједначавања).

• Не могу се унификовати ни литерали \(\rho(f(x))\) и \(\rho(g(x))\), јер им се разликују функцијски симболи на првој позицији (никаквом заменом променљивих \(f\) не може постати исто што и \(g\)).

• Не могу се унификовати ни литерали \(x\) и \(f(x)\), јер шта год да се одабере за \(x\), други литерал ће се разликовати од првог јер ће имати једну додатну примену функције \(f\)

• Литерали \(x\) и \(y\) (две променљиве) се увек могу унификовати.

• Литерали \(f(x, x)\) и \(f(a, b)\), се не могу унификовати. Наиме, променљива \(x\) би истовремено требало да буде замењена и константом \(a\) и константном \(b\), што је немогуће.

Постоји алгоритам који за свака два литерала проверава да ли се могу унификовати и ако могу, проналази најопштији унификатор (замену променљивих).

Резолуција у предикатској логици, дакле, покушава да пронађе два супротна литерала који се могу унификовати и ако успе, примењује унификатор (замену променљивих) на обе клаузуле и након тога као резолвенту у скуп клаузула убацује клаузулу која садржи све остале литерале, осим та два супротна (али инстанциране на основу пронађеног унификатора). Наведимо још један пример примене правила резолуције у предикатској логици. Резолвирајмо следећи пар клаузула:

\[\begin{split}\mathrm{zivotinja}(g(x)) \vee \mathrm{voli}(f(x), x)\\ \neg \mathrm{voli}(y, a) \vee \mathrm{pazi}(y, a)\end{split}\]

Могуће је унификовати формуле \(\mathrm{voli}(f(x), x)\) и \(\neg \mathrm{voli}(y, a)\) тако што се променљива \(x\) замени са \(a\), а променљива \(y\) са \(f(a)\). Након инстанцирања, тј. примене ове замене променљивих добијамо:

\[\begin{split}\mathrm{zivotinja}(g(a)) \vee \mathrm{voli}(f(a), a)\\ \neg \mathrm{voli}(f(a), a) \vee \mathrm{pazi}(f(a), a)\end{split}\]

Сада се може извршити резолуција и добити резолвента:

\[\mathrm{zivotinja}(g(a)) \vee \mathrm{pazi}(f(a), a)\]

У нашем примеру могуће је извршити и резолуцију клаузула

\[\begin{split}\neg \mathrm{grk}(x) \vee \mathrm{covek}(x)\\ \neg \mathrm{covek}(x) \vee \mathrm{smrtan}(x)\\\end{split}\]

чиме би се добила клазула

\[\neg \mathrm{grk}(x) \vee \mathrm{smrtan}(x)\]

Приметимо да правило резолуције на неки начин одговара правилу транзитивности импликације.

Поред правила резолуције потребно је да се допусти и примена правила факторисања, које допушта да се у скуп клаузула дода клаузула која се добија када се у некој полазној клаузули изврши унификација неколико њених литерала. На пример, ако имамо клаузлу \(P(x, f(y)) \vee P(g(z), f(z)) \vee \neg R(f(x), z)\), можемo унификовати њена прва два литерала заменом \(x\) са \(g(z)\) и \(y\) са \(z\) и тиме добити нову клаузулу (фактор полазне) \(P(g(z), f(z)) \vee \neg R(f(g(z)), z)\).

Основна теорема метода резолуције за предикатску логику је следећа:

Скуп клаузула је незадовољив ако и само ако се применом правила резолуције и факторисања из њега може извести празна клаузула.

Правила (бинарне) резолуције и факторисања се могу спојити у једно правило n-арне резолуције које допушта да се истовремено унификује неколико литерала из једне и неколико њима супротних литерала из друге клаузуле.

Главни проблем у имплементацији је навођење резолуције, јер се додавањем резолвенти скуп клаузула веома брзо шири што заузима пуно меморије и успорава извођење нових корисних резолвенти. Научници су годинама радили на осмишљавању стратегија које би што ефикасније усмериле процес резолуције тако да се што пре изведе празна клаузула. Као што смо рекли, ако је полазна формула задовољива, процес резолуције може да траје бесконачно и да се никада не дође до празне клаузуле (програм се тада никада неће зауставити).