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

Доказательство теорем. Применим метод резолюций в доказательстве одной простой теоремы из теории групп.

В качестве исходной возьмем следующую аксиоматику теории групп:

Предположим, что нам надо доказать теорему G: ($x)("y)(yx=y), т.е. что в группе существует правая единица.

Наша задача–установить, что формула G есть логическое следствие формул F₁, F₂, F₃. Прежде, чем решать эту задачу, перейдем к другой сигнатуре. Введем символ трехместного предика P, который интерпретируется следующим образом:

P(x,y,z) означает, что xy=z.

В новой сигнатуре формулы F₁, F₂, F₃ и G запишутся так:

Сформулируем множество T={F₁,F₂,F₃,ØG}, каждую из формул этого множества приведем к сколемовской нормальной форме и удалим кванторы общности (конъюнкция в сколемовских нормальных формах не появится). Получим множество дизъюнктов D₁,D₂,D₃,D₄:

Построим вывод пустого дизъюнкта из множества дизъюнктов D₁,...,D₄. Пусть эти дизъюнкты–первые дизъюнкты вывода. Заменим переменные в дизъюнкте D₂, получим дизъюнкт D₂^/=P(f(x^/,y^/),x^/,y^/). Литералы P(x,y,u) и D₂^/ унифицируются подстановкой s₁={x=f(x^/,y^/),y= x^/, u=y^/}. Применим правило резолюций к D₁ и D₂ (и указанным литералам), получим дизъюнкт

D₅="P(x^/,,z,v)ÚØP(f(x^/,y^/)v,w)ÚP(y^/,z,w).

Далее, литерал P(f(x^/,y^/),v,w) и D₂ унифицируются подстановкой s₂={x^/=x,y^/=y,v=x,w=y}. Правило резолюций, примененное к D₁ и D₂, дает дизъюнкт

D₆=ØP(x,z,x)ÚP(y,z,y).

Резольвентой дизъюнктов D₃ и D₆ будет дизъюнкт

D₇=P(y,g(y^/,y^/),y).

(Для получения этой резольвенты заменим переменные в D₃, получим D₃=P(x^/,g(x^/,y^/),y^/) и используем подстановку s₃={x=y^/,z=g(y^/,y^/)}. Наконец, из дизъюнктов D₄ и D₇ с помощью подстановки s₄={y=h(g(y^/,y^/)), x=g(y^/,y^/)} получаем пустой дизъюнкт.

Планирование действий. Отметим вначале одно свойство метода резюлюций. Пусть сигнатура t состоит из двух символов двухместных предикатов P и Q, которые интерпретируются следующим образом: P(x,y) означает, что х–сын y, Q(x,z) означает, что х–внук z.Рассмотрим формулы:

смысл которых достаточно ясен.

Используя метод резолюцийц, покажем, что G есть логическое следствие F₁ и F₂. Приведем формулы F₁,F₂ и ØG к сколемовской нормальной форме, получим дизъюнкты:

Вывод пустого дизъюнкта получается довольно просто:

Подстановка z=f(f(a)) означает, что дед элемента a есть отец элемента a. Таким образом, метод резолюций не только устанавливает факт логического следствия формулы G из формул F₁ и F₂, но еще и «подсказывает», как по данному х получить z такой, чтобы формула Q(x,z) была истинна.

Довольно часто интересующая нас переменная участвует не в одной подстановке, как в этом примере переменная z, а в нескольких. Для того, чтобы тследить все подстановки, в которых может изменить значение переменная, к формуле ØG добавляют литерал ответа ANS(z) и заканчивают вывод не пустым дизъюнктом, а литералом ответа.

В качестве примера использования метода резолюций в задачах планирования действий рассмотрим известную в теории искусственного интеллекта задачу об обезъяне и бананах. В задаче говорится об обезъяне, которая хочет съесть бананы, подвешенные к потолку комнаты. Рост обезъяны недостаточен, чтобы достать бананы. Однако в комнате есть стул, встав на который обезъяна может достать бананы. Какие ей надо совершить действия, чтобы достать бананы?

Задачу формализуем следующим образом. Комнату с находящимися в ней обезъяной, стулом и бананами будем называть предметной областью. Конкретной местонахождение в комнате обезъяны, стула и бананов будем называть состоянием предметной области. Рассмотрим два предиката P(x,y,z,s) R(z). Пусть

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

Условия задачи запишутся в виде следующих формул:

F₁=("x,y,z,s))[P(x,y,z,s)®P(u,y,z, (x,,,u,s))],

F₂=("x,z,s)[P(x,x,z,s)®P(u,u,s, (x,u,s)],

F₃=("x)[P(x,x,x,s)®R( (s))].

Пусть в начальном состоянии s₀ обезъяна находилась в точке а, стул–в точке b, бананы–в точке c. Следовательно, к написанным формулам надо ддобавить формулу

F₄=P(a,b,c,s₀).

Надо показать, что формула G=($s)R(s) есть логическое следствие формул F₁,F₂,F₃,F₄. Из множества формул F₁,F₂,F₃,F₄,ØG получим множество дизъюнктов D₁–D₅ (к дизъюнкту, полученному из ØG добавлен литерал ответа ANS(s)):

Последовательность дизъюнктов D₁–D₅ продолжаем до вывода литерала ответа:

Итак, для того, чтобы обезъяне взять бананы, надо сначала из точки а идти в точку b, затем из точки b нести стул в точку с и в точке с, встав на стул, взять бананы.