Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

L3=P(g(z),f(a), b), L4 = P(c,f(a), b) - константный частный случай литерала или атом, т.к. нет переменных. Подстановки, примененные в рассматриваемом примере, можно обозна­ чить следующим образом: 01 = {z/x, w/yj, здесь Z подставляется вместо x,aw вместо у; 62 = {а/у}; вз = {g(z)/x, а/у}; 64 = {с/х, а/у}. Применение подстановки в к литералу L обозначаем Lg. Тогда имеем Lei=Li, ^^3=^3, L0^=L2, Если в - подстановка и она применяется к каждому из литералов L/, то по­ лученные частные случаи обозначаются через {и}д. Последовательное применение двух подстановок di и 62 дает новую под­ становку вз, которую обозначаем вз = di о 02. Множество {Li} литералов называется унифицируемым, если существует такая подстановка в, что (Ll)e = (1^2)0 = .. = (Lyjg. в этом случае подстановку в называют унификатором для {LJ. Унификация возможна различными способами. Например, литералы Р{х) и Р(у) можно унифицировать подставив вместо хиу постояннуюс и в результате получим: Р(с)яР(с), (3.7) либо заменить х и на какой то иной терм. При замене переменных постоян­ ными, будем получать частный случай, который в дальнейшем уже не меняет­ ся. Более общий случай получится, если заменить х и на какую то перемен­ ную, например, на z, тогда в результате получим: P {z)h P {z). (3.8) Результат (3.8) более общий, более универсальный, ибо его можно преоб­ разовать в (3.7), заменив z на с, а из (3.7) получить (3.8) нельзя. Унификатор (7 для множества выражений {Ei,E2,... ,Ek} называется наибо­ лее общим унификатором тогда и только тогда, когда для каждого унификатора в для этого множества существует такая подстановка X, что в = сг ° А Одно из важных требований унификации состоит в том, что унификатор должен быть максимально общим, т.е. для любых двух термов должен быть найден наиболее общий унификатор. При потере общности при унификации уменьшается возможность достижения окончательного решения рассматривае­ мой задачи или такая возможность исчезает полностью. Существует алгоритм, называемый алгоритмом унификации, который приводит к наиболее общему унификатору для унифицируемого множества ли­ тералов {Li} и сообщает о неудаче, если это множество неунифицируемо. 1А