Правило резолюцій

Правило резолюцій — це правило висновування, що сходить до методу доказу теорем через пошук протиріч; використовується в логіці висловлювань і логіці предикатів першого порядку. Правило резолюцій, що застосовується послідовно для списку резольвент, дозволяє відповісти на питання, чи існує у вхідній множині логічих виразів протиріччя. Правило резолюцій запропоновано в 1930 році в докторській дисертації Жака Ербрана для доведення теорем у формальних системах першого порядку. Правило розроблено Джоном Аланом Робінсоном в 1965 році.

Алгоритми доказу виводимості $A\vdash B$, побудовані на основі цього методу, застосовуються в багатьох системах штучного інтелекту, а також є фундаментом, на якому побудовано мову логічного програмування «Пролог».

Логіка висловлень

Правило резолюцій першочергово застосовується до диз'юнктів  — диз'юнкцій пропозиційних змінних чи їх заперечень. Правило застосовується до двох диз'юнктів у випадку, коли вони містять пропозиційні змінні, одна з яких є запереченням другої. Наприклад:

${\frac {a_{1}\lor \ldots \vee a_{i}\vee \ldots \lor a_{n},\quad b_{1}\lor \ldots \vee b_{j}\vee \ldots \lor b_{m}}{a_{1}\lor \ldots \lor a_{i-1}\lor a_{i+1}\lor \ldots \lor a_{n}\lor b_{1}\lor \ldots \lor b_{j-1}\lor b_{j+1}\lor \ldots \lor b_{m}}}$

де $a_{i}$ є доповненням $b_{j}$, (наприклад $a_{i}=x$, а $b_{i}=\lnot x$)

Для можливості використання цього правила необхідно записати формулу у кон'юнктивній нормальній формулі. Довільна формула логіки висловлень еквівалентна деякій формулі цього виду. При записі формули у кон'юнктивній формі кожен диз'юнкт можна подати як множину літералів (пропозиційних формул чи їх заперечень), а саму формулу як множину диз'юнктів. Наприклад формулу:

$\neg p\wedge (q\vee r\vee q)\wedge (\neg r\vee \neg s)\wedge (p\vee s)\wedge (\neg q\vee \neg s)$

можна подати так:

$\{\{\neg p\},\{q,r\},\{\neg r,\neg s\},\{p,s\},\{\neg q,\neg s\}\}$

Також таким чином можна визначити правило резолюцій:

• ${\frac {\{C,p\}\quad \{C',\neg p\}}{\{C,C'\}}}$

Позначимо:

$Res(F)=F\cup \{R\}$, де $R$ диз'юнкт одержаний за правилом резолюцій з деяких диз'юнктів формули $F$ і: Mit $Res^{\star }(F)=\bigcup _{n\in \mathbb {N} }Res^{n}(F)$ об'єднання всіх диз'юнктів одержаних з диз'юнктів формули $F$ за скінченну кількість використань правила резолюцій.

Деяка формула $F$ записана у КНФ є невиконуваною тоді і тільки тоді, коли $\emptyset \in Res^{\star }(F)$. Як наслідок з цього для довільних формул $A_{1},A_{2}\ldots A_{n}$ формула $F$ є логічним наслідком тих формул тоді і тільки тоді, коли $\emptyset \in Res^{\star }(A_{1}\lor A_{2}\lor \ldots \lor A_{n}\lor \lnot F)$. Тобто система формального виводу заснована на правилі резолюцій є коректною і повною.

Приклад

Нехай є формули:

$(P\rightarrow S)$

$(S\rightarrow \neg P)$

$(\neg S\rightarrow P)$

Потрібно довести що:

$(P\rightarrow S),(S\rightarrow \neg P),(\neg S\rightarrow P)\models S$

Спершу приведімо дані формули до кон'юнктивної нормальної форми:

$P\rightarrow S\quad \equiv \quad \neg P\vee S$

$S\rightarrow \neg P\quad \equiv \quad \neg S\vee \neg P$

$\neg S\rightarrow P\quad \equiv \quad S\vee P$

Далі запишемо:

$\{\{\neg P,S\},\{\neg S,\neg P\},\{S,P\},\{\neg S\}\}$

