Відкрити головне меню

Метод резолюціїРедагувати

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

 

де 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Редагувати


Див. такожРедагувати

ДжерелаРедагувати