13.7. Подстановка и унификация

Применение метода резолюций в логике предикатов усложня­ется тем, что дизъюнкты содержат термы, которые могут не совпадать в двух одинаковых литерах. Например, С₁=Р(х)Q(x), С₂=Р(f(а))V(a). В этих дизъюнктах нет контрарных литер, однако, если мы подставим f(а) вместо x в С₁, то получим С₁=Р(f(а))Q(f(я)); теперь литеры Р(f(а)) и Р(f(а)) будут уже контрарные. Получим резольвенту Q(f(а))V(a).

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

Определение 13.14. Подстановка — это конечное множество вида {t₁/v₁, ..., t_n/v_n}, где v_i – переменная, t_i - терм, отличный от v_i, и все v_i различны.

Определение 13.15. Пусть  = {t₁/v₁, ..., t_n/v_n}, и Е— выражение. Тогда Е выражение, полученное из Е заменой всех вхождений переменных v_i(1in) на термы t_i.

Определение 13.16. Пусть  = {t₁/v₁, ..., t_n/v_n},  = {u₁/y₁, ..., u_k/y_k} – подстановки. Композиция подстановок ° получается из мно­жества {t₁/v₁, ..., t_n/v_n, u₁/y₁, ..., u_k/y_k} вычеркиванием всех элементов t_j/v_j, для которых t_j=v_j. (тождественная подстанов­ка), и всех элементов u_i/y_i. таких, что у_i{v_i, …, v_n}.

Пример. Пусть  = {t₁/v₁, t₂/v₂} = {f(y)/x, z/y} ={u₁/y₁, u₂/y₂, u₃/y₃}={a/x, b/y, y/z}. Тогда °= {t₁/v₁, t₂/v_2­, u₁/y₁, u₂/y₂, u₃/y₃}={f(b)/x, y/y, a/x, b/y, y/z}. Так как t₂/x_2­=y/y, то y/y должно быть вычеркнуто из множества °. Элементы а/х, b/у также долж­ны быть вычеркнуты, так как подстановки для х и у уже определены. В результате получаем: ° = {f(b)/х, у/z).

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

Определение 13.17. Подстановка  называется унификатором множества {Е₁, ..., Е_m} тогда и только тогда, когда Е₁ = ... = Е_m. Множество {Е­₁, ..., E_m} называется унифицируемым, если для него существует унификатор. Унификатор  для множества выраже­ний {Е₁, ..., Е_m} называется наиболее общим унификатором, если для каждого унификатора  этого множества существует такая подстановка , что  = ^о.

Например, для двух дизъюнктов {Р(а, у), Р(х, f(b)} подстановка {а/х, f(b)/у} является наиболее общим унификатором.

Введя понятие унификации, мы можем рассмотреть метод резо­люции для логики первого порядка.

Определение 13.18. Если две или более литер (с одинаковым знаком) дизъюнкта С имеют наиболее общий унификатор , то С называется склейкой С. Если С - единичный дизъюнкт, то склейка называется единичной склейкой.

Пример. Пусть С = Р(х)Р(f(у))Q(х). Тогда первая и вто­рая литеры имеют наиболее общий унификатора ={f(y)/x}. Следо­вательно, С = Р(f(у))Q(f(у)) есть склейка С.

Определение 13.19. Пусть С₁, и С₂ - два дизъюнкта (называемые дизъюнктами-посылками), которые не имеют никаких общих переменных. Пусть L₁, и L₂ две литеры в С₁, и С₂, соответствен­но. Если L₁ и L₂ имеют наиболее общий унификатор , то дизъюнкт (C₁\L₁)(C₁\L₁) называется (бинарной) резольвентой С₁, и С₂.Литеры L₁ и L₂ называются отрезаемыми литерами.

Определение 13.20. Резольвентой дизъюнктов-посылок С₁, и С₂ является одна из следующих резольвент:

1) бинарная резольвента С₁ и С₂;

2) бинарная резольвента С₁ и склейки С₂;

3) бинарная резольвента С₁ и склейки С₁;

4) бинарная резольвента склейки С₁, и склейки С₂.

Пример. Пусть C₁=P(x)P(f(y))R(g(y)) и C₂ = P(f(g(a)))Q(b). Склейка C₁ есть C₂=P(f(y))R(g(y)). Выполним подста­новку g(а)/у. Бинарная резольвента С₁ и С₂ есть R(g(g(a)))Q(b). Следовательно, R(g(g(a)))Q(b) есть резольвента С₁ и С₂.