Зарипова, Э.Р. Дискретная математика Часть II. Математическая логика

68 Говорят, что множество унифицируемо, если для него существует унификатор. Определение. Множество рассогласований непустого множества выражений W получается выявлением первой (слева) позиции, на которой не для всех выражений из W стоит один и тот же символ, а затем выписыванием из каждого выражения в W подвыражения, которое начинается с символа, занимающего эту позицию. Пример 13.5. Найти множество рассогласований. { ( , ( , )), ( , ), ( , ( ( ( ))))} W P x f y z P x a P x g h k x  Множество рассогласований: {f(y,z), a, g(h(k(x)))}. Алгоритм унификации: Шаг 1. K=0, W k =W,  k – пустой унификатор. Шаг 2. Если W k – единичный дизъюнкт, то остановка:  k – унификатор для W . В противном случае находим множество рассогласований D k для W k . Шаг 3. Если существуют такие элементы v k и t k в D k , что v k – переменная, не входящая в t k , то перейти к шагу 4. В противном случае остановка: W не унифицируемо. Шаг 4. Пусть  k+1 =  k {t k /v k } и W k+1 =W k {t k /v k } . Шаг 5. k:=k+1 и перейти к шагу 2.