Послідовно використовуючи правило резолюцій отримуємо:

${\frac {\{\neg S\}\qquad \{S,P\}}{\{P\}}}$

${\frac {\{\neg S\}\qquad \{\neg P,S\}}{\{\neg P\}}}$

${\frac {\{P\}\qquad \{\neg P\}}{\emptyset }}$

що й доводить твердження.

Числення висловлювань

Нехай $C_{1}$ і $C_{2}$ — дві пропозиції в численні висловлювань, і нехай $C_{1}=P\lor C'_{1}$, а $C_{2}=\lnot P\lor C'_{2}$, де $P$ — пропозіціональная змінна, а $C'_{1}$ й $C'_{2}$ — будь-які пропозиції (зокрема, може бути, порожні або складаються тільки з одного літерала).

Правило виводу

${\frac {C_{1},C_{2}}{C'_{1}\lor C'_{2}}}$

називається правилом резолюцій.

Пропозиції C₁ і C₂ називаються резольвуючими (або батьківськими), пропозиція $C'_{1}\lor C'_{2}$  — резольвентою, а формули $P$ і $\lnot P$ — контрарними літералами. Загалом в правилі резолюції беруться два вирази і виробляється новий вираз, що містить всі літерали двох початкових виразів, за винятком двох взаємно обернених літералів.

Метод резолюції

Метод резолюцій запропонований у 1930 р. в докторській дисертації Жака Ербрана для доведення теорем у формальних системах першого порядку. Метод резолюцій спирається на обчислення резольвент. Існує теорема, яка стверджує, що питання про доказовість довільної формули в численні предикатів зводиться до питання про вивідність порожнього списку в обчисленні резольвент. Тому доведення того, що список формул в обчисленні резольвент порожній, еквівалентне доведенню хибності формули в численні предикатів.

Рішення в логічній моделі на основі методу резолюцій Дано твердження: «Сократ — людина»;

«Людина — це жива істота»;

«Всі живі істоти смертні».

Потрібно методом резолюцій довести твердження «Сократ смертний».

Рішення: Крок 1. Перетворимо висловлювання на диз'юнктивну форму;

Крок 2. Запишемо заперечення цільового виразу (необхідного виводу), тобто «Сократ безсмертний»;

Крок 3. Скласти кон'юнкцію всіх диз'юнктів, включивши в неї заперечення цільового виразу;

Крок 4. У циклі проведемо операцію пошуку резольвентів над кожною парою диз'юнктів;

Отримання порожнього диз'юнкта означає, що висловлювання «Сократ безсмертний» — хибне, значить, істинне висловлювання «Сократ смертний».

Доказ теорем зводиться до доказу того, що деяка формула $~G$ (гіпотеза теореми) є логічним наслідком множини формул $~F_{1},...,F_{k}$(припущень). Тобто сама теорема може бути сформульована таким чином: «якщо $~F_{1},...,F_{k}$ істинні, то істинна й $~G$».

