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

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

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

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

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

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

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

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

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

B_j S или B_j = C_i ,

где: i < j

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

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

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

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

B; S

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

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

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

2.2.4. Упорядоченный линейный вывод в лппп.

Будем считать, что литеры в клозе упорядочены. Для того чтобы сохранять информацию об отрезанных литерах, они не удаляются, а только обрамляются. Если на каком-то шаге получается клоз, содержащий две одинаковые литеры, то оставляется самая левая из них, после чего отбрасываются все обрамлённые литеры, за которыми не следуют необрамлённые. Эта операция называется отождествлением влево. Если в упорядоченном клозе последняя литера унифицируется с отрицанием одной из обрамлённых литер, то клоз называется редуцируемым и производится его редукция, то есть:

1) удаляется последнюю литеру и обрамленную литеру, с отрицанием которой унифицируется последняя литера;

2) отбросываются все обрамлённые литеры, за которыми не следуют необрамлённые.

Например, pqsq

pqsq

p

//Пример переделать под ЛППП (14)

P (x)  Q (x, f (x))  S (y)   Q (x, f (b))

{b/x}

P (b)  Q (b, f(b))  S (y)   Q (b, f ))

P (b)

Упорядоченной бинарной резольвентой (упорядоченной резольвентой) клозов C₁ и C₂, содержащих контрарные литеры L₁ и L₂ (причем L₁ – последняя литера в клозе C) называется клоз C вида C={C₁}{C₂L₂}, где C₁ получен из С₁ путём обрамления последней литеры.

Например, pq

qr

pqr

//пример переделать под ЛППП (15)

{b/x} P (x)  Q (x, f (a))

Q (b, a)  R (z)

P (b)  Q (b, f (a))  R (z)

Упорядоченным линейным выdодом (OL-выводом) пустого клоза из S (OL-опровержением множества S) называется вывод, удовлетворяющий следующим условиям:

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

2. вывод имеет следующий вид:

//cхему подправить (12 – аналогично)

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

OL-вывод является так называемой почти полной стратегией.

Теорема о полноте OL-вывода. Если множество клозов S противоречиво, а множество {S/C} - выполнимо, где CS, то существует OL-вывод пустого клоза из S с верхним дизъюнктом C.

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