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

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

Метод резолюції відноситься до напівконструктивного методу, він легко піддається алгоритмізації. Суть його полягає в тому, що два посилкових диз'юнкта з протилежними термами завжди можна склеїти в один заключний диз'юнкт, в якому відсутні протилежні терми:

$A\lor B,\ B\lor C=A\lor C$

де A,C - довільні терми, або цілі диз'юнкти з довільним набором термів, включаючи нуль, а та - довільні терми. При послідовному застосуванні принципу резолюцій зменшується число букв, деякі повністю знищуються, а вихідна клауза будується у формі кон'юктивного протиріччя:

$P_{1},P_{2},...,P_{n}=0$

Доказ теорем зводиться до доказу того, що деяка формула $~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}}.$
Таким чином порожній диз'юнкт виведений, отже вираз із запереченням висловлювання спростовано, отже саме висловлювання доведено.

Принцип резолюції

Принцип резолюцій повністю замінює аксіому порядку, оскільки вона сама може бути доведена в рамках методу резолюцій.

$A,B\Rightarrow A$

A,B,A‾ ⇒ 0

0,B ⇒ 0

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

Приклади

Приклад 1

Приклад 1. Довести методом резолюцій істинність клаузи: 

A→B, C→D, B→E, D→F‾, E→F, A→C⇒A‾

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

1.	A‾⋁B ⇒
2.	C‾⋁D
3.	B‾⋁E
4.	D‾⋁F
5.	E‾⋁F‾
6.	A‾⋁C
7.	A
8.	C‾⋁F (2,4)
9.	B‾⋁F‾ (3,5)
10.	A‾⋁F‾ (9,1)
11.	A‾⋁F (8,6)
12.	A‾ (10,11)
13.	0 (12,7)

Таблиця 1.

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

Див. також

• Теорія алгоритмів
• Список алгоритмів
• Структури даних
• Програмування
• Хвильовий алгоритм

Джерела

• Метод резолюції в логіці висловлень