Стратегии проведения резолюции.

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

Рассмотрим самые распространенные стратегии.

A) Полный перебор. Проверяются все возможные варианты поиска резольвент на каждом шаге. Недостаток этой стратегии заключается в том, что очень высока трудоёмкость соответствующего алгоритма. Основное достоинство – полнота.

B) Линейные резолюции. Линейным называется вывод, удовлетворяющий следующей схеме (рис?):

 

Рис? Схема линейной резолюции

//cхему подправить (11)

 

где С_i - центральные клозы, В_j - боковые. Боковой клоз всегда выбирается либо из входного множества (S), либо среди клозов, полученных на предыдущих шагах. Клоз C называется верхним в выводе. Под входным понимается само начальное множество опровергаемых клозов.

//тут формальное условие на B_j (12)

B_j S или B_j = C_i,

где: i < j

 

Недостаток этой стратегии в том, что она не полна.

C) Входная резолюция.

Это частный случай линейной резолюции. Накладывается дополнительное условие на то, что боковой клоз можно выбирать только из входного множества. Сохраняется основной недостаток линейной резолюции, заключающийся в ее неполноте.

//формальное условие (13)

B; S

D) Стратегия OL-вывода (Ordered Lined).

E) Вывод на клозах Хорна (реализован в Прологе).

Примечание. Последние две стратегии будут рассмотрены подробнее, как наиболее часто применяющиеся на практике.