ОСНОВИ ДИСКРЕТНОГО АНАЛІЗУ.
Автори: Н.Д.Федоренко,В.В.Демченко

     3.18. МЕТОД РЕЗОЛЮЦІЙ ДОВЕДЕННЯ В ЛОГІЦІ ВИСЛОВЛЮВАНЬ

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

,

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

,

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

,

,

.

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

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



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


(див.табл.24)

Таблиця 24.

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

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





Рис.8

ЗМІСТ