Преимущества и недостатки метода резолюции

 

1. Надо знать и помнить всего одно правило.

2. Применение этого правила можно автоматизировать(запрограммировать на ПК).

3.Ответы можно извлекать из унификаторов.

Недостатки:

Не гарантируется конец работы (бесконечный цикл при попытке найти доказательство). Но это бывает очень редко, так как большинство реальных задач не содержат “неразрешимых ” формул.

Общий вывод:

1. Предложения Пролога можно интерпретировать как предложения исчисления предикатов первого порядка.

(фразы Хорна)

2. Компилятор Пролога можно рассматривать как резолюционную процедуру доказательства, использующую поиск в глубину (сверху - вниз и слева – направо)

3. Все вычислительные задачи можно сформулировать, пользуясь только отрицанием, правилами и фактами, а те из задач, которые являются разрешимыми, можно решить с помощью общей резолюции сверху вниз.

(неразрешимыми считаем те задачи, которые не имеют опровержения)

 

Дополнительная информация:

Резолюция обладает важными свойствами корректности и полноты.

 

Резолюция корректна в том смысле, что если с ее помощью из множества допущений S1 и отрицания F выводится противоречие, то обязательно справедливо отношение S1 |-- F .

Резолюция полна в том смысле, что если справедливо S1|-F ,то противоречие непременно выводится из S1 и F .

Проблема общезначимости

Логика первого порядка только частично разрешима. Но есть алгоритмы, которые всегда устанавливают справедливость отношения S1|- F ,если оно действительно имеет место. Это значит, что если составили неразрешимую логическую программу, то есть не имеющую опровержения и подали ее на вход частично разрешимой процедуры, основанной на резолюции и реализовали на ЭВМ ,то может произойти зацикливание.

Исследования подтвердили, что логика хорновских дизъюнктов является универсальным вычислительным формализмом. Ее проверили на множестве натуральных чисел, на частично рекурсивных функциях, на классе алгоритмов Маркова и тому подобное.