Метод резолюції
Було запропоновано об'єднати цю статтю або розділ з Правило резолюцій, але, можливо, це варто додатково обговорити. Пропозиція з грудня 2014. |
Метод резолюції відноситься до напівконструктивного методу, він легко піддається алгоритмізації. Суть його полягає в тому, що два посилкових диз'юнкта з протилежними термами завжди можна склеїти в один заключний диз'юнкт, в якому відсутні протилежні терми:
де A,C - довільні терми, або цілі диз'юнкти з довільним набором термів, включаючи нуль, а та - довільні терми. При послідовному застосуванні принципу резолюцій зменшується число букв, деякі повністю знищуються, а вихідна клауза будується у формі кон'юктивного протиріччя:
Доказ теорем зводиться до доказу того, що деяка формула (гіпотеза теореми) є логічним наслідком множини формул (припущень). Тобто сама теорема може бути сформульована таким чином: «якщо істинні, то істинна і ».
».Для доказу того, що формула є логічним наслідком множини формул , метод резолюцій застосовується наступним чином. Спочатку складається множина формул . Потім кожна з цих формул приводиться до КНФ(кон'юнкція диз'юнктів) і в отриманих формулах закреслюються знаки кон'юнкції. Виходить множина диз'юнктів . І, нарешті, шукається висновок порожнього диз'юнкта з . Якщо порожній диз'юнкт виводимо з , то формула є логічним наслідком формул . Якщо з не можна вивести # ,то не є логічним наслідком формул . Такий метод доведення теорем називається методом резолюцій
.Розглянемо приклад докази методом резолюцій. Нехай у нас є наступні твердження:
:«Яблуко червоне і ароматне.»
:«Якщо яблуко червоне, то яблуко смачне.»
Доведемо твердження «яблуко смачне». Введемо множину формул, що описують прості висловлювання, відповідні вищенаведеним твердженням. нехай
:X1 - «Яблуко червоне»,
:X2 - «Яблуко ароматне»,
:X3 - «Яблуко смачне».
Тоді самі твердження можна записати у вигляді складних формул:: - «Яблуко червоне і ароматне.».
: - «Якщо яблуко червоне, то яблуко смачне.».
Тоді твердження, яке треба довести, виражається формулою X3.
Отже, доведемо, що X3 є логічним наслідком і .. Спочатку складаємо множину формул з запереченням доказуваного висловлювання; отримуємо:
Тепер приводимо всі формули до кон'юнктивної нормальної форми і закреслюємо кон'юнкції. Отримуємо наступну множину диз'юнктів:
Далі шукаємо вивід порожнього диз'юнкта.
Застосовуємо до першого і третього диз'юнкта правило резолюції:
Застосовуємо до четвертого і п'ятого диз'юнктів правило резолюції:
Таким чином порожній диз'юнкт виведений, отже вираз із запереченням висловлювання спростовано, отже саме висловлювання доведено.
Принцип резолюцій повністю замінює аксіому порядку, оскільки вона сама може бути доведена в рамках методу резолюцій.
A,B,A‾ ⇒ 0
0,B ⇒ 0
Звернемо увагу на те, що посилка В взагалі не використовується, тобто необов'язково треба використовувати всі посилки, головне отримати нуль. Всі доведення клауз починають з приведення їх в нормальну кон'юктивну форму, потім виписують по порядку всі посилки і склеюють згідно з чергою.
Приклад 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.
Метод резолюцій використовується в логічних мовах програмування. Алгоритм склейок утворює структуру деревоподібної форми, що добре видно з наступного прикладу.'
На цю статтю не посилаються інші статті Вікіпедії. Будь ласка розставте посилання відповідно до прийнятих рекомендацій. |