Математическая логика и теория алгоритмов

Теперь имеем формулы логики предикатов, в которых присутст­ вуют термы (в частности, переменные). Отличие метода резолюций в логике предикатов состоит в дополнительной процедуре работы с термами для унификации формул. Пусть имеем мнолсество литер {L,}. Если для этого множества существует общий унификатор 0ь например, (Li)Q J ~ (-^2)0, — (^s)e,> ™ из этих трех литер достаточно оставить только одну. Если для некото­ рых оставшихся существует общий унификатор 02, например, = ( L A)^^, ТО тоже оставляем только одну из них и т.д. Пример. Пусть D = P{f{a))vP{x)vQ{a^u))v Q{xJ{b))\j Q{z,w), тогда: 0 = {dx, blu, alz, f{b)lw}, Ds= P(/(a))v P (a) vQ (a J{b)). Если две или более литер дизъюнкта D имеют наиболее общий унификатор 0: (lik - {lj)s = (Li)e, то оставление одного из этих литералов вместо всех них называют склейкой. Пусть имеем два дизъюнкта Di иDj и переменные, входящие в D\, не входят в D2 и обратно. Если это не так, то переименованием переменных этого можно добиться. Пусть в Di есть литера, например, Li, а в D2 - литера Lj. Если Ц и 1Lj имеют наиболее общий унифика­ тор 9, т. е. (•^'Ое ~ (1 •^^2)0» то новый дизъюнкт R: r =m )9-(Li)8)v((D2)0-(L2)e) называется бинарной резольвентой Dj и (в логике предикатов). Литеры L\ viLi называются отрезаемыми литерами. Рассмотрим пример. Пусть D}=P{x) v Q(x), D2 =1 P(a)v Т{х). Переименуем х в Вг. D2 =1 P(a)v Т(у). Положим, что 0 = {а/х). Тогда имеем ; 111