Лекции по дискретной математике. Математическая логика. Зарипова Э.Р - 59 стр.

UptoLike

ВУЗ: 

РУДН | Москва

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

Рубрика: 

59
множества выражений W получается выявлением первой (слева)
позиции, на которой не для всех выражений из W стоит один и тот
же символ, а затем выписыванием из каждого выражения в W
подвыражения, которое начинается с символа, занимающего эту
позицию.
Пример 13.5.
}))))(((,(),,()),,(,({ xkhgxPaxPzyfxPW =
Множество рассогласований:
{f(y,z), a, g(h(k(x)))}.
Алгоритм унификации:
Шаг 1. K=0, W
k
=W,
τ
k
- пустой унификатор.
Шаг 2 . Если W
k
- единичный дизъюнкт, то остановка:
τ
k
–
унификатор для W. В противном случае находим множество
рассогласований D
k
для W
k
.
Шаг 3. Если существуют такие элементы v
k
и t
k
в D
k
, что v
k
-
переменная, не входящая в t
k
, то перейти к шагу 4. В противном
случае остановка: W не унифицируемо.
Шаг 4. Пусть
τ
k+1
=
τ
k
{t
k
/v
k
} и W
k+1
=W
k
{t
k
/v
k
} .
Шаг 5. k:=k+1 и перейти к шагу 2.
14. Метод резолюций в исчислении предикатов
Метод резолюций в исчислении предикатов
Определение. Атомарная формула есть литера.
Определение
. Если две или более литер (с одинаковым знаком)
дизъюнкта C имеют общий унификатор
δ
, то C
δ
называется
склейкой C. Если C
δ
- единичный дизъюнкт, то склейка
называется единичной склейкой.
Пример 14.1.
Пусть )())(()( xQyfPxPC ∨∨= . Тогда
подчеркнутые литеры имеют общий унификатор }/)({ xyf
=
δ
.
Следовательно,
(()) (()) (()) (()) (())C Pfy Pfy Qfy Pfy Qfy
δ
=∨∨=∨
есть склейка C .
Определение
. Пусть C
1
и C
2
- два дизъюнкта, которые не имеют

Страницы