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

Правило резолюцій — це правило висновування, що сходить до методу доказу теорем через пошук протиріч; використовується в логіці висловлювань і логіці предикатів першого порядку. Правило резолюцій, що застосовується послідовно для списку резольвент, дозволяє відповісти на питання, чи існує у вхідній множині логічих виразів протиріччя. Правило резолюцій запропоновано в 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}}}$

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

Пропозиції 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$ .[2]

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

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

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

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

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

Примітки

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

Див. також

Джерела

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.
Leitsch, Alexander (1997). The Resolution Calculus. Springer-Verlag.
Gallier, Jean H. (1986). Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row Publishers.

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.

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

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