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

75 отличаются только названиями переменных, т.е. существует биек- тивное отображение f между var ( t 1 ) и var ( t 2 ) , такое что t 2 получается при одновременной замене всех переменных x из var ( t 1 ) на f ( x ), а t 1 получается из t 2 при замене y из var ( t 2 ) на f – 1 ( y ). Разобьем все множество термов на подмножества. Для каж- дого подмножества выполняется правило: для каждых двух эле- ментов множества t 1 и t 2 существуют подстановки, которые выво- дят терм t 1 из t 2 и t 2 из t 1 . В этом случае все множество термов раз- бивается на классы эквивалентности. Внутри каждого подмножест- ва отношение выводимости является отношением эквивалентности. Очевидно, что отношение выводимости обладает антисим- метричностью, если рассматриваются термы, принадлежащие раз- личным классам эквивалентности. Отношение выводимости обла- дает транзитивностью. Таким образом, на множестве классов экви- валентности отношение выводимости является отношением час- тичного порядка. Существует максимальный терм x , который не может быть получен ни одной подстановкой. Существуют минимальные термы  вполне конкретизируемые термы. Термы t 1 и t 2 унифицируемы или сопоставимы, если сущест- вует такая подстановка, что  [ t 1 ] =   [ t 2 ]. Подстановка  называется унификатором, а результат общей унификацией t 1 и t 2 . Например, подстановка:  (   = {( x  a ), ( y  w ), ( u  a ), ( v  w ), ( e  a )}), примененная к термам t 1 = f 1 ( x , y , g ( x , 1)) и t 2 = f 2 ( u , v , g ( e , 1)), дает результат:  [ f 1 ( x , y , g ( x , 1))] = f 1 ( a , w , g ( a , 1));  [ f 2 ( u , v , g ( e , 1))] = f 2 ( a , w , g ( a , 1)) . Результаты подстановки совпадают:   [ t 1 ] =   [ t 2 ], поэтому подстановка   является унификатором термов t 1 и t 2 .