Подстановка и унификация в логике предикатов 1-го порядка. Алгоритм нахождения наиболее общего унификатора

если = {x₁ = t₁, x₂ = t₂ … x_n = t_n}, F – дизъюнкт, то через (F) будем обозначать дизъюнкт, полученный из F одновременной заменой x₁ на t₁ и т.д. x_n на t_n

Ех: = {x₁ = f(x₂), x₂ = c}

Пустая подстановка – подстановка, не содержащая равенств.

Унификация - подбор такой подстановки, которая позволит сделать несколько литералов идентичными.

Пусть {E₁, …, E_k} – множество литералов или множество термов. Подстановка называется унификатором этого множества,

если (E₁) = (E₂) = … = (E_k)

Множество унифицируемо, если существует унификатор этого множества.

Ех: множество атомов функционирования {Q (a, x, f(x)), Q(u, y, z)}

Унифицируемо подстановкой {u = a, y = x, z = f(x)}

Результат унификации: {Q(a, x, f(x)), Q(a, x, f(x))}

Ех2: множество {R(x, f(x)), R(u, u)} не унифицируемо, если заменить x на u получим {R(u, f(u)), R(u, u)} нельзя проводить замену u = f(u), т.к. тогда получим

R(f(u), f(f(u))) и R(f(u), f(u)).

Если множество унифицируемо, то существует, как правило, не один унификатор этого множества, а несколько. Среди всех унификаторов данного множества выделяют наиболее общий унификатор.

Пусть имеется две подстановки:

= {x₁ = t₁, x₂ = t₂ … x_k = t_k}

= {y₁ = s₁, y₂ = s₂ … y_e = s_e}

Тогда произведением подстановок и называется подстановка, которая получается из последовательных равенств

{x₁ = (t₁), x₂ = (t₂), … x_k = (t_k), y₁ = s₁, y₂ = s₂, y_e = s_e} вычёркиваем равенства вида x_i = x_i для 1 i k, y_i = s_i, если y_i {x₁, …, x_k}, для 1 j l.

Произведением (композицией) подстановок и называется подстановка, которая получается путём применения подстановки к термам подстановки с добавлением из всех подстановочных пар, содержащих переменные, отсутствующее в .

Ех: = {z = f(x, y)}

= {x = a, y = b, w = c, z = d}

Последовательность равенств из определения произведения имеет вид:

= {z = f(x, y), x = a, y = b, w = c} = {z = f (a, b), x = a, y = b, w = c}.

Унификатор множества литералов или термов называется наиболее общим унификатором этого множества, если для любого унификатора того же множества литералов существует подстановка такая, что =

Ех: {P(x, f(a), g(z), P(f(b, y, v)))}

Наиболее общим унификатором является подстановка = {x = f(b), y = f(a), v = g(z)}

Если в качестве взять унификатор {x = f(b), y = f(a), z = c, v = g(c)},

то = {z = c}

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

Ех: если M = {P(x, f(y), a), P(x, u, g(y)), P(x, c, v)}, множество рассогласованностей состоит из термов f(y), u, c

Множество рассогласованностей {P(x, y), P(a, g(z))} есть само множество

Если M = { P(x, y), Q(a, v)}, то множество рассогласованностей равно

{P(x, y), Q(a, v)}

Алгоритм нахождения наиболее общего унификатора.

Шаг 1. k = 0, M _k= M, _k = , где - пустая подстановка

Шаг 2. Если множество M _k состоит из одного литерала (содержит 1 элемент), то выдать _k в качестве наиболее общего унификатора и завершить работу. В противном случае найти множество N _k рассогласованностей в M _k.

Шаг 3. Если в множестве N _k существует переменная v_k и терм t_k, не содержащий v_k, то перейти к шагу 4, иначе выдать сообщение о том, что множество М не унифицируемо и завершить работу.

Шаг 4. Положить _k+1 = {v_k = t_k} _k, т.е. подстановка _k+1 получается из _k заменой v_k на t_k и, возможно добавлением равенства v_k = t_k.

В множестве M _k выполнить замену v_k = t_k, полученное множество литералов взять в качестве M _k+1

Шаг 5. Присвоить k = k + 1 и перейти к шагу 2.