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

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

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

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

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

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

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

Метод резолюцій[ред.ред. код]

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

Ідея методу резолюцій полягає в тому, що доказ істинності чи хибності висунутого припущення, наприклад:


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


Якщо в процесі доведення виникає протиріччя між запереченням гіпотези і аксіомами, що виражається в знаходженні порожнього списку (диз'юнктів), то висунута гіпотеза правильна. Таке доведення може бути отримано на підставі теореми Ербрана, яка гарантує, що існуюче протиріччя може бути завжди досягнуто за кінцеве число кроків, які б не були значення істинності, що даються функціям, присутнім в гіпотезах. У методі резолюцій множина пропозицій зазвичай розглядається як складовий предикат, що містить кілька предикатів, з'єднаних логічними функціями і кванторами існування і загальності. Так, як однакові за змістом предикати можуть мати різний вигляд, то пропозиції перетворюються в клаузальну форму - різновид кон'юнктивної нормальної форми (КНФ), у якої вилучені квантори існування, загальності, символи імплікації, рівнозначності та ін. Клаузальну форму називають сколемовскою кон'юнктивною формою. У клаузальній формі вся початкова логічна формула представляється у вигляді множини пропозицій (клауз) С, так званою клаузальною множиною S:

Будь-яка пропозиція C, з якої утворюється клаузальна множина S, є сукупністю атомарних предикатів або їх заперечень, з'єднаних символом диз'юнкції:

Вивід рішення в логічній моделі на основі методу резолюцій[ред.ред. код]

Дано твердження:

«Сократ - людина»;

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

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

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

Рішення:

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

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

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

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

Airportal

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

В цілому, метод резолюцій цікавий завдяки простоті та системності, але застосуємо тільки для обмеженого числа випадків (доведення не повинно мати велику глибину, а число потенційних резолюцій не повинно бути великим). Крім методу резолюцій і правил виводу існують інші методи отримання висновків у логіці предикатів.

Доведення методом резолюцій істинності клаузи[ред.ред. код]

Доведення. Приведемо клаузу до нормальної кон'юктивної форми (див.табл.24):


Таблиця 24.

Метод резолюцій використовується в логічних мовах програмування, (ПРОЛОГ). Алгоритм склейок утворює структуру деревовидної форми, що добре видно з наступного прикладу.

Приклад. Довести клаузу : 

Детальний опис методу резолюцій

Див. також[ред.ред. код]

Джерела[ред.ред. код]

  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.