Пример 3 (Дедуктивные базы данных)

Отметим вначале одно свойство метода резолюций. Пусть сигнатура состоит из двух символов двухместных предикатов P и Q, которые интерпретируются следующим образом:

P(x,y) означает, что х– сын y,

Q(x,z) означает, что х– внук z.

Рассмотрим формулы:

F₁="x,y,z (P(x,y)&P(y,z) É Q(x,z)),

F₂="x $yP(x,y),

G="x $zQ(x,z),

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

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

D₁= P(x,y) Ú P(y,z) ÚQ(x,z),

D₂=P(x,f(x)),

D₃= Q(a,z).

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

D₄= P(a,y) Ú P(y,z) ((D₁ D₃,){x=a}),

D₅= P(f(a),z) ((D₂ D₄ ),{x=a, y=f(a)}),

D₆=□ ((D₂ D₅), {x=f(a),z=f(f(a))}.

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

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

Пример 4 (Планирование действий).

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

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

P(x,y,z,s) означает, что в состоянии s обезьяна находится в точке x, стул –

в y, бананы – в z,

R(s) означает, что в состоянии s обезьяна взяла бананы.

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

ИДТИ(x,y,s) – состояние, которое получится из s, если обезьяна из точки x

перешла в y,

НЕСТИ(x,y,s) – состояние, которое получится из s, если обезьяна перенесла

стул из точки x в y,

БРАТЬ(s) – состояние, которое получится из s, если обезьяна взяла бананы.

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

F₁= "x,y,z,s (P(x,y,z,s) ÉP(y,y,z, ИДТИ(x,y,s)),

F₂="x, u, s (P(x,x,u,s) É P(u,u,u, НЕСТИ(x,u,s)) ,

F₃="x (P(x,x,x,s) ÉR(БРАТЬ(s))).

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

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

Надо показать, что формула G=$sR(s) есть логическое следствие формул F₁,F₂,F₃,F₄.

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

D₁= P(x,y,z,s) Ú P(y,y,z,ИДТИ(x,y,s)),

D₂= P(x,x,u,s,) ÚP(u,u,u,НЕСТИ(x,u,s)),

D₃= P(x,x,x,s) ÚR(БРАТЬ(s)),

D₄=P(a,b,c,s₀),

D₅= R(s) ÚANS(s).

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

D6= P(x,x,x,s) ÚANS(БРАТЬ(s)) (из D₃ D₅),

D₇= P(x,x,u,s) ÚANS(БРАТЬ(НЕСТИ(x,u,s))) (из D₂ и D₆),

D₈= P(x,y,z,s) ÚANS(БРАТЬ(НЕСТИ((y,z,ИДТИ(x,y,s)))) (из D₁ и D₇),

D₉=ANS(БРАТЬ(НЕСТИ(b,c,ИДТИ((a,b,s₀)))) (из D₄ и D₈).

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