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

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до: навігація, пошук

Правило резолюцій — це правило висновку, що сходить до методу доказу теорем через пошук протиріч; використовується в логіці висловлювань і логіці предикатів першого порядку. Правило резолюцій, що застосовується послідовно для списку резольвент, дозволяє відповісти на питання, чи існує у вхідній множині логічих виразів протиріччя. Правило резолюцій запропоновано в 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 \or C'_1, а C_2 = \lnot P \or C'_2, де P — пропозіціональная змінна, а C'_1 й C'_2 — будь-які пропозиції (зокрема, може бути, порожні або складаються тільки з одного літерала).

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

\frac{C_1, C_2}{C'_1 \or C'_2}

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

Пропозиції C1 і C2 називаються резольвуючими (або батьківськими), пропозиція C'_1 \or 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)

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

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

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

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

\frac{C_1, C_2}{(C'_1 \or C'_2)\sigma}R

називається правилом резолюції в численні предикатів, якщо в пропозиціях C1 та C2 існують уніфіцировані контрарні літерали P1 та P2, тобто C_1 = P_1 \or C'_1, а C_2 = \lnot P_2 \lor C'_2, причому атомарні формули P1 и P2 є уніфікуючим найбільш загальним уніфікатором \sigma..

У цьому випадку резольвенти пропозицій C1 та C2 є пропозиція C1 и C2, отримане з пропозиції C'_1 \or C'_2застосуванням уніфікатора \sigma.[2]

Однак внаслідок нерозв'зності логіки предикатів першого порядку для здійсненної (несуперечливої) множини диз'юнктів процедура, заснована на принципі резолюції, може працювати нескінченно довго. Зазвичай резолюція застосовується в логічному програмуванні в сукупності з прямим або зворотнім методом міркування. Прямий метод (від посилок) з посилок А, В виводить висновок В (правило 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.