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

UptoLike

ВУЗ: 

ПГУ | Пенза

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

Рубрика: 

31
Найти наибольшую нижнюю границу множества T/ с заданным на нем отношением <.
Решение: .
Множество полных конкретизации дизъюнктов (дизъюнкция конечного числа литер) в
эрбрановой области называется множеством фундаментальных конкретизации,
Унификация
Унификация (сопоставление) является основной операцией в методе резолюций. Пусть
даны два дизъюнкта
и , принадлежащие множеству S. Предположим, что литеры l
1
и l
2
являются унифицируемыми, т. е. обладают общей фундаментальной конкретизацией. Из каждой
пары фундаментальных конкретизаций
и ,
таких, что l
1
'=l
1
'=l
1
' получается резольвента .
Каждый дизъюнкт такого типа является логическим следствием из С
1
и С
2
. Задача состоит
в том, чтобы найти такой дизъюнкт R, фундаментальные конкретизации которого были бы в
точности конкретизациями того же самого типа, как и для R' . Обозначим через l
U
наибольшую
нижнюю границу пары {l
1
, l
2
} относительно порядка < . Наиболее общим унификатором литер l
1
и
l
2
, ,будем называть подстановку
U
, такую, что
U
[l
1
]=
U
[l
2
]=l
U
.
Резольвентным дизъюнктом (резольвентой) R с требуемым свойством будет следующее
выражение:
.
Метод резолюций
Главная идея метода резолюций состоит в том, что, если одна и та же атомарная формула
(или сопоставимые формулы) появляется (-ются) в одном дизъюнкте без отрицания, а в другом - с
отрицанием, то дизъюнкт, называемый резольвентой и получаемый в результате соединения этих
двух дизъюнктов, из которых вычеркнута
)(),(( bgafyh(t)
,...}{
11
lC
,...}{
22
lC
,...}{
'
1
'
1
lC
,...}{
'
2
'
2
lC
}){\(}){\(
''
2
''
1
'
lClCR
}{\])[σ(}){\][σ(
1U1U UU
lClCR
Найти наибольшую нижнюю границу множества T/ с заданным на нем отношением <.

        Решение: h(t)        y ( f (a), g (b) .

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


                                                      Унификация
        Унификация (сопоставление) является основной операцией в методе резолюций. Пусть
даны два дизъюнкта
C1 {l1 ,...}и C2 {l2 ,...}, принадлежащие множеству S. Предположим, что литеры l1 и l2

являются унифицируемыми, т. е. обладают общей фундаментальной конкретизацией. Из каждой
пары фундаментальных конкретизаций
C1' {l1' ,...}и C2'   { l2' ,...},
                                                '
таких, что l1'=l1'=l1' получается резольвента R                 (C1' \ {l ' })    (C2' \ { l ' }) .

        Каждый дизъюнкт такого типа является логическим следствием из С1 и С2 . Задача состоит
в том, чтобы найти такой дизъюнкт R, фундаментальные конкретизации которого были бы в
точности конкретизациями того же самого типа, как и для R' . Обозначим через lU наибольшую
нижнюю границу пары {l1 , l2} относительно порядка < . Наиболее общим унификатором литер l1 и
l2, ,будем называть подстановку             U   , такую, что    U   [l1]=    U   [l2]=lU.
        Резольвентным дизъюнктом (резольвентой) R с требуемым свойством будет следующее
выражение:
                                        R (σ U [C1 ] \ {lU })       (σ U [C1 ]) \ { lU } .


                                                   Метод резолюций
        Главная идея метода резолюций состоит в том, что, если одна и та же атомарная формула
(или сопоставимые формулы) появляется (-ются) в одном дизъюнкте без отрицания, а в другом - с
отрицанием, то дизъюнкт, называемый резольвентой и получаемый в результате соединения этих
двух дизъюнктов, из которых вычеркнута




                                                               31

Страницы