Математическая логика и теория алгоритмов. Галуев Г.А. - 41 стр.

UptoLike

ВУЗ: 

ТТИ ЮФУ | Таганрог

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

Рубрика: 

Математическая Логика и Теория Алгоритмов стр. 41 из 64
© 2003 Галуев Геннадий Анатольевич
Сформулируем теперь алгоритм унификации:
0
1 К=0, множество
ε
σ
=
=
kk
WW , (пустое)
0
2 Если
k
W - единичный дизъюнкт, то
k
σ
это НОУ для W, конец алгоритма.
В противном случае найдем множество
k
D рассогласования для
k
W .
0
3 Если существуют такие элементы
k
γ
и
k
t , то переход к п.
0
4 .
0
4
⎭
⎬
⎫
⎩
⎨
⎧
=
+
k
k
kk
t
γ
οσσ
1
,
⎭
⎬
⎫
⎩
⎨
⎧
=
+
k
k
kk
t
WW
γ
1
(т.е. каждый элемент в
1+k
W получается применением подстановки
⎭
⎬
⎫
⎩
⎨
⎧
k
k
t
γ
к со-
ответствующему элементу из
k
W ).
0
5 1+= kk Переход к п.
0
2
О
О
п
п
р
р
е
е
д
д
е
е
л
л
е
е
н
н
и
и
е
е
.
. Если две или более литер (с одинаковым знаком инверсии) дизъ-
юнкта
C имеет НОУ
σ
, то
σ
C называют склейкой. Если
σ
C - единичный дизъюнкт, то
склейка называется единичной склейкой.
Например: пусть
C есть )())(()( xVQxfVPxP . Тогда литеры )(xP и ))(( yfP имеют
НОУ
{
}
x
yf )(
=
σ
. Значит ))(())(( yfQVyfP ¬ - есть склейка C т.е.
σ
C .
О
О
п
п
р
р
е
е
д
д
е
е
л
л
е
е
н
н
и
и
е
е
.
. Пусть
1
C и
2
C два дизъюнкта (дизъюнкты посылки), которые не
имеют общих переменных. Пусть
1
L и
2
L две литеры в
1
C и
2
C соответственно. Если
1
L и
2
L
имеют НОУ
σ
, то дизъюнкт
σσ
'
2
'
1
VCC , где
σ
'
1
C (или
σ
'
2
C ) получается выражением из
σ
1
C (
σ
2
C
) примера
σ
1
L
(или
σ
2
L
), называется бинарной резольвентой
1
C
и
2
C
.
О
О
п
п
р
р
е
е
д
д
е
е
л
л
е
е
н
н
и
и
е
е
.
. Резольвентой дизъюнктов посылок
1
C и
2
C является одна из сле-
дующих резольвент:
- бинарная резольвента
1
C и
2
C ;
- бинарная резольвента
1
C и склейки
2
C ;
- бинарная резольвента склейки
1
C и
2
C ;
- бинарная резольвента склейки
1
C и склейки
2
C .
Метод резолюций заключается в применении правила резолюций, которое поро-
ждает резольвенты для множества дизъюнктов.
Этот метод полон, т.е. для любого невыполнимого множества дизъюнктов можно
породить пустой дизъюнкт.
Рассмотрим пример работы этого метода.
Пусть имеется множество формул
1
F есть ))(&)()(( xRxWxCx →∀
2
F есть
)(&)( xQxxC∃
G есть )(&)( xRxxQ∃
Докажем с помощью метода резолюций, что
G является логическим следстви-
ем
1
F и
2
F , т.е. нужно доказать, что GFF ⎤&&
21
противоречиво. Преобразуем
1
F ,
2
F и
G⎤ в стандартную (скулемовскую) формулу.
Для
1
F имеем ))()((&)()(( xVRxCxVWxCx ⎤⎤∀
для
2
F имеем )(&)( aQaC
для
G⎤ )()( xRVxQx ⎤⎤∀ следовательно множество дизъюнктов S есть

Страницы