3.7. Семантическая резолюция

В семантической резолюции предотвращение порождения лишних дизъюнктов осуществляется за счет разбиения исходного множества дизъюнктов S на два подмножества S₁ и S₂ и разрешения резольвирования только между этими подмножествами. Разбиение множества S на два подмножества S₁ и S₂ осуществляется на основе вводимой интерпретации I. Так в S₁ входят те дизъюнкты из множества S, которые не удовлетворяют интерпретации I, в S₂ входят те дизъюнкты, которые удовлетворяют интерпретации I. Также вводится упорядочивание литер в дизъюнкте и разрешается резольвирование только по литерам с наибольшим порядком.

Определение. Пусть I-интерпретация для S и Р - упорядочивание литер в S. Тогда множество {E₁,E₂,...,E_q,N} называется семантическим клашем (clash) (или PI-клаш), если E₁,E₂,...,E_q, называемые электронами, и N, называемое ядром, удовлетворяют следующим условиям.

1. Все электроны E₁,E₂,...,E_q ложны в интерпретации I.

2. Резольвента R₁=N и резольвента R_i+1 получается из E_i и R_i.

3. Литеры в E_i резольвируются с наибольшим порядком.

4. R_q+1 носит название PI-резольвента.

PI-резольвента всегда ложна в интерпретации I.

Определение. Пусть Р -упорядочивание литер и I-интерпретация. Тогда PI-выводом будем называть С₁,С₂,...,С_к, где С_i (i=1,...к) есть либо дизъюнкт из S, либо PI-резольвента.

PI-вывод пустого дизъюнкта есть PI-вывод, в котором С_к=.

Теорема 3.8. о полноте семантической резолюции (Slagle). Пусть Р-упорядочивание литер и I-интерпретация. Если множество дизъюнктов S противоречиво, то всегда существует PI-вывод пустого дизъюнкта.

Частными случаями семантической резолюции являются:

• положительная гиперрезолюция;

• отрицательная гиперрезолюция;

• стратегия множества поддержки.

Пример 3.25.

Докажем пример 2.3, используя различные модификации семантической резолюции.

A&B(AB)

S={A, B, AB}

а) Положительная гиперрезолюция.

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

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

I={ A, B}, A>B

E₁=A E₂=B N₁=AB



Рис. 3.6.(а)

б) Отрицательная гиперрезолюция.

Отрицательная гиперрезолюция - это семантическая резолюция, в которой электроны содержат только литеры с отрицаниями.

I={ A, B}, A>B

E₁= AB N₁=A

N₂=B

E₂ = B



Рис.3.6.(б)

в) Стратегия множества поддержки.

Стратегия множества поддержки основывается на процедуре опровержения:

F1&F2&...&Fn&B, где F1,F2,...,Fn -выполнимые посылки, а B-ложь.

Тогда S₁={ F1,F2,...,Fn}, S₂={B}.

Множество поддержки S₁={A, B}, S₂={ AB}

I={ A, B}, A>B

A B AB



Рис.3.6.(с)

Деревья, представленные на Рис.3.6. (а, в, с), иллюстрируют вывод.

Пример 3.26.

Докажем утверждение примера 2.11, используя принцип резолюции и различные его модификации.

x(P(x)y(B(y)L(x,y)))

x(O(x)B(x))

_________________________

x(P(x)y(O(y)L(x,y)))

Приведем посылки и заключение к стандартной форме.

1.x(P(x)y(B(y)L(x,y)))=

xy(P(x)(B(y)L(x,y)))=

xy(P(x)B(y)L(x,y))=

P(x)B(y)L(x,y)

2. x(O(x)B(x))=  O(x)B(x)

3. (x(P(x)y(O(y)L(x,y))))=

(xy (P(x)(O(y)L(x,y))))=

(xy (P(x) O(y)  L(x,y)))=

xy(P(x)&O(y) &L(x,y))= P(a)&O(b) &L(a,b)

а) Принцип резолюции

1. P(x)B(y)L(x,y)

2.  O(x)B(x)

3. P(a)

4. O(b)

5. L(a,b)

______________________

6. B(y)  L(a,y) (1,3)  ={a/x}

7. B(b) (2,4)  ={b/x}

8. L(a,b) (6,7)  ={b/y}

9.  (5,8)

Дерево вывода представлено ниже, на рис. 3.7.

P(x)B(y)L(x,y) P(a)  O(x)B(x) O(b)

B(y)L(a,y) B(b)

L(a,b) L(a,b)



Рис.3.7.

б) Положительная гиперрезолюция

I={P, O, L,B}, P>B>L>O

Дерево вывода представлено ниже, на рис. 3.8.

E2= L(a,b) E1=P(a) N1=P(x)B(y)L(x,y) E3=O(b) N3= O(x)B(x)

E4=B(b)

Рис.3.8.

в) Отрицательная гиперрезолюция

I={P, O, L, B}, P>B>L>O

Дерево вывода представлено ниже, на рис. 3.9.

E1= P(x)B(y)L(x,y)

N1=P(a)

E2= B(y)L(a,y) N2= O(x)B(x)

E3= L(a,y)O(y) N3=L(a,b)

E4= O(b) N4=O(b)

Рис.3.9.

Задачи. Доказать утверждения п.2.2.2. (IV) и п.2.3.(II), используя три случая семантической резолюции: положительную гиперрезолюцию, отрицательную гиперрезолюцию и стратегию множества поддержки. Построить деревья вывода.