Представление и обработка знаний

73 Для логики предикатов при получении резольвент (новых дизъюнктов) возникают трудности в связи с согласованием кон- трарных пар. Например: C 1 : P ( x )   R ( x ); C 2 :  P ( g ( x ))  Q ( x ). В этом случае для получения резольвенты осуществляют подстановку: g ( x ) вместо x . Тогда: C 1 * : P ( g ( x ))   R ( x ), C 2 * :  P ( g ( x ))  Q ( x ) и получаем резольвенту: C :  R ( x )  Q ( x ). Процесс согласования называется унификацией. Подстановкой называют функцию, которая ставит в соответ- ствие каждому элементу множества переменных V множество тер- мов T :  : V  T. Например, множества равны соответственно V = { x , y , z } и T = { y , z , g ( x )}. Рассмотрим подстановку:  : {( x  g ( x )), ( y  y ), ( z  z )}. Переменная x ( x  V ) – активная для подстановки, если  ( x )  x . В рассмотренном примере активной переменной для под- становки является только переменная x. Подстановка называется элементарной, если в ней имеется только одна активная переменная. Подстановка   рассмотренного примера является элементарной. В следующем примере рассмотрим применение подстановки:   = {( x  f ( x )), ( y  g ( x , y ))} к терму: g ( f ( x ), g ( f ( z ), y )). Пусть мно- жество V = { x , y }, а T = { f ( x ), g ( x , y )}. Результатом подстановки   является терм: g ( f ( f ( x )), g ( f ( z ), g ( x , y )).