Основные понятия и методы теории формальных систем. Волохович А.В. - 27 стр.

    3. Каждая из литер в W k рассматривается как цепочка символов и
   выделяются первые подвыражения литер, не являющихся
   одинаковыми у всех элементов W k , т. е. образуется так называемое
   множество рассогласований типа (x k , t k ). Если в этом множестве x k
   – переменная, а t k – терм, отличный от x k , то перейти к пункту 4.
   В противном случае окончить работу: W неунифицируемо.
4. Пусть σ k + 1 = σ k { t k / x k } и W k + 1 = W k { t k / x k }.
5. Установить k=k+ 1 и перейти к пункту 2.

   Пример. Найти НОУ для W = { P(y, g(z), f(x)), P(a, x, f(g(y)))}.
   1) σ 0 =ε и W 0 = W.
   2) так как W 0 не является одноэлементным множеством, то
перейти к пункту 3.
   3) {у, а}, т. е. {а/у}.
   4) σ 1 =σ 0 {а/у} = ε {а/у} = {а/у}.
   W 1 = W 0 {а/у} = { P(a, g(z), f(x)), P(a, x, f(g(a)))}.
   5) так как W 1 опять неодноэлементно, то множество
рассогласований будет {g(z),x}, т. е. {g(z)/x}.
   6) σ 2 =σ 1 {g(z)/x} = {а/у, g(z)/x},
   W 2 = W 1 { g(z)/x } = { P(a, g(z), f(g(z))), P(a, g(z), f(g(a)))}.
   7) имеем {z, a},{z/ a}.
   8) σ 3 = σ 2 {z, a} = {а/у, g(z)/x, z,a},
   W 3 = W 2 { z, a } = { P(a, g(a), f(g(a))), P(a, g(a), f(g(a)))}= { P(a,
g(a), f(g(a)))},
   σ 3 =σ 2 {z, a} = {а/у, g(z)/x, z,a} есть НОУ для W .

    Если две или более одинаковые литеры (одного и того же знака)
дизъюнкта С имеют НОУσ, то Сσ называется фактором дизъюнкта
С.
    Пусть С 1 и С 2 – два дизъюнкта, не имеющих общих переменных
(это всегда можно получить переименованием переменных). И пусть
L 1 и L 2 = ¬ L 1 – литеры в дизъюнктах С 1 и С 2 соответственно,
имеющие НОУσ. Тогда бинарной резольвентой для С 1 и С 2 является
дизъюнкт вида С=( С 1 σ – L 1 σ) U (С 2 σ – L 2 σ). Бинарная резольвента
может быть получена одним из четырех способов:
    1) резольвента для С 1 и С 2 ;
    2) резольвента для С 1 и фактора дизъюнкта С 2 ;
    3) резольвента для фактора дизъюнкта С 1 и С 2 ;
    4) резольвента для фактора дизъюнкта С 1 и фактора дизъюнкта
С2.
    Пример. Пусть
                         С 1 = Р(f(g(а))) ∨ ¬ R(b),
                      С 2 = ¬ P(x) ∨ ¬ P(f(y)) ∨ Q(y).



27