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

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

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

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

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

Доказ теорем зводиться до доказу того, що деяка формула (гіпотеза теореми) є логічним наслідком множини формул (припущень). Тобто сама теорема може бути сформульована таким чином: «якщо істинні, то істинна і ».
».Для доказу того, що формула  є логічним наслідком множини формул , метод резолюцій застосовується наступним чином. Спочатку складається множина формул . Потім кожна з цих формул приводиться до КНФ(кон'юнкція диз'юнктів) і в отриманих формулах закреслюються знаки кон'юнкції. Виходить множина диз'юнктів . І, нарешті, шукається висновок порожнього диз'юнкта з . Якщо порожній диз'юнкт виводимо з , то формула є логічним наслідком формул . Якщо з не можна вивести # ,то не є логічним наслідком формул . Такий метод доведення теорем називається методом резолюцій
.Розглянемо приклад докази методом резолюцій. Нехай у нас є наступні твердження:
:«Яблуко червоне і ароматне.»
:«Якщо яблуко червоне, то яблуко смачне.»
Доведемо твердження «яблуко смачне». Введемо множину формул, що описують прості висловлювання, відповідні вищенаведеним твердженням. нехай
:X1 - «Яблуко червоне»,
:X2 - «Яблуко ароматне»,
:X3 - «Яблуко смачне».
Тоді самі твердження можна записати у вигляді складних формул:: - «Яблуко червоне і ароматне.».
:  - «Якщо яблуко червоне, то яблуко смачне.».
Тоді твердження, яке треба довести, виражається формулою X3.
Отже, доведемо, що X3 є логічним наслідком  і .. Спочатку складаємо множину формул з запереченням доказуваного висловлювання; отримуємо:
Тепер приводимо всі формули до кон'юнктивної нормальної форми і закреслюємо кон'юнкції. Отримуємо наступну множину диз'юнктів:

Далі шукаємо вивід порожнього диз'юнкта.
Застосовуємо до першого і третього диз'юнкта правило резолюції:

Застосовуємо до четвертого і п'ятого диз'юнктів правило резолюції:

Таким чином порожній диз'юнкт виведений, отже вираз із запереченням висловлювання спростовано, отже саме висловлювання доведено.

Принцип резолюції[ред. | ред. код]

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


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.

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

Приклад2[ред. | ред. код]


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

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