Для доказу того, що формула $~G$ є логічним наслідком множини формул $~F_{1},...,F_{k}$, метод резолюцій застосовується наступним чином. Спочатку складається множина формул ${\mathcal {f}}F_{1},...,F_{k},\neg G{\mathcal {g}}$. Потім кожна з цих формул приводиться до КНФ (сполучення диз'юнктів) і в отриманих формулах закреслюються знаки кон'юнкції. Виходить безліч диз'юнктів $S$. І, нарешті, шукається висновок порожнього диз'юнктів з $S$. Якщо порожній диз'юнкт виводимо з $S$, то формула $~G$ є логічним наслідком формул $~F_{1},...,F_{k}$. Якщо з $S$ не можна вивести #, то $~G$ не є логічним наслідком формул $~F_{1},...,F_{k}$. Такий метод доведення теорем називається методом резолюцій .
Розглянемо приклад докази методом резолюцій. Нехай у нас є наступні твердження:

«Яблуко червоне і ароматне.»

«Якщо яблуко червоне, то яблуко смачне.»

Доведемо твердження «яблуко смачне». Введемо множину формул, що описують прості висловлювання, відповідні вищенаведеним твердженням. Нехай

X1 — «Яблуко червоне»,

X2 — «Яблуко ароматне»,

X3 — «Яблуко смачне».

Тоді самі твердження можна записати у вигляді складних формул:

$X1\And X2$ — «Яблуко червоне і ароматне.»

$X1\rightarrow X3$ — «Якщо яблуко червоне, то яблуко смачне.»

Тоді твердження, яке треба довести, виражається формулою X3.
Отже, доведемо, що X3 є логічним наслідком $(X1\And X2)$ та $(X1\rightarrow X3)$. Спочатку складаємо множину формул з запереченням доказуваного висловлювання; отримуємо:
${\mathcal {f}}(X1\And X2),(X1\rightarrow X3),\neg X3{\mathcal {g}}.$
Тепер приводимо всі формули до кон'юнктівной нормальній форми і закреслюємо кон'юнкції. Отримуємо наступну множину диз'юнктів:
${\mathcal {f}}X1,X2,(\neg X1\vee X3),\neg X3{\mathcal {g}}.$
Далі шукаємо висновок порожнього диз'юнкта.
Застосовуємо до першого і третього диз'юнкта правило резолюції:
${\mathcal {f}}X1,X2,(\neg X1\vee X3),\neg X3,X3{\mathcal {g}}.$
Застосовуємо до четвертого і п'ятого диз'юнкт правило резолюції:
${\mathcal {f}}X1,X2,(\neg X1\vee X3),\neg X3,X3,\#{\mathcal {g}}.$
Таким чином порожній диз'юнкт виведений, отже вираз із запереченням висловлювання спростовано, отже саме висловлювання доведено. В цілому, метод резолюцій цікавий завдяки простоті та системності, але застосуємо тільки для обмеженого числа випадків (доведення не повинно мати велику глибину, а число потенційних резолюцій не повинно бути великим). Крім методу резолюцій і правил виводу існують інші методи отримання висновків у логіці предикатів.

Логіка першого порядку

Для двох літералів логіки першого порядку існує уніфікація, якщо існує така заміна їх символів змінних деякими термами, що дані літерали стають ідентичними. Наприклад: для $P(x,a,y)$ і $P(c,a,z)$, існує уніфікація, що визначається заміною $x\to c,y\to z$. Натомість для $P(x,a,y)$ і $P(c,b,z)$ уніфікація неможлива.

Нехай тепер $C_{1},C_{2}\,$ два диз'юнкти, що мають два предикати один з яких із запереченням, а другий ні і для яких існує уніфікація. Тоді резольвента двох диз'юнктів визначається:

$C_{R}=(C_{1}\cup C_{2})\setminus \{L_{1},\neg L_{2}\}$

Нехай тепер $F$ — формула записана у нормальній формі Сколема. Незважаючи на квантори загальності цю формулу можна подати як об'єднання диз'юнктів.

Позначимо:

$Res(F)=F\cup \{R\}$, де $R$ диз'юнкт одержаний за правилом резолюцій з деяких диз'юнктів формули $F$ і

$Res^{\star }(F)=\bigcup _{n\in \mathbb {N} }Res^{n}(F)$ об'єднання всіх диз'юнктів одержаних з диз'юнктів формули $F$ за скінченну кількість використань правила резолюцій.

Деяка формула $F$ записана у нормальній формі Сколема є невиконуваною тоді і тільки тоді коли $\emptyset \in Res^{\star }(F)$. З властивостей сколемізації відомо, що для довільної формули логіки першого порядку існує формула у нормальній формі Сколема, що виконується тоді і тільки тоді коли виконується початкова формула. Як наслідок з цього для довільних формул $A_{1},A_{2}\ldots A_{n}$ формула $F$ є логічним наслідком тих формул тоді і тільки тоді, коли $\emptyset \in Res^{\star }(A_{1}\lor A_{2}\lor \ldots \lor A_{n}\lor \lnot F)$. Тобто система формального виводу заснована на правилі резолюцій є коректною і повною і в цьому випадку.

Приклад

Доведемо, що формула є логічно загальнозначимою: $\forall x(p(x)\vee q(x))\wedge \neg p(a)\rightarrow q(a)$ Спершу слід використати процедуру сколемізації:

$\neg (\forall x(p(x)\vee q(x))\wedge \neg p(a)\rightarrow q(a))$

$\equiv \neg (\neg (\forall x(p(x)\vee q(x))\wedge \neg p(a))\vee q(a))$

$\equiv \forall x(p(x)\vee q(x))\wedge \neg p(a)\vee q(a)$

$\equiv \forall x(p(x)\vee q(x))\wedge \neg p(a)\wedge \neg q(a)$

Відкидаючи квантор загальності:

$(p(x)\vee q(x))\wedge \neg p(a)\wedge \neg q(a)$

$\{\{p(x),q(x)\},\{\neg p(a)\},\{\neg q(a)\}\}$

Далі послідовно використовується правило резолюцій:

${\frac {\{p(x),q(x)\}\quad \{\neg p(a)\}}{\{q(a)\}}}$

заміна (x → a)

${\frac {\{\neg q(a)\}\quad \{q(a)\}}{\emptyset }}$

заміна (x → a)

що й доводить твердження.

Обчислення предикатів

Нехай C₁ та C₂ — дві пропозиції в численні предикатів.

Правило виводу

${\frac {C_{1},C_{2}}{(C'_{1}\lor C'_{2})\sigma }}R$

називається правилом резолюції в численні предикатів, якщо в пропозиціях C₁ та C₂ існують уніфіцировані контрарні літерали P₁ та P₂, тобто $C_{1}=P_{1}\lor C'_{1}$, а $C_{2}=\lnot P_{2}\lor C'_{2}$, причому атомарні формули P₁ и P₂ є уніфікуючим найбільш загальним уніфікатором $\sigma$..

У цьому випадку резольвенти пропозицій C₁ та C₂ є пропозиція C₁ и C₂, отримане з пропозиції $C'_{1}\lor C'_{2}$застосуванням уніфікатора $\sigma$.

Однак внаслідок нерозв'зності логіки предикатів першого порядку для здійсненної (несуперечливої) множини диз'юнктів процедура, заснована на принципі резолюції, може працювати нескінченно довго. Зазвичай резолюція застосовується в логічному програмуванні в сукупності з прямим або зворотнім методом міркування. Прямий метод (від посилок) з посилок А, В виводить висновок В (правило modus ponens). Основний недолік прямого методу міркування полягає в його ненаправленості: повторні застосування методу зазвичай призводять до різкого зростання проміжних висновків, не пов'язаних з цільовим ув'язненням.
Зворотний метод (від мети) є спрямованим: з бажаного висновку В тих самих посилок він виводить новий подціловий висновок А. Кожен крок висновування в цьому випадку завжди пов'язаний з спочатку поставленою метою.

Істотний недолік принципу резолюції полягає у формуванні на кожному кроці виводу безлічі резольвентів — нових диз'юнктів, більшість з яких виявляються зайвими. У зв'язку з цим розроблені різні модифікації принципу резолюції, що використовують більш ефективні стратегії пошуку і різного роду обмеження на вид вихідних диз'юнктів.

Висновок в логічних моделях

Висновок у формальній логічній системі є процедурою, яка із заданої групи виразів виводить відмінне від заданих семантично правильний вираз. Ця процедура, представлена ​​у певній формі, і є правилом виводу. Якщо група виразів, що утворює посилку, є істинною, то повинно гарантуватися, що застосування правила висновування забезпечить отримання істинного виразу як висновку.

Найбільш часто використовуються два методи. Перший — метод правил виводу або метод природного (натурального) висновування, названий так тому, що використовуваний тип міркувань в численні предикатів наближається до звичайного людського розуміння. Другий — метод резолюцій. У його основі лежить літочислення резольвент.

Див. також

• Числення висловлень
• Логіка першого порядку
• Кон'юнктивна нормальна форма
• Нормальна форма Сколема
• Детальний опис методу резолюцій

Джерела

1. J. Alan Robinson (1965), A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM (JACM), Volume 12, Issue 1, pp. 23-41.
2. Leitsch, Alexander (1997). The Resolution Calculus. Springer-Verlag.
3. Gallier, Jean H. (1986). Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row Publishers.