Основы построения и функционирования интеллектуальных информационных систем. Былкин В.Д - 32 стр.

UptoLike

ВУЗ: 

ПГУ | Пенза

Составители: 

Рубрика: 

32
упоминавшаяся повторяющаяся формула (или сопоставимые формулы), является
следствием указанных дизъюнктов.
Пусть S - множество дизъюнктов, исследуемых на невыполнимость. Алгоритм для метода
резолюции представлен ниже.
Пока Λ € S, искать l
1
, l
2
, S
1
, S
2
такие, что S
1
и S
2
есть дизъюнкты или факторы дизъюнктов;
l
1
€ S
1
, l
2
€ S
2
и l
1
, l
2
унифицируемы.
Вычислить резольвенту r , заменив S на S \{r}.
Пример. Доказать, что если G - группа, каждый элемент которой является обратным самому себе,
то G - коммутативна.
Будем использовать следующие гипотезы:
H
1
: x y z [(x y) z = x (y z)];
H
2
: x [x e = x = e z];
H
3
: x [x x = e]
Заключение имеет следующий вид: С: x y [x y = x y ]; Для исключения предиката
равенства полагаем
P (x, y, z) =
def
x y = z.
Представив гипотезы и отрицание заключения в клаузальной форме, получим множество
дизъюнктов:
1. ┐P(x, y, u) v P(y, z, ) v P(u, z, ) v P(x, , )
2. ┐P(x, y, u) v P(y, z, ) v P(x, , ) v P(u, z, )
3. P(x, e, x)
4. P(e, x, x)
5. P(x, x, x)
6. P(a, b, c)
7. ┐P(b, a, c)
Получение пустого дизъюнкта представлено ниже. В правой части списка указаны номера
дизъюнктов, над которыми осуществляется резолюция, а также используемые унификаторы.
8. ┐P(x, z, ) v ┐P(e, z, ) v P(x, , )
1 {(y, x) , (u, e)}, 5
9. ┐P(b, z, ) v P(a, , ) v P(c, z, )
2 {(x, a) , (y, b), (u, c)}, 6
10. ┐P(x, z, ) v P(x, , z)
4 {(x, z)} ; 8 {( , z)}
11. ┐ P(a, e, ) v P(c, b , )
5 {(x, b)} ; 9 {(z , b) , ( , e)}
12. P(c, b, a)
3 {(x, a)} ; 11 {( , a)}
13. P(c, a, b)
10 {(x, c) , (z, b), ( ,a )}, 12
14. ┐P(x, y, u) v ┐P(x, e, ) v P(u, y , )
2 {( , e), (z, y)} , 5 {( , z)}
15. ┐P(x, y, u) v ┐P(u, y, x)
3, 14 {( , x)}
16. P(b, a, c)
13, 15 {(x, c) , (y, a), (u ,b )}
17. ^
7, 16 
        упоминавшаяся повторяющаяся формула (или сопоставимые формулы), является
следствием указанных дизъюнктов.
       Пусть S - множество дизъюнктов, исследуемых на невыполнимость. Алгоритм для метода
резолюции представлен ниже.
       Пока Λ € S, искать l1 , l2 , S1 , S2 такие, что S1 и S2 есть дизъюнкты или факторы дизъюнктов;
l1 € S1 , l2 € S2 и l1, l2 унифицируемы.
Вычислить резольвенту r , заменив S на S \{r}.
Пример. Доказать, что если G - группа, каждый элемент которой является обратным самому себе,
то G - коммутативна.
Будем использовать следующие гипотезы:
     H1: x y z [(x y) z = x (y z)];
     H2: x [x e = x = e z];
     H3: x [x x = e]
Заключение имеет следующий вид: С: x y [x                y=x      y ]; Для исключения предиката
равенства полагаем
                                           P (x, y, z) = def x y = z.
   Представив гипотезы и отрицание заключения в клаузальной форме, получим множество
дизъюнктов:
   1. ┐P(x, y, u) v P(y, z, ) v P(u, z, ) v P(x, , )
   2. ┐P(x, y, u) v P(y, z, ) v P(x, , ) v P(u, z, )
   3. P(x, e, x)
   4. P(e, x, x)
   5. P(x, x, x)
   6. P(a, b, c)
   7. ┐P(b, a, c)
   Получение пустого дизъюнкта представлено ниже. В правой части списка указаны номера
дизъюнктов, над которыми осуществляется резолюция, а также используемые унификаторы.
   8. ┐P(x, z, ) v ┐P(e, z, ) v P(x, , )                   1 {(y, x) , (u, e)}, 5
   9. ┐P(b, z, ) v P(a, , ) v P(c, z, )                    2 {(x, a) , (y, b), (u, c)}, 6
   10.   ┐P(x, z, ) v P(x, , z)                            4 {(x, z)} ; 8 {( , z)}
   11.   ┐ P(a, e, ) v P(c, b , )                          5 {(x, b)} ; 9 {(z , b) , ( , e)}
   12.   P(c, b, a)                                        3 {(x, a)} ; 11 {( , a)}
   13.   P(c, a, b)                                        10 {(x, c) , (z, b), ( ,a )}, 12
   14.   ┐P(x, y, u) v ┐P(x, e, ) v P(u, y , )             2 {( , e), (z, y)} , 5 {( , z)}
   15.   ┐P(x, y, u) v ┐P(u, y, x)                         3, 14 {( , x)}
   16.   P(b, a, c)                                        13, 15 {(x, c) , (y, a), (u ,b )}
   17.   ^                                                 7, 16




                                                      32

Страницы