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

Занятие 3.4. (8-ое)

Метод резолюций

Решить следующие задачи методом резолюций.

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

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

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

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

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

F1: "x,y,z ((xy)z=x(yz)),

F2: "x,y $z(zx=y),

F3: "x,y $z(xz=y).


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

Наша задача – установить, что формула G есть логическое следствие формул F1, F2, F3.

Прежде, чем решать эту задачу, перейдем к другой сигнатуре. Введем символ трехместного предиката P, который интерпретируется следующим образом: P(x,y,z) означает, что xy=z.

В новой сигнатуре формулы F1, F2, F3 и G запишутся так:

F1/="x,y,z,u,v,w (P(x,y,u)&P(y,z,v)&P(x,v,w) ÉP(u,z,w)),

F2/="x,y $z P(z,x,y),

F3/="x,y $z P(x,z,y),

G/=$x "y P(y,x,y).

Сформируем множество T={F1,F2,F3, Пример 3 (Дедуктивные базы данных) - student2.ru G}, каждую из формул этого множества приведем к сколемовской нормальной форме и удалим кванторы общности (конъюнкция в сколемовских нормальных формах не появится). Получим множество дизъюнктов D1,D2,D3,D4:

D1= Пример 3 (Дедуктивные базы данных) - student2.ru P(x,y,u) Ú Пример 3 (Дедуктивные базы данных) - student2.ru P(y,z,v) Ú Пример 3 (Дедуктивные базы данных) - student2.ru P(x,v,w) ÚP(u,z,w),

D2= P(f(x,y),x,y),

D3= P(x,g(x,y)y),

D4= Пример 3 (Дедуктивные базы данных) - student2.ru P(h(x),x,h(x)).

Построим вывод пустого дизъюнкта из множества дизъюнктов D1,...,D4. Пусть эти дизъюнкты–первые дизъюнкты вывода. Заменим переменные в дизъюнкте D2, получим дизъюнкт D2/=P(f(x/,y/),x/,y/).

Литералы P(x,y,u) из D1и D2/ унифицируются подстановкой s1={x\f(x/,y/),y\ x/, u\y/}. Применим правило резолюций к D1 и D2 (и указанным литералам), получим дизъюнкт

D5= Пример 3 (Дедуктивные базы данных) - student2.ru P(x/,z,v) Ú Пример 3 (Дедуктивные базы данных) - student2.ru P(f(x/,y/)v,w) Ú P(y/,z,w).

Далее, литерал P(f(x/,y/),v,w) из D5 и D2 унифицируются подстановкой s2={x/\x,y/\y,v\x,w\y}.

Правило резолюций, примененное к D5 и D2, дает дизъюнкт

D6= Пример 3 (Дедуктивные базы данных) - student2.ru P(x,z,x) ÚP(y,z,y).

Резольвентой дизъюнктов D3 и D6 будет дизъюнкт

D7=P(y,g(y/,y/),y).

Для получения этой резольвенты заменим переменные в D3, получим D3=P(x/,g(x/,y/),y/) и используем подстановку s3={x\y/,z\g(y/,y/)}.

Наконец, из дизъюнктов D4 и D7 с помощью подстановки s4={y\h(g(y/,y/)), x\g(y/,y/)} получаем

D8= □ - пустой дизъюнкт.

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

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

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

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

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

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

F2="x $yP(x,y),

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

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

Используя метод резолюций, покажем, что G есть логическое следствие F1 и F2. Приведем формулы F1,F2 и Пример 3 (Дедуктивные базы данных) - student2.ruG к сколемовской нормальной форме, получим дизъюнкты:

D1= Пример 3 (Дедуктивные базы данных) - student2.ru P(x,y) Ú Пример 3 (Дедуктивные базы данных) - student2.ru P(y,z) ÚQ(x,z),

D2=P(x,f(x)),

D3= Пример 3 (Дедуктивные базы данных) - student2.ru Q(a,z).

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

D4= Пример 3 (Дедуктивные базы данных) - student2.ru P(a,y) Ú Пример 3 (Дедуктивные базы данных) - student2.ru P(y,z) ((D1 D3,){x=a}),

D5= Пример 3 (Дедуктивные базы данных) - student2.ru P(f(a),z) ((D2 D4 ),{x=a, y=f(a)}),

D6=□ ((D2 D5), {x=f(a),z=f(f(a))}.

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

Довольно часто интересующая нас переменная участвует не в одной подстановке, как в этом примере переменная z, а в нескольких. Для того, чтобы отследить все подстановки, в которых может изменить значение переменная, к формуле Пример 3 (Дедуктивные базы данных) - student2.ruG добавляют литерал ответа 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, если обезьяна взяла бананы.

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

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

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

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


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

F4=P(a,b,c,s0).

Надо показать, что формула G=$sR(s) есть логическое следствие формул F1,F2,F3,F4.

Из множества формул F1,F2,F3,F4,Пример 3 (Дедуктивные базы данных) - student2.ruG получим множество дизъюнктов D1–D5 (к дизъюнкту, полученному из Пример 3 (Дедуктивные базы данных) - student2.ruG добавлен литерал ответа ANS(s)):

D1= Пример 3 (Дедуктивные базы данных) - student2.ru P(x,y,z,s) Ú P(y,y,z,ИДТИ(x,y,s)),

D2= Пример 3 (Дедуктивные базы данных) - student2.ru P(x,x,u,s,) ÚP(u,u,u,НЕСТИ(x,u,s)),

D3= Пример 3 (Дедуктивные базы данных) - student2.ru P(x,x,x,s) ÚR(БРАТЬ(s)),

D4=P(a,b,c,s0),

D5= Пример 3 (Дедуктивные базы данных) - student2.ru R(s) ÚANS(s).

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

D6= Пример 3 (Дедуктивные базы данных) - student2.ru P(x,x,x,s) ÚANS(БРАТЬ(s)) (из D3 D5),

D7= Пример 3 (Дедуктивные базы данных) - student2.ru P(x,x,u,s) ÚANS(БРАТЬ(НЕСТИ(x,u,s))) (из D2 и D6),

D8= Пример 3 (Дедуктивные базы данных) - student2.ru P(x,y,z,s) ÚANS(БРАТЬ(НЕСТИ((y,z,ИДТИ(x,y,s)))) (из D1 и D7),

D9=ANS(БРАТЬ(НЕСТИ(b,c,ИДТИ((a,b,s0)))) (из D4 и D8).

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

Наши рекомендации