Унификация формул ИП.

Унификацией называется процесс подстановки термов на места переменных в ппф с целью приведения этих формул к требуемому виду.

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

Пример. Пусть необходимо из утверждений "все люди смертны" и "Сократ - человек" доказать формальным путем (используя ИППП) теорему "Сократ - смертен". Тогда предметные аксиомы будут иметь следующий вид:

1. AA1: A^-1x(Ч(x)->C(x))
   AA2: Ч(Сократ)

Доказательство:
а) Ч(Сократ)->С(Сократ) (правило специализации R6 к AA1);
б) С(Сократ) (правило заключения к AA2 и а).
Здесь для применения правила специализации на шаге а необходимо было найти подстановку "Сократ вместо x".

Подстановочным частным случаем некоторой ппф называется ппф, получившаяся подстановкой в эту (первоначальную) ппф термов на места переменных. При этом:

1. каждое вхождение переменной заменяется на один и тот же терм;
2. переменная не может быть заменена термом, содержащим ту же самую переменную.

Пример. Для ппф P(x,f(y),b) некоторыми подстановочными частными случаями будут:

1. P(z,f(v),b)
2. P(g(z),f(a),b)
3. P(c,f(a),b)

при этом первая ппф является алфавитным вариантом подстановки, а третья называется основным частным случаем, поскольку не содержит переменных.

Подстановки принято представлять в виде множества пар "терм/переменная":

s={t₁/v₁, t₂/v₂, ... ,t_n/v_n} .

Пример. Для рассмотренного выше примера подстановки выглядят следующим образом:

1. s1={z/x, v/y};
   s2={g(z)/x, a/y};
   s3={c/x, a/y}.

Для обозначения подстановочного частного случая некоторой ппф F пишут Fs.
Композиция двух подстановок s1 и s2, обозначаемая как s1s2, получается применением s2 к термам s1 с последующим добавлением тех пар из s2, которые содержат переменные, не встречающиеся среди переменных s1.

Некоторые свойства подстановок:

1. (Fs1)s2 = F(s1s2)
   (s1s2)s3 = s1(s2s3)
   s1s2 не равно s2s1 в общем случае

Множество ппф {F_i} унифицируемо, если существует подстановка s такая, что

F₁s = F₂s = ... = F_ns .

В этом случае s называется унификатором для множества {F_i}.

Наиболее общий унификатор (ноу) g обладает тем свойством, что, если s - любой унификатор для {F_i}, то существует некоторая подстановка s' такая, что

{F_i}s = {F_i}gs' .

Более того, основной частный случай, порождаемый ноу, является единственным с точностью до алфавитных его вариантов.

Существует много (не рассматриваемых здесь) алгоритмов, которые можно использовать для унификации конечного множества ппф [2].

Примечание. Унификация является более общим механизмом по сравнению с механизмом сопоставления с образцом (используемым в СУБД).