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

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

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

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

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

${\displaystyle {\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}}}}$

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

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

${\displaystyle \neg p\wedge (q\vee r\vee q)\wedge (\neg r\vee \neg s)\wedge (p\vee s)\wedge (\neg q\vee \neg s)}$

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

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

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

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

Позначимо:

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

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

Приклад

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

${\displaystyle (P\rightarrow S)}$

${\displaystyle (S\rightarrow \neg P)}$

${\displaystyle (\neg S\rightarrow P)}$

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

${\displaystyle (P\rightarrow S),(S\rightarrow \neg P),(\neg S\rightarrow P)\models S}$

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

${\displaystyle P\rightarrow S\quad \equiv \quad \neg P\vee S}$

${\displaystyle S\rightarrow \neg P\quad \equiv \quad \neg S\vee \neg P}$

${\displaystyle \neg S\rightarrow P\quad \equiv \quad S\vee P}$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Позначимо:

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

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

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

Приклад

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

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

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

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

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

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

${\displaystyle (p(x)\vee q(x))\wedge \neg p(a)\wedge \neg q(a)}$

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

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

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

заміна (x → a)

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

заміна (x → a)

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

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

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

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

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

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

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

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

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

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

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

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

Примітки

1. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем стр. 77
2. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем стр. 85

Див. також

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

Джерела

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.