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

У логіці, зокрема логіці висловлень і логіці першого порядку, правило резолюцій є правилом виводу формул записаних у кон'юнктивній нормальній формі і нормальній формулі Сколема. Широко застосовується при автоматичному доведенні теорем. Було вперше запропоновано Джоном Аланом Робінсоном у 1965 році.

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

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

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

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

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

Для двох літералів логіки першого порядку існує уніфікація, якщо існує така заміна їх символів змінних деякими термами, що дані літерали стають ідентичними. Наприклад: для $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)

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

Див. також

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

Джерела

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.